scmfsa6a.miz



    begin

    reserve l,m,n for Nat,

i,j,k for Instruction of SCM+FSA ,

I,J,K for Program of SCM+FSA ;

    ::$Canceled

    definition

      let P be preProgram of SCM+FSA ;

      :: SCMFSA6A:def1

      func Directed P -> preProgram of SCM+FSA equals (P +~ (( halt SCM+FSA ),( goto ( card P))));

      coherence ;

      projectivity by FUNCT_4: 127;

    end

    registration

      let I be Program of SCM+FSA ;

      cluster ( Directed I) -> initial non empty;

      coherence

      proof

        thus ( Directed I) is initial

        proof

          let m,n be Nat such that

           A1: n in ( dom ( Directed I)) and

           A2: m < n;

          n in ( dom I) by A1, FUNCT_4: 99;

          then m in ( dom I) by A2, AFINSQ_1:def 12;

          hence thesis by FUNCT_4: 99;

        end;

        thus ( Directed I) is non empty;

      end;

    end

    theorem :: SCMFSA6A:1

     not ( halt SCM+FSA ) in ( rng ( Directed I)) by FUNCT_4: 100;

    theorem :: SCMFSA6A:2

    ( Reloc (( Directed I),m)) = ((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto (m + ( card I))))) * ( Reloc (I,m)))

    proof

      ( rng (( halt SCM+FSA ) .--> ( goto ( card I)))) = {( goto ( card I))} by FUNCOP_1: 8;

      then

       A1: ( rng (( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto ( card I))))) c= (( rng ( id the InstructionsF of SCM+FSA )) \/ {( goto ( card I))}) by FUNCT_4: 17;

      

       A2: (( rng ( id the InstructionsF of SCM+FSA )) \/ {( goto ( card I))}) = the InstructionsF of SCM+FSA by ZFMISC_1: 40;

      ( dom (( halt SCM+FSA ) .--> ( goto ( card I)))) = {( halt SCM+FSA )};

      

      then ( dom (( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto ( card I))))) = (( dom ( id the InstructionsF of SCM+FSA )) \/ {( halt SCM+FSA )}) by FUNCT_4:def 1

      .= the InstructionsF of SCM+FSA by ZFMISC_1: 40;

      then

      reconsider f = (( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto ( card I)))) as Function of the InstructionsF of SCM+FSA , the InstructionsF of SCM+FSA by A1, A2, FUNCT_2:def 1, RELSET_1: 4;

      

       A3: ( IncAddr (( goto ( card I)),m)) = ( goto (m + ( card I))) by SCMFSA_4: 1;

      ( dom ( id the InstructionsF of SCM+FSA )) = the InstructionsF of SCM+FSA ;

      then

       A4: f = (( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ),( goto ( card I)))) by FUNCT_7:def 3;

      

       A5: ( rng I) c= the InstructionsF of SCM+FSA by RELAT_1:def 19;

      

       A6: ( Reloc (( Directed I),m)) = ( IncAddr (( Shift (( Directed I),m)),m)) by COMPOS_1: 34;

      

       A7: ( Reloc (I,m)) = ( IncAddr (( Shift (I,m)),m)) by COMPOS_1: 34;

      ( Directed I) = (f * I) by A4, A5, FUNCT_7: 116;

      

      hence ( Reloc (( Directed I),m)) = ( IncAddr ((f * ( Shift (I,m))),m)) by A6, VALUED_1: 22

      .= ((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto (m + ( card I))))) * ( Reloc (I,m))) by A3, A7, COMPOS_1: 47;

    end;

    reserve a,b for Int-Location,

f for FinSeq-Location,

s,s1,s2 for State of SCM+FSA ;

    set q = (( intloc 0 ) .--> 1);

    set f = ( the_Values_of SCM+FSA );

    theorem :: SCMFSA6A:3

    

     Th3: ( InsCode i) in { 0 , 6, 7, 8} or (( Exec (i,s)) . ( IC SCM+FSA )) = (( IC s) + 1)

    proof

      assume

       A1: not ( InsCode i) in { 0 , 6, 7, 8};

      then

       A2: ( InsCode i) <> 0 & ( InsCode i) <> 6 by ENUMSET1:def 2;

      

       A3: ( InsCode i) <> 7 & ( InsCode i) <> 8 by A1, ENUMSET1:def 2;

      ( InsCode i) = 0 or ... or ( InsCode i) = 12 by SCMFSA_2: 16;

      per cases by A2, A3;

        suppose ( InsCode i) = 1;

        then ex a, b st i = (a := b) by SCMFSA_2: 30;

        hence thesis by SCMFSA_2: 63;

      end;

        suppose ( InsCode i) = 2;

        then ex a, b st i = ( AddTo (a,b)) by SCMFSA_2: 31;

        hence thesis by SCMFSA_2: 64;

      end;

        suppose ( InsCode i) = 3;

        then ex a, b st i = ( SubFrom (a,b)) by SCMFSA_2: 32;

        hence thesis by SCMFSA_2: 65;

      end;

        suppose ( InsCode i) = 4;

        then ex a, b st i = ( MultBy (a,b)) by SCMFSA_2: 33;

        hence thesis by SCMFSA_2: 66;

      end;

        suppose ( InsCode i) = 5;

        then ex a, b st i = ( Divide (a,b)) by SCMFSA_2: 34;

        hence thesis by SCMFSA_2: 67;

      end;

        suppose ( InsCode i) = 9;

        then ex a, b, f st i = (b := (f,a)) by SCMFSA_2: 38;

        hence thesis by SCMFSA_2: 72;

      end;

        suppose ( InsCode i) = 10;

        then ex a, b, f st i = ((f,a) := b) by SCMFSA_2: 39;

        hence thesis by SCMFSA_2: 73;

      end;

        suppose ( InsCode i) = 11;

        then ex a, f st i = (a :=len f) by SCMFSA_2: 40;

        hence thesis by SCMFSA_2: 74;

      end;

        suppose ( InsCode i) = 12;

        then ex a, f st i = (f :=<0,...,0> a) by SCMFSA_2: 41;

        hence thesis by SCMFSA_2: 75;

      end;

    end;

    ::$Canceled

    theorem :: SCMFSA6A:8

    for s1,s2 be State of SCM+FSA , n be Nat, i be Instruction of SCM+FSA holds (( IC s1) + n) = ( IC s2) & ( DataPart s1) = ( DataPart s2) implies (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) & ( DataPart ( Exec (i,s1))) = ( DataPart ( Exec (( IncAddr (i,n)),s2)))

    proof

      set D = ( Data-Locations SCM+FSA );

      let s1,s2 be State of SCM+FSA ;

      let n be Nat;

      let i be Instruction of SCM+FSA ;

      assume that

       A1: (( IC s1) + n) = ( IC s2) and

       A2: ( DataPart s1) = ( DataPart s2);

      reconsider k1 = ( IC s1) as Element of NAT ;

      

       A3: ((( IC s1) + 1) + n) = ((k1 + 1) + n)

      .= (( IC s2) + 1) by A1;

       A4:

      now

        set I = ( InsCode i);

        assume that

         A5: I < 6 or 8 < I and

         A6: I <> 0 ;

         not (I = 6 or ... or I = 8) by A5;

        then not I in {6, 7, 8} by ENUMSET1:def 1;

        then

         A7: ( IncAddr (i,n)) = i by SCMFSA_4: 4;

         not (I = 0 or (I = 6 or ... or I = 8)) by A5, A6;

        then

         A8: not I in { 0 , 6, 7, 8} by ENUMSET1:def 2;

        then ( IC ( Exec (i,s1))) = (( IC s1) + 1) by Th3;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A3, A8, A7, Th3;

      end;

      ( InsCode i) = 0 or ... or ( InsCode i) = 12 by SCMFSA_2: 16;

      per cases ;

        suppose ( InsCode i) = 0 ;

        then

         A9: i = ( halt SCM+FSA ) by SCMFSA_2: 95;

        then ( Exec (i,s1)) = s1 & ( Exec (i,s2)) = s2 by EXTPRO_1:def 3;

        hence thesis by A1, A2, A9, COMPOS_0: 4;

      end;

        suppose

         A10: ( InsCode i) = 1;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da,db be Int-Location such that

         A11: i = (da := db) by A10, SCMFSA_2: 30;

        

         A12: ( IncAddr (i,n)) = i by A11, COMPOS_0: 4;

         A13:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A14: c = da;

            

            hence (( Exec (i,s1)) . c) = (s1 . db) by A11, SCMFSA_2: 63

            .= (s2 . db) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A11, A12, A14, SCMFSA_2: 63;

          end;

            suppose

             A15: c <> da;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A11, SCMFSA_2: 63

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A11, A12, A15, SCMFSA_2: 63;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A11, SCMFSA_2: 63

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A11, A12, SCMFSA_2: 63;

        end;

        hence thesis by A13, SCMFSA_M: 2;

      end;

        suppose

         A16: ( InsCode i) = 2;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da,db be Int-Location such that

         A17: i = ( AddTo (da,db)) by A16, SCMFSA_2: 31;

        

         A18: ( IncAddr (i,n)) = i by A17, COMPOS_0: 4;

         A19:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A20: c = da;

            (s1 . da) = (s2 . da) & (s1 . db) = (s2 . db) by A2, SCMFSA_M: 2;

            

            hence (( Exec (i,s1)) . c) = ((s2 . da) + (s2 . db)) by A17, A20, SCMFSA_2: 64

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A17, A18, A20, SCMFSA_2: 64;

          end;

            suppose

             A21: c <> da;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A17, SCMFSA_2: 64

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A17, A18, A21, SCMFSA_2: 64;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A17, SCMFSA_2: 64

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A17, A18, SCMFSA_2: 64;

        end;

        hence thesis by A19, SCMFSA_M: 2;

      end;

        suppose

         A22: ( InsCode i) = 3;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da,db be Int-Location such that

         A23: i = ( SubFrom (da,db)) by A22, SCMFSA_2: 32;

        

         A24: ( IncAddr (i,n)) = i by A23, COMPOS_0: 4;

         A25:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A26: c = da;

            (s1 . da) = (s2 . da) & (s1 . db) = (s2 . db) by A2, SCMFSA_M: 2;

            

            hence (( Exec (i,s1)) . c) = ((s2 . da) - (s2 . db)) by A23, A26, SCMFSA_2: 65

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A23, A24, A26, SCMFSA_2: 65;

          end;

            suppose

             A27: c <> da;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A23, SCMFSA_2: 65

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A23, A24, A27, SCMFSA_2: 65;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A23, SCMFSA_2: 65

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A23, A24, SCMFSA_2: 65;

        end;

        hence thesis by A25, SCMFSA_M: 2;

      end;

        suppose

         A28: ( InsCode i) = 4;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da,db be Int-Location such that

         A29: i = ( MultBy (da,db)) by A28, SCMFSA_2: 33;

        

         A30: ( IncAddr (i,n)) = i by A29, COMPOS_0: 4;

         A31:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A32: c = da;

            (s1 . da) = (s2 . da) & (s1 . db) = (s2 . db) by A2, SCMFSA_M: 2;

            

            hence (( Exec (i,s1)) . c) = ((s2 . da) * (s2 . db)) by A29, A32, SCMFSA_2: 66

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A29, A30, A32, SCMFSA_2: 66;

          end;

            suppose

             A33: c <> da;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A29, SCMFSA_2: 66

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A29, A30, A33, SCMFSA_2: 66;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A29, SCMFSA_2: 66

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A29, A30, SCMFSA_2: 66;

        end;

        hence thesis by A31, SCMFSA_M: 2;

      end;

        suppose

         A34: ( InsCode i) = 5;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da,db be Int-Location such that

         A35: i = ( Divide (da,db)) by A34, SCMFSA_2: 34;

        

         A36: ( IncAddr (i,n)) = i by A35, COMPOS_0: 4;

         A37:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A38: c = db;

            (s1 . da) = (s2 . da) & (s1 . db) = (s2 . db) by A2, SCMFSA_M: 2;

            

            hence (( Exec (i,s1)) . c) = ((s2 . da) mod (s2 . db)) by A35, A38, SCMFSA_2: 67

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A35, A36, A38, SCMFSA_2: 67;

          end;

            suppose

             A39: c = da & c <> db;

            (s1 . da) = (s2 . da) & (s1 . db) = (s2 . db) by A2, SCMFSA_M: 2;

            

            hence (( Exec (i,s1)) . c) = ((s2 . da) div (s2 . db)) by A35, A39, SCMFSA_2: 67

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A35, A36, A39, SCMFSA_2: 67;

          end;

            suppose

             A40: c <> da & c <> db;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A35, SCMFSA_2: 67

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A35, A36, A40, SCMFSA_2: 67;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A35, SCMFSA_2: 67

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A35, A36, SCMFSA_2: 67;

        end;

        hence thesis by A37, SCMFSA_M: 2;

      end;

        suppose ( InsCode i) = 6;

        then

        consider loc be Nat such that

         A41: i = ( goto loc) by SCMFSA_2: 35;

        

         A42: ( IncAddr (i,n)) = ( goto (loc + n)) by A41, SCMFSA_4: 1;

         A43:

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A41, SCMFSA_2: 69

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A42, SCMFSA_2: 69;

        end;

        ( IC ( Exec (i,s1))) = loc by A41, SCMFSA_2: 69;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A42, SCMFSA_2: 69;

        now

          let c be Int-Location;

          

          thus (( Exec (i,s1)) . c) = (s1 . c) by A41, SCMFSA_2: 69

          .= (s2 . c) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . c) by A42, SCMFSA_2: 69;

        end;

        hence thesis by A43, SCMFSA_M: 2;

      end;

        suppose ( InsCode i) = 7;

        then

        consider loc be Nat, da be Int-Location such that

         A44: i = (da =0_goto loc) by SCMFSA_2: 36;

        

         A45: ( IncAddr (i,n)) = (da =0_goto (loc + n)) by A44, SCMFSA_4: 2;

         A46:

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A44, SCMFSA_2: 70

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A45, SCMFSA_2: 70;

        end;

        hereby

          per cases ;

            suppose (s1 . da) = 0 ;

            then (s2 . da) = 0 & ( IC ( Exec (i,s1))) = loc by A2, A44, SCMFSA_2: 70, SCMFSA_M: 2;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A45, SCMFSA_2: 70;

          end;

            suppose (s1 . da) <> 0 ;

            then (s2 . da) <> 0 & ( IC ( Exec (i,s1))) = (( IC s1) + 1) by A2, A44, SCMFSA_2: 70, SCMFSA_M: 2;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A3, A45, SCMFSA_2: 70;

          end;

        end;

        now

          let c be Int-Location;

          

          thus (( Exec (i,s1)) . c) = (s1 . c) by A44, SCMFSA_2: 70

          .= (s2 . c) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . c) by A45, SCMFSA_2: 70;

        end;

        hence thesis by A46, SCMFSA_M: 2;

      end;

        suppose ( InsCode i) = 8;

        then

        consider loc be Nat, da be Int-Location such that

         A47: i = (da >0_goto loc) by SCMFSA_2: 37;

        

         A48: ( IncAddr (i,n)) = (da >0_goto (loc + n)) by A47, SCMFSA_4: 3;

         A49:

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A47, SCMFSA_2: 71

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A48, SCMFSA_2: 71;

        end;

        hereby

          per cases ;

            suppose (s1 . da) > 0 ;

            then (s2 . da) > 0 & ( IC ( Exec (i,s1))) = loc by A2, A47, SCMFSA_2: 71, SCMFSA_M: 2;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A48, SCMFSA_2: 71;

          end;

            suppose (s1 . da) <= 0 ;

            then (s2 . da) <= 0 & ( IC ( Exec (i,s1))) = (( IC s1) + 1) by A2, A47, SCMFSA_2: 71, SCMFSA_M: 2;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A3, A48, SCMFSA_2: 71;

          end;

        end;

        now

          let c be Int-Location;

          

          thus (( Exec (i,s1)) . c) = (s1 . c) by A47, SCMFSA_2: 71

          .= (s2 . c) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . c) by A48, SCMFSA_2: 71;

        end;

        hence thesis by A49, SCMFSA_M: 2;

      end;

        suppose

         A50: ( InsCode i) = 9;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider db,da be Int-Location, f be FinSeq-Location such that

         A51: i = (da := (f,db)) by A50, SCMFSA_2: 38;

        

         A52: ( IncAddr (i,n)) = i by A51, COMPOS_0: 4;

         A53:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A54: c = da;

            then

            consider m be Nat such that

             A55: m = |.(s1 . db).| and

             A56: (( Exec ((da := (f,db)),s1)) . c) = ((s1 . f) /. m) by SCMFSA_2: 72;

            

             A57: (s1 . f) = (s2 . f) by A2, SCMFSA_M: 2;

            consider m2 be Nat such that

             A58: m2 = |.(s2 . db).| and

             A59: (( Exec ((da := (f,db)),s2)) . c) = ((s2 . f) /. m2) by A54, SCMFSA_2: 72;

            m = m2 by A2, A55, A58, SCMFSA_M: 2;

            hence (( Exec (i,s1)) . c) = (( Exec (( IncAddr (i,n)),s2)) . c) by A51, A56, A59, A57, COMPOS_0: 4;

          end;

            suppose

             A60: c <> da;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A51, SCMFSA_2: 72

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A51, A52, A60, SCMFSA_2: 72;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A51, SCMFSA_2: 72

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A51, A52, SCMFSA_2: 72;

        end;

        hence thesis by A53, SCMFSA_M: 2;

      end;

        suppose

         A61: ( InsCode i) = 10;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider db,da be Int-Location, f be FinSeq-Location such that

         A62: i = ((f,db) := da) by A61, SCMFSA_2: 39;

        

         A63: ( IncAddr (i,n)) = i by A62, COMPOS_0: 4;

         A64:

        now

          let g be FinSeq-Location;

          per cases ;

            suppose

             A65: g = f;

            

             A66: (s1 . da) = (s2 . da) & (s1 . f) = (s2 . f) by A2, SCMFSA_M: 2;

            consider m2 be Nat such that

             A67: m2 = |.(s2 . db).| and

             A68: (( Exec (((f,db) := da),s2)) . f) = ((s2 . f) +* (m2,(s2 . da))) by SCMFSA_2: 73;

            consider m1 be Nat such that

             A69: m1 = |.(s1 . db).| and

             A70: (( Exec (((f,db) := da),s1)) . f) = ((s1 . f) +* (m1,(s1 . da))) by SCMFSA_2: 73;

            m1 = m2 by A2, A69, A67, SCMFSA_M: 2;

            hence (( Exec (i,s1)) . g) = (( Exec (( IncAddr (i,n)),s2)) . g) by A62, A65, A70, A68, A66, COMPOS_0: 4;

          end;

            suppose

             A71: g <> f;

            

            hence (( Exec (i,s1)) . g) = (s1 . g) by A62, SCMFSA_2: 73

            .= (s2 . g) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . g) by A62, A63, A71, SCMFSA_2: 73;

          end;

        end;

        now

          let c be Int-Location;

          

          thus (( Exec (i,s1)) . c) = (s1 . c) by A62, SCMFSA_2: 73

          .= (s2 . c) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . c) by A62, A63, SCMFSA_2: 73;

        end;

        hence thesis by A64, SCMFSA_M: 2;

      end;

        suppose

         A72: ( InsCode i) = 11;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da be Int-Location, f be FinSeq-Location such that

         A73: i = (da :=len f) by A72, SCMFSA_2: 40;

        

         A74: ( IncAddr (i,n)) = i by A73, COMPOS_0: 4;

         A75:

        now

          let c be Int-Location;

          per cases ;

            suppose

             A76: c = da;

            

            hence (( Exec (i,s1)) . c) = ( len (s1 . f)) by A73, SCMFSA_2: 74

            .= ( len (s2 . f)) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A73, A74, A76, SCMFSA_2: 74;

          end;

            suppose

             A77: c <> da;

            

            hence (( Exec (i,s1)) . c) = (s1 . c) by A73, SCMFSA_2: 74

            .= (s2 . c) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . c) by A73, A74, A77, SCMFSA_2: 74;

          end;

        end;

        now

          let f be FinSeq-Location;

          

          thus (( Exec (i,s1)) . f) = (s1 . f) by A73, SCMFSA_2: 74

          .= (s2 . f) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . f) by A73, A74, SCMFSA_2: 74;

        end;

        hence thesis by A75, SCMFSA_M: 2;

      end;

        suppose

         A78: ( InsCode i) = 12;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (( IncAddr (i,n)),s2))) by A4;

        consider da be Int-Location, f be FinSeq-Location such that

         A79: i = (f :=<0,...,0> da) by A78, SCMFSA_2: 41;

        

         A80: ( IncAddr (i,n)) = i by A79, COMPOS_0: 4;

         A81:

        now

          let g be FinSeq-Location;

          per cases ;

            suppose

             A82: g = f;

            (ex m1 be Nat st m1 = |.(s1 . da).| & (( Exec ((f :=<0,...,0> da),s1)) . f) = (m1 |-> 0 )) & ex m2 be Nat st m2 = |.(s2 . da).| & (( Exec ((f :=<0,...,0> da),s2)) . f) = (m2 |-> 0 ) by SCMFSA_2: 75;

            hence (( Exec (i,s1)) . g) = (( Exec (( IncAddr (i,n)),s2)) . g) by A2, A79, A80, A82, SCMFSA_M: 2;

          end;

            suppose

             A83: g <> f;

            

            hence (( Exec (i,s1)) . g) = (s1 . g) by A79, SCMFSA_2: 75

            .= (s2 . g) by A2, SCMFSA_M: 2

            .= (( Exec (( IncAddr (i,n)),s2)) . g) by A79, A80, A83, SCMFSA_2: 75;

          end;

        end;

        now

          let c be Int-Location;

          

          thus (( Exec (i,s1)) . c) = (s1 . c) by A79, SCMFSA_2: 75

          .= (s2 . c) by A2, SCMFSA_M: 2

          .= (( Exec (( IncAddr (i,n)),s2)) . c) by A79, A80, SCMFSA_2: 75;

        end;

        hence thesis by A81, SCMFSA_M: 2;

      end;

    end;

    ::$Canceled

    begin

    definition

      ::$Canceled

      let I,J be Program of SCM+FSA ;

      :: SCMFSA6A:def3

      func I ";" J -> Program of SCM+FSA equals (( stop ( Directed I)) ';' J);

      coherence ;

    end

    registration

      let I be Program of SCM+FSA , J be halt-ending Program of SCM+FSA ;

      cluster (I ";" J) -> halt-ending;

      coherence ;

    end

    registration

      let P be preProgram of SCM+FSA ;

      cluster ( Directed P) -> halt-free;

      correctness by FUNCT_4: 100;

    end

    registration

      cluster halt-free for Program of SCM+FSA ;

      existence

      proof

        take ( Directed the Program of SCM+FSA );

        thus thesis;

      end;

    end

    registration

      let I be Program of SCM+FSA , J be unique-halt Program of SCM+FSA ;

      cluster (I ";" J) -> unique-halt;

      coherence ;

    end

    

     Lm1: for I be preProgram of SCM+FSA holds ( card ( Directed I)) = ( card I)

    proof

      let I be preProgram of SCM+FSA ;

      

      thus ( card ( Directed I)) = ( card ( dom ( Directed I))) by CARD_1: 62

      .= ( card ( dom I)) by FUNCT_4: 99

      .= ( card I) by CARD_1: 62;

    end;

    

     Lm2: for I be Program of SCM+FSA holds ( card ( stop ( Directed I))) = ( card ( stop I))

    proof

      let I be Program of SCM+FSA ;

      

      thus ( card ( stop ( Directed I))) = (( card ( Directed I)) + 1) by COMPOS_1: 72

      .= (( card I) + 1) by Lm1

      .= ( card ( stop I)) by COMPOS_1: 72;

    end;

    theorem :: SCMFSA6A:15

    

     Th5: for I,J be Program of SCM+FSA , l be Nat st l in ( dom I) & (I . l) <> ( halt SCM+FSA ) holds ((I ";" J) . l) = (I . l)

    proof

      let I,J be Program of SCM+FSA , l be Nat such that

       A1: l in ( dom I) and

       A2: (I . l) <> ( halt SCM+FSA );

      ( Reloc (J,( card I))) = ( IncAddr (( Shift (J,( card I))),( card I))) by COMPOS_1: 34;

      then

       A3: ( dom ( Reloc (J,( card I)))) = ( dom ( Shift (J,( card I)))) by COMPOS_1:def 21;

      

       A4: (( card ( stop I)) -' 1) = ( card I) by COMPOS_1: 71;

      

       A5: ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

      now

        assume l in ( dom ( Reloc (J,( card I))));

        then l in { (m + ( card I)) where m be Nat : m in ( dom J) } by A3, VALUED_1:def 12;

        then

        consider m be Nat such that

         A6: l = (m + ( card I)) and m in ( dom J);

        (m + ( card I)) < ( card I) by A1, A6, AFINSQ_1: 66;

        hence contradiction by NAT_1: 11;

      end;

      

      hence ((I ";" J) . l) = (( Directed I) . l) by FUNCT_4: 11, A4, A5

      .= (I . l) by A2, FUNCT_4: 105;

    end;

    theorem :: SCMFSA6A:16

    for I,J be Program of SCM+FSA holds ( Directed I) c= (I ";" J)

    proof

      let I,J be Program of SCM+FSA ;

      

       A1: (( card ( stop I)) -' 1) = ( card I) by COMPOS_1: 71;

      

       A2: ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

       A3:

      now

        let x be object;

        assume x in ( dom ( Directed I));

        then

         A4: x in ( dom I) by FUNCT_4: 99;

        ( dom I) misses ( dom ( Reloc (J,( card I)))) by COMPOS_1: 48;

        then not x in ( dom ( Reloc (J,( card I)))) by A4, XBOOLE_0: 3;

        hence (( Directed I) . x) = ((I ";" J) . x) by FUNCT_4: 11, A1, A2;

      end;

      ( dom (I ";" J)) = (( dom ( Directed I)) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4:def 1, A1, A2;

      then ( dom ( Directed I)) c= ( dom (I ";" J)) by XBOOLE_1: 7;

      hence thesis by A3, GRFUNC_1: 2;

    end;

    theorem :: SCMFSA6A:17

    

     Th7: for I,J be Program of SCM+FSA holds ( dom I) c= ( dom (I ";" J))

    proof

      let I,J be Program of SCM+FSA ;

      

       A1: (( card ( stop I)) -' 1) = ( card I) by COMPOS_1: 71;

      ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

      

      then ( dom (I ";" J)) = (( dom ( Directed I)) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4:def 1, A1

      .= (( dom I) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4: 99;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: SCMFSA6A:18

    for I,J be Program of SCM+FSA holds (I +* (I ";" J)) = (I ";" J)

    proof

      let I,J be Program of SCM+FSA ;

      

       A1: for x be object st x in ( dom (I ";" J)) holds ((I +* (I ";" J)) . x) = ((I ";" J) . x) by FUNCT_4: 13;

      ( dom (I +* (I ";" J))) = (( dom I) \/ ( dom (I ";" J))) by FUNCT_4:def 1

      .= ( dom (I ";" J)) by Th7, XBOOLE_1: 12;

      hence thesis by A1, FUNCT_1: 2;

    end;

    begin

    definition

      let i, J;

      :: SCMFSA6A:def4

      func i ";" J -> Program of SCM+FSA equals (( Macro i) ";" J);

      correctness ;

    end

    definition

      let I, j;

      :: SCMFSA6A:def5

      func I ";" j -> Program of SCM+FSA equals (I ";" ( Macro j));

      correctness ;

    end

    definition

      let i, j;

      :: SCMFSA6A:def6

      func i ";" j -> Program of SCM+FSA equals (( Macro i) ";" ( Macro j));

      correctness ;

    end

    registration

      cluster sequential for Instruction of SCM+FSA ;

      existence

      proof

        take (( intloc 0 ) := ( intloc 0 ));

        thus thesis;

      end;

    end

    registration

      cluster sequential -> No-StopCode for Instruction of SCM+FSA ;

      coherence

      proof

        let i be Instruction of SCM+FSA such that

         A1: i is sequential;

        reconsider i as Element of the InstructionsF of SCM+FSA ;

        i <> ( halt SCM+FSA ) by A1;

        then i is No-StopCode by COMPOS_0:def 12;

        hence thesis;

      end;

    end

    registration

      let i,j be sequential Instruction of SCM+FSA ;

      cluster (i ";" j) -> halt-ending unique-halt;

      coherence ;

    end

    registration

      let I be MacroInstruction of SCM+FSA , j be sequential Instruction of SCM+FSA ;

      cluster (I ";" j) -> halt-ending unique-halt;

      coherence ;

    end

    registration

      let i be sequential Instruction of SCM+FSA , J be MacroInstruction of SCM+FSA ;

      cluster (i ";" J) -> halt-ending unique-halt;

      coherence ;

    end

    theorem :: SCMFSA6A:19

    (i ";" j) = (( Macro i) ";" j);

    theorem :: SCMFSA6A:20

    (i ";" j) = (i ";" ( Macro j));

    theorem :: SCMFSA6A:21

    

     Th11: ( card (I ";" J)) = (( card I) + ( card J))

    proof

      

       A1: ( card ( dom (I ";" J))) = ( card (I ";" J)) & ( card ( dom I)) = ( card I);

      

       A2: ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

      (( card ( stop I)) -' 1) = ( card I) by COMPOS_1: 71;

      

      then

       A3: ( dom (I ";" J)) = (( dom ( Directed I)) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4:def 1, A2

      .= (( dom I) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4: 99;

      ( card ( dom ( Reloc (J,( card I))))) = ( card ( Reloc (J,( card I)))) by CARD_1: 62

      .= ( card J) by COMPOS_1: 49

      .= ( card ( dom J));

      hence thesis by A1, A3, CARD_2: 40, COMPOS_1: 48;

    end;

    theorem :: SCMFSA6A:22

    for I be preProgram of SCM+FSA holds I is halt-free implies ( Directed I) = I by FUNCT_4: 103;

    theorem :: SCMFSA6A:23

    

     Th13: for I be preProgram of SCM+FSA , k be Element of NAT holds ( Reloc (( Directed I),k)) = (( Reloc (I,k)) +~ (( halt SCM+FSA ),( goto (( card I) + k))))

    proof

      let I be preProgram of SCM+FSA ;

      let k be Element of NAT ;

      

       A1: ( dom ( Reloc (I,k))) = { (m + k) where m be Nat : m in ( dom I) } by COMPOS_1: 33;

      

       A2: ( dom ( Directed I)) = ( dom I) by FUNCT_4: 99;

      

       A3: ( dom ( Reloc (( Directed I),k))) = { (m + k) where m be Nat : m in ( dom I) } by A2, COMPOS_1: 33;

       A4:

      now

        let x be object;

        assume

         A5: x in { (m + k) where m be Nat : m in ( dom I) };

        then

        consider n be Nat such that

         A6: x = (n + k) and

         A7: n in ( dom I);

        ( dom ( Directed I)) = ( dom I) by FUNCT_4: 99;

        then

        reconsider i = (( Directed I) . n) as Instruction of SCM+FSA by A7, FUNCT_1: 106;

        reconsider i0 = (I . n) as Instruction of SCM+FSA by A7, FUNCT_1: 106;

         A8:

        now

          per cases ;

            suppose

             A9: i0 = ( halt SCM+FSA );

            then

             A10: i = ( goto ( card I)) by A7, FUNCT_4: 106;

            

             A11: (( Reloc (I,k)) . x) = ( IncAddr (i0,k)) by A6, A7, COMPOS_1: 35

            .= ( halt SCM+FSA ) by A9, COMPOS_0: 4;

            then (( Reloc (I,k)) . x) in {( halt SCM+FSA )} by TARSKI:def 1;

            then (( Reloc (I,k)) . x) in ( dom (( halt SCM+FSA ) .--> ( goto (( card I) + k))));

            then x in ( dom ((( halt SCM+FSA ) .--> ( goto (( card I) + k))) * ( Reloc (I,k)))) by A1, A5, FUNCT_1: 11;

            

            hence ((( Reloc (I,k)) +~ (( halt SCM+FSA ),( goto (( card I) + k)))) . x) = (((( halt SCM+FSA ) .--> ( goto (( card I) + k))) * ( Reloc (I,k))) . x) by FUNCT_4: 13

            .= ((( halt SCM+FSA ) .--> ( goto (( card I) + k))) . (( Reloc (I,k)) . x)) by A1, A5, FUNCT_1: 13

            .= ( goto (( card I) + k)) by A11, FUNCOP_1: 72

            .= ( IncAddr (i,k)) by A10, SCMFSA_4: 1;

          end;

            suppose

             A12: i0 <> ( halt SCM+FSA );

            

             A13: (( Reloc (I,k)) . x) = ( IncAddr (i0,k)) by A6, A7, COMPOS_1: 35;

            

             A14: ( InsCode ( halt SCM+FSA )) = 0 by COMPOS_1: 70;

            ( InsCode i0) <> 0 by A12, SCMFSA_2: 95;

            then ( IncAddr (i0,k)) <> ( halt SCM+FSA ) by A14, COMPOS_0:def 9;

            then not (( Reloc (I,k)) . x) in {( halt SCM+FSA )} by A13, TARSKI:def 1;

            then not (( Reloc (I,k)) . x) in ( dom (( halt SCM+FSA ) .--> ( goto (( card I) + k))));

            then not x in ( dom ((( halt SCM+FSA ) .--> ( goto (( card I) + k))) * ( Reloc (I,k)))) by FUNCT_1: 11;

            

            hence ((( Reloc (I,k)) +~ (( halt SCM+FSA ),( goto (( card I) + k)))) . x) = (( Reloc (I,k)) . x) by FUNCT_4: 11

            .= ( IncAddr (i,k)) by A12, A13, FUNCT_4: 105;

          end;

        end;

        thus (( Reloc (( Directed I),k)) . x) = ((( Reloc (I,k)) +~ (( halt SCM+FSA ),( goto (( card I) + k)))) . x) by A8, A2, A6, A7, COMPOS_1: 35;

      end;

      ( dom (( Reloc (I,k)) +~ (( halt SCM+FSA ),( goto (( card I) + k))))) = { (m + k) where m be Nat : m in ( dom I) } by A1, FUNCT_4: 99;

      hence thesis by A3, A4, FUNCT_1: 2;

    end;

    theorem :: SCMFSA6A:24

    

     Th14: for I,J be Program of SCM+FSA holds ( Directed (I ";" J)) = (I ";" ( Directed J))

    proof

      let I,J be Program of SCM+FSA ;

      

       A1: (( card ( stop I)) -' 1) = ( card I) by COMPOS_1: 71;

      

       A2: ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

      

      hence (I ";" ( Directed J)) = (( Directed I) +* (( Reloc (J,( card I))) +~ (( halt SCM+FSA ),( goto (( card J) + ( card I)))))) by Th13, A1

      .= (( Directed I) +* (( Reloc (J,( card I))) +~ (( halt SCM+FSA ),( goto ( card (I ";" J)))))) by Th11

      .= ((( Directed I) +~ (( halt SCM+FSA ),( goto ( card (I ";" J))))) +* (( Reloc (J,( card I))) +~ (( halt SCM+FSA ),( goto ( card (I ";" J)))))) by FUNCT_4: 127

      .= ( Directed (I ";" J)) by FUNCT_7: 117, A1, A2;

    end;

    theorem :: SCMFSA6A:25

    

     Th15: ((I ";" J) ";" K) = (I ";" (J ";" K))

    proof

      

       A1: (( card ( stop I)) -' 1) = ( card I) by COMPOS_1: 71;

      

       A2: ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

      

       A3: ( card ( stop ( Directed (I ";" J)))) = ( card ( stop (I ";" J))) by Lm2;

      

       A4: (( card ( stop (I ";" J))) -' 1) = ( card (I ";" J)) by COMPOS_1: 71;

      

       A5: ( card ( stop ( Directed J))) = ( card ( stop J)) by Lm2;

      (( card ( stop J)) -' 1) = ( card J) by COMPOS_1: 71;

      

      then

       A6: ( Reloc ((J ";" K),( card I))) = (( Reloc (( Directed J),( card I))) +* ( Reloc (( Reloc (K,( card J))),( card I)))) by COMPOS_1: 42, A5

      .= (( Reloc (( Directed J),( card I))) +* ( Reloc (K,(( card J) + ( card I))))) by COMPOS_1: 43;

      

      thus ((I ";" J) ";" K) = ((I ";" ( Directed J)) +* ( Reloc (K,( card (I ";" J))))) by Th14, A4, A3

      .= (( Directed I) +* (( Reloc (( Directed J),( card I))) +* ( Reloc (K,( card (I ";" J)))))) by FUNCT_4: 14, A1, A2

      .= (I ";" (J ";" K)) by A6, Th11, A1, A2;

    end;

    theorem :: SCMFSA6A:26

    ((I ";" J) ";" k) = (I ";" (J ";" k)) by Th15;

    theorem :: SCMFSA6A:27

    ((I ";" j) ";" K) = (I ";" (j ";" K)) by Th15;

    theorem :: SCMFSA6A:28

    ((I ";" j) ";" k) = (I ";" (j ";" k)) by Th15;

    theorem :: SCMFSA6A:29

    ((i ";" J) ";" K) = (i ";" (J ";" K)) by Th15;

    theorem :: SCMFSA6A:30

    ((i ";" J) ";" k) = (i ";" (J ";" k)) by Th15;

    theorem :: SCMFSA6A:31

    ((i ";" j) ";" K) = (i ";" (j ";" K)) by Th15;

    theorem :: SCMFSA6A:32

    ((i ";" j) ";" k) = (i ";" (j ";" k)) by Th15;

    theorem :: SCMFSA6A:33

    ( card (i ";" J)) = (( card J) + 2)

    proof

      

      thus ( card (i ";" J)) = (( card ( Macro i)) + ( card J)) by Th11

      .= (( card J) + 2) by COMPOS_1: 56;

    end;

    theorem :: SCMFSA6A:34

    ( card (I ";" j)) = (( card I) + 2)

    proof

      

      thus ( card (I ";" j)) = (( card ( Macro j)) + ( card I)) by Th11

      .= (( card I) + 2) by COMPOS_1: 56;

    end;

    theorem :: SCMFSA6A:35

    ( card (i ";" j)) = 4

    proof

      

      thus ( card (i ";" j)) = (( card ( Macro i)) + ( card ( Macro j))) by Th11

      .= (( card ( Macro i)) + 2) by COMPOS_1: 56

      .= (2 + 2) by COMPOS_1: 56

      .= 4;

    end;

    theorem :: SCMFSA6A:36

    for I be preProgram of SCM+FSA holds ( card ( Directed I)) = ( card I) by Lm1;

    theorem :: SCMFSA6A:37

    

     Th27: for I be Program of SCM+FSA holds ( card ( stop ( Directed I))) = ( card ( stop I)) by Lm2;

    theorem :: SCMFSA6A:38

    ( Reloc (J,( card I))) c= (I ";" J)

    proof

      (I ";" J) = (( CutLastLoc ( stop ( Directed I))) +* ( Reloc (J,(( card ( stop I)) -' 1)))) by Th27

      .= (( CutLastLoc ( stop ( Directed I))) +* ( Reloc (J,( card I)))) by COMPOS_1: 71;

      hence thesis by FUNCT_4: 25;

    end;

    theorem :: SCMFSA6A:39

    ( dom (I ";" J)) = (( dom I) \/ ( dom ( Reloc (J,( card I)))))

    proof

      (I ";" J) = (( CutLastLoc ( stop ( Directed I))) +* ( Reloc (J,(( card ( stop I)) -' 1)))) by Th27

      .= (( Directed I) +* ( Reloc (J,( card I)))) by COMPOS_1: 71;

      

      hence ( dom (I ";" J)) = (( dom ( Directed I)) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4:def 1

      .= (( dom I) \/ ( dom ( Reloc (J,( card I))))) by FUNCT_4: 99;

    end;

    theorem :: SCMFSA6A:40

    n in ( dom ( Reloc (J,( card I)))) implies ((I ";" J) . n) = (( Reloc (J,( card I))) . n)

    proof

      assume

       A1: n in ( dom ( Reloc (J,( card I))));

      (I ";" J) = (( CutLastLoc ( stop ( Directed I))) +* ( Reloc (J,(( card ( stop I)) -' 1)))) by Th27

      .= (( Directed I) +* ( Reloc (J,( card I)))) by COMPOS_1: 71;

      hence ((I ";" J) . n) = (( Reloc (J,( card I))) . n) by A1, FUNCT_4: 13;

    end;

    begin

    registration

      let I be really-closed Program of SCM+FSA ;

      cluster ( stop ( Directed I)) -> really-closed;

      coherence

      proof

        set F = ( stop ( Directed I));

        let l be Nat such that

         A1: l in ( dom F);

        

         A2: ( card ( Directed I)) = ( card I) by FUNCT_4: 99;

        then

         A3: ( dom F) = (( dom I) \/ {( card I)}) by AFINSQ_1: 89;

        

         A4: ( dom ( Directed I)) = ( dom I) by FUNCT_4: 99;

        per cases ;

          suppose l = ( card I);

          

          then (F /. l) = (F . ( card ( Directed I))) by A2, A1, PARTFUN1:def 6

          .= ( halt SCM+FSA ) by COMPOS_1: 64;

          then ( NIC ((F /. l),l)) = {l} by AMISTD_1: 2;

          hence ( NIC ((F /. l),l)) c= ( dom F) by A1, ZFMISC_1: 31;

        end;

          suppose l <> ( card I);

          then not l in {( card I)} by TARSKI:def 1;

          then

           A5: l in ( dom I) by A3, A1, XBOOLE_0:def 3;

          

           A6: (F /. l) = (F . l) by PARTFUN1:def 6, A1

          .= (( Directed I) . l) by A4, A5, AFINSQ_1:def 3;

          

           A7: ( dom I) c= ( dom F) by A3, XBOOLE_1: 7;

          ( card I) in {( card I)} by TARSKI:def 1;

          then

           A8: ( card I) in ( dom F) by A3, XBOOLE_0:def 3;

          per cases ;

            suppose (I . l) = ( halt SCM+FSA );

            then (( Directed I) . l) = ( goto ( card I)) by A5, FUNCT_4: 106;

            then (F /. l) = ( goto ( card I)) by A6;

            then ( NIC ((F /. l),l)) = {( card I)} by SCMFSA10: 33;

            hence ( NIC ((F /. l),l)) c= ( dom F) by ZFMISC_1: 31, A8;

          end;

            suppose (I . l) <> ( halt SCM+FSA );

            

            then

             A9: (( Directed I) . l) = (I . l) by FUNCT_4: 105

            .= (I /. l) by A5, PARTFUN1:def 6;

            ( NIC ((I /. l),l)) c= ( dom I) by A5, AMISTD_1:def 9;

            then ( NIC ((I /. l),l)) c= ( dom F) by A7, XBOOLE_1: 1;

            hence ( NIC ((F /. l),l)) c= ( dom F) by A6, A9;

          end;

        end;

      end;

    end

    registration

      let I,J be really-closed Program of SCM+FSA ;

      cluster (I ";" J) -> really-closed;

      coherence ;

    end

    theorem :: SCMFSA6A:41

    for I,J be MacroInstruction of SCM+FSA , n be Nat st n < ( LastLoc I) holds ((I ";" J) . n) = (I . n)

    proof

      let I,J be MacroInstruction of SCM+FSA , l be Nat such that

       A1: l < ( LastLoc I);

      ( LastLoc I) in ( dom I) by VALUED_1: 30;

      then

       A2: l in ( dom I) by A1, AFINSQ_1:def 12;

      then (I . l) <> ( halt SCM+FSA ) by A1, COMPOS_1:def 15;

      hence thesis by A2, Th5;

    end;