scmfsa6c.miz



    begin

    reserve x for set,

i for Instruction of SCM+FSA ,

a,b for Int-Location,

f for FinSeq-Location,

l,l1 for Nat,

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

P,P1,P2 for Instruction-Sequence of SCM+FSA ;

    set SA0 = ( Start-At ( 0 , SCM+FSA ));

    theorem :: SCMFSA6C:1

    for I be keeping_0 parahalting really-closed Program of SCM+FSA , J be parahalting really-closed Program of SCM+FSA holds (( IExec ((I ";" J),P,s)) . a) = (( IExec (J,P,( IExec (I,P,s)))) . a)

    proof

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

      

       A1: not a in ( dom ( Start-At ((( IC ( IExec (J,P,( IExec (I,P,s))))) + ( card I)), SCM+FSA ))) by SCMFSA_2: 102;

      ( IExec ((I ";" J),P,s)) = ( IncIC (( IExec (J,P,( IExec (I,P,s)))),( card I))) by SCMFSA6B: 20;

      hence thesis by A1, FUNCT_4: 11;

    end;

    theorem :: SCMFSA6C:2

    for I be keeping_0 parahalting really-closed Program of SCM+FSA , J be parahalting really-closed Program of SCM+FSA holds (( IExec ((I ";" J),P,s)) . f) = (( IExec (J,P,( IExec (I,P,s)))) . f)

    proof

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

      

       A1: not f in ( dom ( Start-At ((( IC ( IExec (J,P,( IExec (I,P,s))))) + ( card I)), SCM+FSA ))) by SCMFSA_2: 103;

      ( IExec ((I ";" J),P,s)) = ( IncIC (( IExec (J,P,( IExec (I,P,s)))),( card I))) by SCMFSA6B: 20;

      hence thesis by A1, FUNCT_4: 11;

    end;

    begin

    ::$Canceled

    definition

      let i be Instruction of SCM+FSA ;

      :: SCMFSA6C:def1

      attr i is keeping_0 means

      : Def1: ( Macro i) is keeping_0;

    end

    

     Lm1: ( Macro ( halt SCM+FSA )) is keeping_0

    proof

      set Mi = ( Macro ( halt SCM+FSA ));

      let s be 0 -started State of SCM+FSA ;

      

       A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

      let P be Instruction-Sequence of SCM+FSA ;

      assume

       A2: Mi c= P;

      let k be Nat;

      

       A3: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

      

       A4: 0 in ( dom Mi) by COMPOS_1: 60;

      ( CurInstr (P,( Comput (P,s, 0 )))) = (P . 0 ) by A1, A3, MEMSTR_0: 39

      .= (Mi . 0 ) by A2, A4, GRFUNC_1: 2

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

      hence (( Comput (P,s,k)) . ( intloc 0 )) = (s . ( intloc 0 )) by EXTPRO_1: 5, NAT_1: 2;

    end;

    registration

      cluster ( halt SCM+FSA ) -> keeping_0;

      coherence by Lm1;

    end

    registration

      let i be sequential Instruction of SCM+FSA ;

      cluster ( Macro i) -> parahalting;

      coherence

      proof

        let s be 0 -started State of SCM+FSA ;

        let P be Instruction-Sequence of SCM+FSA such that

         A1: ( Macro i) c= P;

        ( dom P) = NAT by PARTFUN1:def 2;

        then

         A2: 0 in ( dom P);

        

         A3: 0 in ( dom ( Macro i)) & 1 in ( dom ( Macro i)) by COMPOS_1: 57;

        

         A4: ( IC s) = 0 by MEMSTR_0:def 11;

        

         A5: (P . 0 ) = (( Macro i) . 0 ) by A1, GRFUNC_1: 2, A3

        .= i by COMPOS_1: 58;

        ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec (i,s)) by A5, A2, A4, PARTFUN1:def 6;

        then

         A6: ( IC ( Comput (P,s,1))) = ( 0 + 1) by AMISTD_1:def 8, A4;

        then (( Macro i) . ( IC ( Comput (P,s,1)))) = ( halt SCM+FSA ) by COMPOS_1: 59;

        then (P . ( IC ( Comput (P,s,1)))) = ( halt SCM+FSA ) by A3, A1, GRFUNC_1: 2, A6;

        hence P halts_on s by EXTPRO_1: 30;

      end;

    end

    registration

      let a,b be Int-Location;

      let f be FinSeq-Location;

      cluster ((f,a) := b) -> keeping_0;

      coherence

      proof

        thus ((f,a) := b) is keeping_0

        proof

          set Ma = ( Macro ((f,a) := b));

          let s be 0 -started State of SCM+FSA ;

          

           A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

          let P be Instruction-Sequence of SCM+FSA ;

          assume

           A2: Ma c= P;

          let k be Nat;

          

           A3: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

          

           A4: ( IC s) = (SA0 . ( IC SCM+FSA )) by A3, A1, GRFUNC_1: 2

          .= 0 by FUNCOP_1: 72;

           0 in ( dom Ma) by COMPOS_1: 60;

          then

           A5: (Ma . 0 ) = (P . 0 ) by A2, GRFUNC_1: 2;

          

           A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

          

           A7: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

          .= ( Exec (((f,a) := b),s)) by A4, A5, A6, COMPOS_1: 58;

          1 in ( dom Ma) by COMPOS_1: 60;

          then (Ma . 1) = (P . 1) by A2, GRFUNC_1: 2;

          then

           A8: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

          ( IC ( Exec (((f,a) := b),s))) = ( 0 + 1) by A4, SCMFSA_2: 73;

          then

           A9: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A8, A7, PBOOLE: 143;

          per cases by NAT_1: 14;

            suppose k = 0 ;

            hence thesis;

          end;

            suppose

             A10: 1 <= k;

            (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A7, SCMFSA_2: 73;

            hence thesis by A9, A10, EXTPRO_1: 5;

          end;

        end;

      end;

    end

    registration

      let a be Int-Location, f be FinSeq-Location;

      cluster (f :=<0,...,0> a) -> keeping_0;

      coherence

      proof

        thus (f :=<0,...,0> a) is keeping_0

        proof

          set Ma = ( Macro (f :=<0,...,0> a));

          let s be 0 -started State of SCM+FSA ;

          

           A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

          let P be Instruction-Sequence of SCM+FSA ;

          assume

           A2: Ma c= P;

          let k be Nat;

          

           A3: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

          

           A4: ( IC s) = (SA0 . ( IC SCM+FSA )) by A3, A1, GRFUNC_1: 2

          .= 0 by FUNCOP_1: 72;

           0 in ( dom Ma) by COMPOS_1: 60;

          then

           A5: (Ma . 0 ) = (P . 0 ) by A2, GRFUNC_1: 2;

          

           A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

          

           A7: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

          .= ( Exec ((f :=<0,...,0> a),s)) by A4, A5, A6, COMPOS_1: 58;

          1 in ( dom Ma) by COMPOS_1: 60;

          then (Ma . 1) = (P . 1) by A2, GRFUNC_1: 2;

          then

           A8: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

          ( IC ( Exec ((f :=<0,...,0> a),s))) = ( 0 + 1) by A4, SCMFSA_2: 75;

          then

           A9: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A8, A7, PBOOLE: 143;

          per cases by NAT_1: 14;

            suppose k = 0 ;

            hence thesis;

          end;

            suppose

             A10: 1 <= k;

            (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A7, SCMFSA_2: 75;

            hence thesis by A9, A10, EXTPRO_1: 5;

          end;

        end;

      end;

    end

    registration

      let a be read-write Int-Location, b be Int-Location;

      cluster (a := b) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro (a := b));

        let s be 0 -started State of SCM+FSA ;

        

         A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A2: Ma c= P;

        let k be Nat;

        

         A3: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A4: ( IC s) = (SA0 . ( IC SCM+FSA )) by A3, A1, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A5: (Ma . 0 ) = (P . 0 ) by A2, GRFUNC_1: 2;

        

         A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A7: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec ((a := b),s)) by A4, A5, A6, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A2, GRFUNC_1: 2;

        then

         A8: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec ((a := b),s))) = ( 0 + 1) by A4, SCMFSA_2: 63;

        then

         A9: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A8, A7, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A10: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A7, SCMFSA_2: 63;

          hence thesis by A9, A10, EXTPRO_1: 5;

        end;

      end;

      cluster ( AddTo (a,b)) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro ( AddTo (a,b)));

        let s be 0 -started State of SCM+FSA ;

        

         A11: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A12: Ma c= P;

        let k be Nat;

        

         A13: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A14: ( IC s) = (SA0 . ( IC SCM+FSA )) by A13, A11, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A15: (Ma . 0 ) = (P . 0 ) by A12, GRFUNC_1: 2;

        

         A16: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A17: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec (( AddTo (a,b)),s)) by A14, A15, A16, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A12, GRFUNC_1: 2;

        then

         A18: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec (( AddTo (a,b)),s))) = ( 0 + 1) by A14, SCMFSA_2: 64;

        then

         A19: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A18, A17, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A20: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A17, SCMFSA_2: 64;

          hence thesis by A19, A20, EXTPRO_1: 5;

        end;

      end;

      cluster ( SubFrom (a,b)) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro ( SubFrom (a,b)));

        let s be 0 -started State of SCM+FSA ;

        

         A21: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A22: Ma c= P;

        let k be Nat;

        

         A23: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A24: ( IC s) = (SA0 . ( IC SCM+FSA )) by A23, A21, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A25: (Ma . 0 ) = (P . 0 ) by A22, GRFUNC_1: 2;

        

         A26: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A27: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec (( SubFrom (a,b)),s)) by A24, A25, A26, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A22, GRFUNC_1: 2;

        then

         A28: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec (( SubFrom (a,b)),s))) = ( 0 + 1) by A24, SCMFSA_2: 65;

        then

         A29: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A28, A27, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A30: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A27, SCMFSA_2: 65;

          hence thesis by A29, A30, EXTPRO_1: 5;

        end;

      end;

      cluster ( MultBy (a,b)) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro ( MultBy (a,b)));

        let s be 0 -started State of SCM+FSA ;

        

         A31: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A32: Ma c= P;

        let k be Nat;

        

         A33: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A34: ( IC s) = (SA0 . ( IC SCM+FSA )) by A33, A31, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A35: (Ma . 0 ) = (P . 0 ) by A32, GRFUNC_1: 2;

        

         A36: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A37: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec (( MultBy (a,b)),s)) by A34, A35, A36, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A32, GRFUNC_1: 2;

        then

         A38: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec (( MultBy (a,b)),s))) = ( 0 + 1) by A34, SCMFSA_2: 66;

        then

         A39: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A38, A37, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A40: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A37, SCMFSA_2: 66;

          hence thesis by A39, A40, EXTPRO_1: 5;

        end;

      end;

    end

    registration

      cluster keeping_0 sequential for Instruction of SCM+FSA ;

      existence

      proof

        take i = ( the read-write Int-Location := ( intloc 1));

        thus i is keeping_0;

        thus thesis;

      end;

    end

    registration

      let i be keeping_0 Instruction of SCM+FSA ;

      cluster ( Macro i) -> keeping_0;

      coherence by Def1;

    end

    registration

      let a,b be read-write Int-Location;

      cluster ( Divide (a,b)) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro ( Divide (a,b)));

        let s be 0 -started State of SCM+FSA ;

        

         A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A2: Ma c= P;

        let k be Nat;

        

         A3: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A4: ( IC s) = (SA0 . ( IC SCM+FSA )) by A3, A1, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A5: (Ma . 0 ) = (P . 0 ) by A2, GRFUNC_1: 2;

        

         A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A7: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec (( Divide (a,b)),s)) by A4, A5, A6, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A2, GRFUNC_1: 2;

        then

         A8: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec (( Divide (a,b)),s))) = ( 0 + 1) by A4, SCMFSA_2: 67;

        then

         A9: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A8, A7, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A10: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A7, SCMFSA_2: 67;

          hence thesis by A9, A10, EXTPRO_1: 5;

        end;

      end;

    end

    registration

      let a be Int-Location, f be FinSeq-Location, b be read-write Int-Location;

      cluster (b := (f,a)) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro (b := (f,a)));

        let s be 0 -started State of SCM+FSA ;

        

         A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A2: Ma c= P;

        let k be Nat;

        

         A3: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A4: ( IC s) = (SA0 . ( IC SCM+FSA )) by A3, A1, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A5: (Ma . 0 ) = (P . 0 ) by A2, GRFUNC_1: 2;

        

         A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A7: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec ((b := (f,a)),s)) by A4, A5, A6, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A2, GRFUNC_1: 2;

        then

         A8: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec ((b := (f,a)),s))) = ( 0 + 1) by A4, SCMFSA_2: 72;

        then

         A9: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A8, A7, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A10: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A7, SCMFSA_2: 72;

          hence thesis by A9, A10, EXTPRO_1: 5;

        end;

      end;

    end

    registration

      let f be FinSeq-Location, b be read-write Int-Location;

      cluster (b :=len f) -> keeping_0;

      coherence

      proof

        set Ma = ( Macro (b :=len f));

        let s be 0 -started State of SCM+FSA ;

        

         A1: ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        let P be Instruction-Sequence of SCM+FSA ;

        assume

         A2: Ma c= P;

        let k be Nat;

        

         A3: ( IC SCM+FSA ) in ( dom SA0) by TARSKI:def 1;

        

         A4: ( IC s) = (SA0 . ( IC SCM+FSA )) by A3, A1, GRFUNC_1: 2

        .= 0 by FUNCOP_1: 72;

         0 in ( dom Ma) by COMPOS_1: 60;

        then

         A5: (Ma . 0 ) = (P . 0 ) by A2, GRFUNC_1: 2;

        

         A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A7: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Exec ((b :=len f),s)) by A4, A5, A6, COMPOS_1: 58;

        1 in ( dom Ma) by COMPOS_1: 60;

        then (Ma . 1) = (P . 1) by A2, GRFUNC_1: 2;

        then

         A8: (P . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        ( IC ( Exec ((b :=len f),s))) = ( 0 + 1) by A4, SCMFSA_2: 74;

        then

         A9: ( CurInstr (P,( Comput (P,s,1)))) = ( halt SCM+FSA ) by A8, A7, PBOOLE: 143;

        per cases by NAT_1: 14;

          suppose k = 0 ;

          hence thesis;

        end;

          suppose

           A10: 1 <= k;

          (( Comput (P,s,1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A7, SCMFSA_2: 74;

          hence thesis by A9, A10, EXTPRO_1: 5;

        end;

      end;

    end

    registration

      let i be sequential Instruction of SCM+FSA ;

      cluster ( Macro i) -> really-closed;

      coherence

      proof

        set F = ( Macro i);

        let l be Nat;

        

         A1: ( dom F) = { 0 , 1} by COMPOS_1: 61;

        assume

         A2: l in ( dom F);

        per cases by COMPOS_1: 60;

          suppose

           A3: l = 0 ;

          

          then (F /. l) = (F . 0 ) by A2, PARTFUN1:def 6

          .= i by COMPOS_1: 58;

          then ( NIC ((F /. l),l)) = {( 0 + 1)} by A3, AMISTD_1: 12;

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

        end;

          suppose

           A4: l = 1;

          

          then (F /. l) = (F . 1) by A2, PARTFUN1:def 6

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

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

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

        end;

      end;

    end

    registration

      let i be sequential Instruction of SCM+FSA , J be parahalting really-closed Program of SCM+FSA ;

      cluster (i ";" J) -> parahalting really-closed;

      coherence ;

    end

    registration

      let I be parahalting really-closed Program of SCM+FSA , j be sequential Instruction of SCM+FSA ;

      cluster (I ";" j) -> parahalting really-closed;

      coherence ;

    end

    registration

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

      cluster (i ";" j) -> parahalting really-closed;

      coherence ;

    end

    registration

      let i be keeping_0 sequential Instruction of SCM+FSA , J be keeping_0 really-closed Program of SCM+FSA ;

      cluster (i ";" J) -> keeping_0;

      coherence ;

    end

    registration

      let I be keeping_0 really-closed Program of SCM+FSA , j be keeping_0 sequential Instruction of SCM+FSA ;

      cluster (I ";" j) -> keeping_0;

      coherence ;

    end

    registration

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

      cluster (i ";" j) -> keeping_0;

      coherence ;

    end

    begin

    ::$Canceled

    theorem :: SCMFSA6C:4

    

     Th3: ( DataPart s1) = ( DataPart s2) implies ( DataPart ( Exec (i,s1))) = ( DataPart ( Exec (i,s2)))

    proof

      assume

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

      set l = i;

      

       A2: ( dom ( Exec (l,s1))) = the carrier of SCM+FSA by PARTFUN1:def 2;

      then

       A3: ( dom ( Exec (l,s1))) = ( dom ( Exec (l,s2))) by PARTFUN1:def 2;

      

       A4: ( dom (( Exec (l,s1)) | ( Data-Locations SCM+FSA ))) = ( Data-Locations SCM+FSA ) by A2, RELAT_1: 62;

      

       A5: ( dom ( Exec (l,s2))) = the carrier of SCM+FSA by PARTFUN1:def 2;

      then

       A6: ( dom (( Exec (l,s2)) | ( Data-Locations SCM+FSA ))) = ( Data-Locations SCM+FSA ) by RELAT_1: 62;

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

      per cases ;

        suppose ( InsCode i) = 0 ;

        then

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

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

        hence thesis by A1, A7, EXTPRO_1:def 3;

      end;

        suppose ( InsCode i) = 1;

        then

        consider db,da be Int-Location such that

         A8: l = (db := da) by SCMFSA_2: 30;

        

         A9: for x be object st x in (( Data-Locations SCM+FSA ) \ {db}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x)

        proof

          let x be object;

          assume

           A10: x in (( Data-Locations SCM+FSA ) \ {db});

          then

           A11: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A12: not x in {db} by A10, XBOOLE_0:def 5;

          per cases by A11, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

             A13: a <> db by A12, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A10, FUNCT_1: 49

            .= (s1 . a) by A8, A13, SCMFSA_2: 63

            .= (( DataPart s1) . a) by A11, FUNCT_1: 49

            .= (s2 . a) by A1, A11, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A8, A13, SCMFSA_2: 63

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A10, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A10, FUNCT_1: 49

            .= (s1 . a) by A8, SCMFSA_2: 63

            .= (( DataPart s1) . a) by A11, FUNCT_1: 49

            .= (s2 . a) by A1, A11, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A8, SCMFSA_2: 63

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A10, FUNCT_1: 49;

          end;

        end;

        

         A14: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A2, RELAT_1: 62;

        then

         A15: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) by A14, A9, FUNCT_1: 2;

        db in Int-Locations by AMI_2:def 16;

        then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A16: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {db}) \/ {db}) by XBOOLE_1: 39;

        

         A17: (( Exec (l,s2)) . db) = (s2 . da) by A8, SCMFSA_2: 63;

        

         A18: (( Exec (l,s1)) . db) = (s1 . da) by A8, SCMFSA_2: 63;

        da in Int-Locations by AMI_2:def 16;

        then

         A19: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A19, FUNCT_1: 49;

        then (( Exec (l,s1)) | {db}) = (( Exec (l,s2)) | {db}) by A3, A18, A17, GRFUNC_1: 29;

        hence thesis by A16, A15, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 2;

        then

        consider db,da be Int-Location such that

         A20: l = ( AddTo (db,da)) by SCMFSA_2: 31;

        

         A21: for x be object st x in (( Data-Locations SCM+FSA ) \ {db}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x)

        proof

          let x be object;

          assume

           A22: x in (( Data-Locations SCM+FSA ) \ {db});

          then

           A23: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A24: not x in {db} by A22, XBOOLE_0:def 5;

          per cases by A23, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

             A25: a <> db by A24, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A22, FUNCT_1: 49

            .= (s1 . a) by A20, A25, SCMFSA_2: 64

            .= (( DataPart s1) . a) by A23, FUNCT_1: 49

            .= (s2 . a) by A1, A23, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A20, A25, SCMFSA_2: 64

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A22, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A22, FUNCT_1: 49

            .= (s1 . a) by A20, SCMFSA_2: 64

            .= (( DataPart s1) . a) by A23, FUNCT_1: 49

            .= (s2 . a) by A1, A23, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A20, SCMFSA_2: 64

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A22, FUNCT_1: 49;

          end;

        end;

        

         A26: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A2, RELAT_1: 62;

        then

         A27: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) by A26, A21, FUNCT_1: 2;

        db in Int-Locations by AMI_2:def 16;

        then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A28: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {db}) \/ {db}) by XBOOLE_1: 39;

        

         A29: (( Exec (l,s2)) . db) = ((s2 . db) + (s2 . da)) by A20, SCMFSA_2: 64;

        

         A30: (( Exec (l,s1)) . db) = ((s1 . db) + (s1 . da)) by A20, SCMFSA_2: 64;

        db in Int-Locations by AMI_2:def 16;

        then

         A31: db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A32: (s1 . db) = (( DataPart s1) . db) by FUNCT_1: 49

        .= (s2 . db) by A1, A31, FUNCT_1: 49;

        da in Int-Locations by AMI_2:def 16;

        then

         A33: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A33, FUNCT_1: 49;

        then (( Exec (l,s1)) | {db}) = (( Exec (l,s2)) | {db}) by A3, A30, A29, A32, GRFUNC_1: 29;

        hence thesis by A28, A27, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 3;

        then

        consider db,da be Int-Location such that

         A34: l = ( SubFrom (db,da)) by SCMFSA_2: 32;

        

         A35: for x be object st x in (( Data-Locations SCM+FSA ) \ {db}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x)

        proof

          let x be object;

          assume

           A36: x in (( Data-Locations SCM+FSA ) \ {db});

          then

           A37: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A38: not x in {db} by A36, XBOOLE_0:def 5;

          per cases by A37, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

             A39: a <> db by A38, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A36, FUNCT_1: 49

            .= (s1 . a) by A34, A39, SCMFSA_2: 65

            .= (( DataPart s1) . a) by A37, FUNCT_1: 49

            .= (s2 . a) by A1, A37, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A34, A39, SCMFSA_2: 65

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A36, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A36, FUNCT_1: 49

            .= (s1 . a) by A34, SCMFSA_2: 65

            .= (( DataPart s1) . a) by A37, FUNCT_1: 49

            .= (s2 . a) by A1, A37, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A34, SCMFSA_2: 65

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A36, FUNCT_1: 49;

          end;

        end;

        

         A40: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A2, RELAT_1: 62;

        then

         A41: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) by A40, A35, FUNCT_1: 2;

        db in Int-Locations by AMI_2:def 16;

        then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A42: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {db}) \/ {db}) by XBOOLE_1: 39;

        

         A43: (( Exec (l,s2)) . db) = ((s2 . db) - (s2 . da)) by A34, SCMFSA_2: 65;

        

         A44: (( Exec (l,s1)) . db) = ((s1 . db) - (s1 . da)) by A34, SCMFSA_2: 65;

        db in Int-Locations by AMI_2:def 16;

        then

         A45: db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A46: (s1 . db) = (( DataPart s1) . db) by FUNCT_1: 49

        .= (s2 . db) by A1, A45, FUNCT_1: 49;

        da in Int-Locations by AMI_2:def 16;

        then

         A47: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A47, FUNCT_1: 49;

        then (( Exec (l,s1)) | {db}) = (( Exec (l,s2)) | {db}) by A3, A44, A43, A46, GRFUNC_1: 29;

        hence thesis by A42, A41, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 4;

        then

        consider db,da be Int-Location such that

         A48: l = ( MultBy (db,da)) by SCMFSA_2: 33;

        

         A49: for x be object st x in (( Data-Locations SCM+FSA ) \ {db}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x)

        proof

          let x be object;

          assume

           A50: x in (( Data-Locations SCM+FSA ) \ {db});

          then

           A51: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A52: not x in {db} by A50, XBOOLE_0:def 5;

          per cases by A51, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

             A53: a <> db by A52, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A50, FUNCT_1: 49

            .= (s1 . a) by A48, A53, SCMFSA_2: 66

            .= (( DataPart s1) . a) by A51, FUNCT_1: 49

            .= (s2 . a) by A1, A51, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A48, A53, SCMFSA_2: 66

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A50, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A50, FUNCT_1: 49

            .= (s1 . a) by A48, SCMFSA_2: 66

            .= (( DataPart s1) . a) by A51, FUNCT_1: 49

            .= (s2 . a) by A1, A51, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A48, SCMFSA_2: 66

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A50, FUNCT_1: 49;

          end;

        end;

        

         A54: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A2, RELAT_1: 62;

        then

         A55: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) by A54, A49, FUNCT_1: 2;

        db in Int-Locations by AMI_2:def 16;

        then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A56: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {db}) \/ {db}) by XBOOLE_1: 39;

        

         A57: (( Exec (l,s2)) . db) = ((s2 . db) * (s2 . da)) by A48, SCMFSA_2: 66;

        

         A58: (( Exec (l,s1)) . db) = ((s1 . db) * (s1 . da)) by A48, SCMFSA_2: 66;

        db in Int-Locations by AMI_2:def 16;

        then

         A59: db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A60: (s1 . db) = (( DataPart s1) . db) by FUNCT_1: 49

        .= (s2 . db) by A1, A59, FUNCT_1: 49;

        da in Int-Locations by AMI_2:def 16;

        then

         A61: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A61, FUNCT_1: 49;

        then (( Exec (l,s1)) | {db}) = (( Exec (l,s2)) | {db}) by A3, A58, A57, A60, GRFUNC_1: 29;

        hence thesis by A56, A55, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 5;

        then

        consider db,da be Int-Location such that

         A62: l = ( Divide (db,da)) by SCMFSA_2: 34;

        hereby

          per cases ;

            suppose

             A63: da <> db;

            

             A64: for x be object st x in (( Data-Locations SCM+FSA ) \ {db, da}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db, da})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db, da})) . x)

            proof

              let x be object;

              assume

               A65: x in (( Data-Locations SCM+FSA ) \ {db, da});

              then

               A66: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

              

               A67: not x in {db, da} by A65, XBOOLE_0:def 5;

              per cases by A66, SCMFSA_2: 100, XBOOLE_0:def 3;

                suppose x in Int-Locations ;

                then

                reconsider a = x as Int-Location by AMI_2:def 16;

                

                 A68: a <> da by A67, TARSKI:def 2;

                

                 A69: a <> db by A67, TARSKI:def 2;

                

                thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db, da})) . x) = (( Exec (l,s1)) . a) by A65, FUNCT_1: 49

                .= (s1 . a) by A62, A68, A69, SCMFSA_2: 67

                .= (( DataPart s1) . a) by A66, FUNCT_1: 49

                .= (s2 . a) by A1, A66, FUNCT_1: 49

                .= (( Exec (l,s2)) . a) by A62, A68, A69, SCMFSA_2: 67

                .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db, da})) . x) by A65, FUNCT_1: 49;

              end;

                suppose x in FinSeq-Locations ;

                then

                reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

                

                thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db, da})) . x) = (( Exec (l,s1)) . a) by A65, FUNCT_1: 49

                .= (s1 . a) by A62, SCMFSA_2: 67

                .= (( DataPart s1) . a) by A66, FUNCT_1: 49

                .= (s2 . a) by A1, A66, FUNCT_1: 49

                .= (( Exec (l,s2)) . a) by A62, SCMFSA_2: 67

                .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db, da})) . x) by A65, FUNCT_1: 49;

              end;

            end;

            

             A70: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db, da}))) = (( Data-Locations SCM+FSA ) \ {db, da}) by A5, RELAT_1: 62;

            ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db, da}))) = (( Data-Locations SCM+FSA ) \ {db, da}) by A2, RELAT_1: 62;

            then

             A71: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db, da})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db, da})) by A70, A64, FUNCT_1: 2;

            

             A72: (( Exec (l,s2)) . da) = ((s2 . db) mod (s2 . da)) by A62, SCMFSA_2: 67;

            db in Int-Locations by AMI_2:def 16;

            then

             A73: db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            

            then

             A74: (s1 . db) = (( DataPart s1) . db) by FUNCT_1: 49

            .= (s2 . db) by A1, A73, FUNCT_1: 49;

            da in Int-Locations by AMI_2:def 16;

            then

             A75: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            db in Int-Locations by AMI_2:def 16;

            then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            

            then

             A76: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db, da}) by A75, ZFMISC_1: 42

            .= ((( Data-Locations SCM+FSA ) \ {db, da}) \/ {db, da}) by XBOOLE_1: 39;

            

             A77: (( Exec (l,s1)) . da) = ((s1 . db) mod (s1 . da)) by A62, SCMFSA_2: 67;

            

             A78: (( Exec (l,s2)) . db) = ((s2 . db) div (s2 . da)) by A62, A63, SCMFSA_2: 67;

            

             A79: (( Exec (l,s1)) . db) = ((s1 . db) div (s1 . da)) by A62, A63, SCMFSA_2: 67;

            da in Int-Locations by AMI_2:def 16;

            then

             A80: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            

            then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

            .= (s2 . da) by A1, A80, FUNCT_1: 49;

            then (( Exec (l,s1)) | {db, da}) = (( Exec (l,s2)) | {db, da}) by A3, A79, A77, A78, A72, A74, GRFUNC_1: 30;

            hence thesis by A76, A71, RELAT_1: 150;

          end;

            suppose

             A81: da = db;

            

             A82: for x be object st x in (( Data-Locations SCM+FSA ) \ {db}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x)

            proof

              let x be object;

              assume

               A83: x in (( Data-Locations SCM+FSA ) \ {db});

              then

               A84: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

              

               A85: not x in {db} by A83, XBOOLE_0:def 5;

              per cases by A84, SCMFSA_2: 100, XBOOLE_0:def 3;

                suppose x in Int-Locations ;

                then

                reconsider a = x as Int-Location by AMI_2:def 16;

                

                 A86: a <> db by A85, TARSKI:def 1;

                

                thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A83, FUNCT_1: 49

                .= (s1 . a) by A62, A81, A86, SCMFSA_2: 68

                .= (( DataPart s1) . a) by A84, FUNCT_1: 49

                .= (s2 . a) by A1, A84, FUNCT_1: 49

                .= (( Exec (l,s2)) . a) by A62, A81, A86, SCMFSA_2: 68

                .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A83, FUNCT_1: 49;

              end;

                suppose x in FinSeq-Locations ;

                then

                reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

                

                thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A83, FUNCT_1: 49

                .= (s1 . a) by A62, A81, SCMFSA_2: 68

                .= ((s1 | ( Data-Locations SCM+FSA )) . a) by A84, FUNCT_1: 49

                .= (s2 . a) by A1, A84, FUNCT_1: 49

                .= (( Exec (l,s2)) . a) by A62, A81, SCMFSA_2: 68

                .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A83, FUNCT_1: 49;

              end;

            end;

            

             A87: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A5, RELAT_1: 62;

            ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A2, RELAT_1: 62;

            then

             A88: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) by A87, A82, FUNCT_1: 2;

            db in Int-Locations by AMI_2:def 16;

            then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            

            then

             A89: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db}) by ZFMISC_1: 40

            .= ((( Data-Locations SCM+FSA ) \ {db}) \/ {db}) by XBOOLE_1: 39;

            

             A90: (( Exec (l,s2)) . db) = ((s2 . db) mod (s2 . da)) by A62, A81, SCMFSA_2: 68;

            

             A91: (( Exec (l,s1)) . db) = ((s1 . db) mod (s1 . da)) by A62, A81, SCMFSA_2: 68;

            db in Int-Locations by AMI_2:def 16;

            then

             A92: db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            

            then

             A93: (s1 . db) = (( DataPart s1) . db) by FUNCT_1: 49

            .= (s2 . db) by A1, A92, FUNCT_1: 49;

            da in Int-Locations by AMI_2:def 16;

            then

             A94: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

            

            then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

            .= (s2 . da) by A1, A94, FUNCT_1: 49;

            then (( Exec (l,s1)) | {db}) = (( Exec (l,s2)) | {db}) by A3, A91, A90, A93, GRFUNC_1: 29;

            hence thesis by A89, A88, RELAT_1: 150;

          end;

        end;

      end;

        suppose ( InsCode i) = 6;

        then

         A95: ex l1 st i = ( goto l1) by SCMFSA_2: 35;

        for x be object st x in ( Data-Locations SCM+FSA ) holds (( DataPart ( Exec (l,s1))) . x) = (( DataPart ( Exec (l,s2))) . x)

        proof

          let x be object;

          assume

           A96: x in ( Data-Locations SCM+FSA );

          per cases by A96, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

            thus (( DataPart ( Exec (l,s1))) . x) = (( Exec (l,s1)) . a) by A96, FUNCT_1: 49

            .= (s1 . a) by A95, SCMFSA_2: 69

            .= (( DataPart s1) . a) by A96, FUNCT_1: 49

            .= (s2 . a) by A1, A96, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A95, SCMFSA_2: 69

            .= (( DataPart ( Exec (l,s2))) . x) by A96, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus (( DataPart ( Exec (l,s1))) . x) = (( Exec (l,s1)) . a) by A96, FUNCT_1: 49

            .= (s1 . a) by A95, SCMFSA_2: 69

            .= (( DataPart s1) . a) by A96, FUNCT_1: 49

            .= (s2 . a) by A1, A96, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A95, SCMFSA_2: 69

            .= (( DataPart ( Exec (l,s2))) . x) by A96, FUNCT_1: 49;

          end;

        end;

        hence thesis by A4, A6, FUNCT_1: 2;

      end;

        suppose ( InsCode i) = 7;

        then

         A97: ex l1, a st i = (a =0_goto l1) by SCMFSA_2: 36;

        for x be object st x in ( Data-Locations SCM+FSA ) holds (( DataPart ( Exec (l,s1))) . x) = (( DataPart ( Exec (l,s2))) . x)

        proof

          let x be object;

          assume

           A98: x in ( Data-Locations SCM+FSA );

          per cases by A98, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

            thus (( DataPart ( Exec (l,s1))) . x) = (( Exec (l,s1)) . a) by A98, FUNCT_1: 49

            .= (s1 . a) by A97, SCMFSA_2: 70

            .= (( DataPart s1) . a) by A98, FUNCT_1: 49

            .= (s2 . a) by A1, A98, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A97, SCMFSA_2: 70

            .= (( DataPart ( Exec (l,s2))) . x) by A98, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus (( DataPart ( Exec (l,s1))) . x) = (( Exec (l,s1)) . a) by A98, FUNCT_1: 49

            .= (s1 . a) by A97, SCMFSA_2: 70

            .= (( DataPart s1) . a) by A98, FUNCT_1: 49

            .= (s2 . a) by A1, A98, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A97, SCMFSA_2: 70

            .= (( DataPart ( Exec (l,s2))) . x) by A98, FUNCT_1: 49;

          end;

        end;

        hence thesis by A4, A6, FUNCT_1: 2;

      end;

        suppose ( InsCode i) = 8;

        then

         A99: ex l1, a st i = (a >0_goto l1) by SCMFSA_2: 37;

        for x be object st x in ( Data-Locations SCM+FSA ) holds (( DataPart ( Exec (l,s1))) . x) = (( DataPart ( Exec (l,s2))) . x)

        proof

          let x be object;

          assume

           A100: x in ( Data-Locations SCM+FSA );

          per cases by A100, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

            thus (( DataPart ( Exec (l,s1))) . x) = (( Exec (l,s1)) . a) by A100, FUNCT_1: 49

            .= (s1 . a) by A99, SCMFSA_2: 71

            .= (( DataPart s1) . a) by A100, FUNCT_1: 49

            .= (s2 . a) by A1, A100, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A99, SCMFSA_2: 71

            .= (( DataPart ( Exec (l,s2))) . x) by A100, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus (( DataPart ( Exec (l,s1))) . x) = (( Exec (l,s1)) . a) by A100, FUNCT_1: 49

            .= (s1 . a) by A99, SCMFSA_2: 71

            .= (( DataPart s1) . a) by A100, FUNCT_1: 49

            .= (s2 . a) by A1, A100, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A99, SCMFSA_2: 71

            .= (( DataPart ( Exec (l,s2))) . x) by A100, FUNCT_1: 49;

          end;

        end;

        hence thesis by A4, A6, FUNCT_1: 2;

      end;

        suppose ( InsCode i) = 9;

        then

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

         A101: l = (db := (fa,da)) by SCMFSA_2: 38;

        

         A102: for x be object st x in (( Data-Locations SCM+FSA ) \ {db}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x)

        proof

          let x be object;

          assume

           A103: x in (( Data-Locations SCM+FSA ) \ {db});

          then

           A104: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A105: not x in {db} by A103, XBOOLE_0:def 5;

          per cases by A104, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

             A106: a <> db by A105, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A103, FUNCT_1: 49

            .= (s1 . a) by A101, A106, SCMFSA_2: 72

            .= (( DataPart s1) . a) by A104, FUNCT_1: 49

            .= (s2 . a) by A1, A104, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A101, A106, SCMFSA_2: 72

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A103, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) . x) = (( Exec (l,s1)) . a) by A103, FUNCT_1: 49

            .= (s1 . a) by A101, SCMFSA_2: 72

            .= (( DataPart s1) . a) by A104, FUNCT_1: 49

            .= (s2 . a) by A1, A104, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A101, SCMFSA_2: 72

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) . x) by A103, FUNCT_1: 49;

          end;

        end;

        

         A107: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db}))) = (( Data-Locations SCM+FSA ) \ {db}) by A2, RELAT_1: 62;

        then

         A108: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {db})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {db})) by A107, A102, FUNCT_1: 2;

        db in Int-Locations by AMI_2:def 16;

        then db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A109: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {db}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {db}) \/ {db}) by XBOOLE_1: 39;

        

         A110: ex k2 be Nat st k2 = |.(s2 . da).| & (( Exec (l,s2)) . db) = ((s2 . fa) /. k2) by A101, SCMFSA_2: 72;

        

         A111: ex k1 be Nat st k1 = |.(s1 . da).| & (( Exec (l,s1)) . db) = ((s1 . fa) /. k1) by A101, SCMFSA_2: 72;

        fa in FinSeq-Locations by SCMFSA_2:def 5;

        then

         A112: fa in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A113: (s1 . fa) = (( DataPart s1) . fa) by FUNCT_1: 49

        .= (s2 . fa) by A1, A112, FUNCT_1: 49;

        da in Int-Locations by AMI_2:def 16;

        then

         A114: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A114, FUNCT_1: 49;

        then (( Exec (l,s1)) | {db}) = (( Exec (l,s2)) | {db}) by A3, A111, A110, A113, GRFUNC_1: 29;

        hence thesis by A109, A108, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 10;

        then

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

         A115: l = ((fa,da) := db) by SCMFSA_2: 39;

        

         A116: for x be object st x in (( Data-Locations SCM+FSA ) \ {fa}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) . x)

        proof

          let x be object;

          assume

           A117: x in (( Data-Locations SCM+FSA ) \ {fa});

          then

           A118: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A119: not x in {fa} by A117, XBOOLE_0:def 5;

          per cases by A118, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) = (( Exec (l,s1)) . a) by A117, FUNCT_1: 49

            .= (s1 . a) by A115, SCMFSA_2: 73

            .= (( DataPart s1) . a) by A118, FUNCT_1: 49

            .= (s2 . a) by A1, A118, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A115, SCMFSA_2: 73

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) by A117, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

             A120: a <> fa by A119, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) = (( Exec (l,s1)) . a) by A117, FUNCT_1: 49

            .= (s1 . a) by A115, A120, SCMFSA_2: 73

            .= (( DataPart s1) . a) by A118, FUNCT_1: 49

            .= (s2 . a) by A1, A118, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A115, A120, SCMFSA_2: 73

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) by A117, FUNCT_1: 49;

          end;

        end;

        

         A121: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa}))) = (( Data-Locations SCM+FSA ) \ {fa}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa}))) = (( Data-Locations SCM+FSA ) \ {fa}) by A2, RELAT_1: 62;

        then

         A122: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) by A121, A116, FUNCT_1: 2;

        fa in FinSeq-Locations by SCMFSA_2:def 5;

        then fa in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A123: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {fa}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {fa}) \/ {fa}) by XBOOLE_1: 39;

        fa in FinSeq-Locations by SCMFSA_2:def 5;

        then

         A124: fa in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A125: (s1 . fa) = (( DataPart s1) . fa) by FUNCT_1: 49

        .= (s2 . fa) by A1, A124, FUNCT_1: 49;

        db in Int-Locations by AMI_2:def 16;

        then

         A126: db in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A127: (s1 . db) = (( DataPart s1) . db) by FUNCT_1: 49

        .= (s2 . db) by A1, A126, FUNCT_1: 49;

        

         A128: ex k2 be Nat st k2 = |.(s2 . da).| & (( Exec (l,s2)) . fa) = ((s2 . fa) +* (k2,(s2 . db))) by A115, SCMFSA_2: 73;

        

         A129: ex k1 be Nat st k1 = |.(s1 . da).| & (( Exec (l,s1)) . fa) = ((s1 . fa) +* (k1,(s1 . db))) by A115, SCMFSA_2: 73;

        da in Int-Locations by AMI_2:def 16;

        then

         A130: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A130, FUNCT_1: 49;

        then (( Exec (l,s1)) | {fa}) = (( Exec (l,s2)) | {fa}) by A3, A129, A128, A127, A125, GRFUNC_1: 29;

        hence thesis by A123, A122, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 11;

        then

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

         A131: l = (da :=len fa) by SCMFSA_2: 40;

        

         A132: for x be object st x in (( Data-Locations SCM+FSA ) \ {da}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {da})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {da})) . x)

        proof

          let x be object;

          assume

           A133: x in (( Data-Locations SCM+FSA ) \ {da});

          then

           A134: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A135: not x in {da} by A133, XBOOLE_0:def 5;

          per cases by A134, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

             A136: a <> da by A135, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {da})) . x) = (( Exec (l,s1)) . a) by A133, FUNCT_1: 49

            .= (s1 . a) by A131, A136, SCMFSA_2: 74

            .= (( DataPart s1) . a) by A134, FUNCT_1: 49

            .= (s2 . a) by A1, A134, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A131, A136, SCMFSA_2: 74

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {da})) . x) by A133, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {da})) . x) = (( Exec (l,s1)) . a) by A133, FUNCT_1: 49

            .= (s1 . a) by A131, SCMFSA_2: 74

            .= (( DataPart s1) . a) by A134, FUNCT_1: 49

            .= (s2 . a) by A1, A134, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A131, SCMFSA_2: 74

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {da})) . x) by A133, FUNCT_1: 49;

          end;

        end;

        da in Int-Locations by AMI_2:def 16;

        then da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A137: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {da}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {da}) \/ {da}) by XBOOLE_1: 39;

        fa in FinSeq-Locations by SCMFSA_2:def 5;

        then

         A138: fa in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . fa) = ((s1 | ( Data-Locations SCM+FSA )) . fa) by FUNCT_1: 49

        .= (s2 . fa) by A1, A138, FUNCT_1: 49;

        

        then (( Exec (l,s1)) . da) = ( len (s2 . fa)) by A131, SCMFSA_2: 74

        .= (( Exec (l,s2)) . da) by A131, SCMFSA_2: 74;

        then

         A139: (( Exec (l,s1)) | {da}) = (( Exec (l,s2)) | {da}) by A2, A5, GRFUNC_1: 29;

        

         A140: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {da}))) = (( Data-Locations SCM+FSA ) \ {da}) by A5, RELAT_1: 62;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {da}))) = (( Data-Locations SCM+FSA ) \ {da}) by A2, RELAT_1: 62;

        then (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {da})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {da})) by A140, A132, FUNCT_1: 2;

        hence thesis by A137, A139, RELAT_1: 150;

      end;

        suppose ( InsCode i) = 12;

        then

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

         A141: i = (fa :=<0,...,0> da) by SCMFSA_2: 41;

        set l = i;

        

         A142: ( dom (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa}))) = (( Data-Locations SCM+FSA ) \ {fa}) by A5, RELAT_1: 62;

        

         A143: ex k2 be Nat st k2 = |.(s2 . da).| & (( Exec (l,s2)) . fa) = (k2 |-> 0 ) by A141, SCMFSA_2: 75;

        

         A144: ex k1 be Nat st k1 = |.(s1 . da).| & (( Exec (l,s1)) . fa) = (k1 |-> 0 ) by A141, SCMFSA_2: 75;

        

         A145: for x be object st x in (( Data-Locations SCM+FSA ) \ {fa}) holds ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) = ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) . x)

        proof

          let x be object;

          assume

           A146: x in (( Data-Locations SCM+FSA ) \ {fa});

          then

           A147: x in ( Data-Locations SCM+FSA ) by XBOOLE_0:def 5;

          

           A148: not x in {fa} by A146, XBOOLE_0:def 5;

          per cases by A147, SCMFSA_2: 100, XBOOLE_0:def 3;

            suppose x in Int-Locations ;

            then

            reconsider a = x as Int-Location by AMI_2:def 16;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) = (( Exec (l,s1)) . a) by A146, FUNCT_1: 49

            .= (s1 . a) by A141, SCMFSA_2: 75

            .= (( DataPart s1) . a) by A147, FUNCT_1: 49

            .= (s2 . a) by A1, A147, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A141, SCMFSA_2: 75

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) by A146, FUNCT_1: 49;

          end;

            suppose x in FinSeq-Locations ;

            then

            reconsider a = x as FinSeq-Location by SCMFSA_2:def 5;

            

             A149: a <> fa by A148, TARSKI:def 1;

            

            thus ((( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) = (( Exec (l,s1)) . a) by A146, FUNCT_1: 49

            .= (s1 . a) by A141, A149, SCMFSA_2: 75

            .= (( DataPart s1) . a) by A147, FUNCT_1: 49

            .= (s2 . a) by A1, A147, FUNCT_1: 49

            .= (( Exec (l,s2)) . a) by A141, A149, SCMFSA_2: 75

            .= ((( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) . x) by A146, FUNCT_1: 49;

          end;

        end;

        ( dom (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa}))) = (( Data-Locations SCM+FSA ) \ {fa}) by A2, RELAT_1: 62;

        then

         A150: (( Exec (l,s1)) | (( Data-Locations SCM+FSA ) \ {fa})) = (( Exec (l,s2)) | (( Data-Locations SCM+FSA ) \ {fa})) by A142, A145, FUNCT_1: 2;

        fa in FinSeq-Locations by SCMFSA_2:def 5;

        then fa in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then

         A151: ( Data-Locations SCM+FSA ) = (( Data-Locations SCM+FSA ) \/ {fa}) by ZFMISC_1: 40

        .= ((( Data-Locations SCM+FSA ) \ {fa}) \/ {fa}) by XBOOLE_1: 39;

        da in Int-Locations by AMI_2:def 16;

        then

         A152: da in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

        then (s1 . da) = (( DataPart s1) . da) by FUNCT_1: 49

        .= (s2 . da) by A1, A152, FUNCT_1: 49;

        then (( Exec (l,s1)) | {fa}) = (( Exec (l,s2)) | {fa}) by A3, A144, A143, GRFUNC_1: 29;

        hence thesis by A151, A150, RELAT_1: 150;

      end;

    end;

     Lm2:

    now

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

      let I be keeping_0 parahalting Program of SCM+FSA , s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      set IE = ( IExec (I,P,s));

      now

        

         A1: ( dom ( Initialized IE)) = the carrier of SCM+FSA by PARTFUN1:def 2;

        

         A2: the carrier of SCM+FSA = ( {( IC SCM+FSA )} \/ ( Data-Locations SCM+FSA )) by STRUCT_0: 4;

        

         A3: ( dom IE) = the carrier of SCM+FSA by PARTFUN1:def 2;

        hence ( dom ( DataPart ( Initialized IE))) = (( dom IE) /\ IF) by A1, RELAT_1: 61;

        then

         A4: ( dom ( DataPart ( Initialized IE))) = ( Data-Locations SCM+FSA ) by A3, A2, XBOOLE_1: 21;

        let x be object;

        assume

         A5: x in ( dom ( DataPart ( Initialized IE)));

        per cases by A5, A4, SCMFSA_2: 100, XBOOLE_0:def 3;

          suppose x in Int-Locations ;

          then

          reconsider x9 = x as Int-Location by AMI_2:def 16;

          per cases ;

            suppose

             A6: x9 is read-write;

            

            thus (( DataPart ( Initialized IE)) . x) = (( Initialized IE) . x) by A5, A4, FUNCT_1: 49

            .= (IE . x) by A6, SCMFSA_M: 37;

          end;

            suppose x9 is read-only;

            then

             A7: x9 = ( intloc 0 );

            

            thus (( DataPart ( Initialized IE)) . x) = (( Initialized IE) . x9) by A5, A4, FUNCT_1: 49

            .= 1 by A7, SCMFSA_M: 9

            .= (IE . x) by A7, SCMFSA6B: 11;

          end;

        end;

          suppose x in FinSeq-Locations ;

          then

          reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;

          

          thus (( DataPart ( Initialized IE)) . x) = (( Initialized IE) . x9) by A5, A4, FUNCT_1: 49

          .= (IE . x) by SCMFSA_M: 37;

        end;

      end;

      hence ( DataPart ( Initialized IE)) = ( DataPart IE) by FUNCT_1: 46;

    end;

    theorem :: SCMFSA6C:5

    

     Th4: for i be sequential Instruction of SCM+FSA holds ( Exec (i,( Initialized s))) = ( IExec (( Macro i),P,s))

    proof

      let i be sequential Instruction of SCM+FSA ;

      set Mi = ( Macro i);

      set sI = (s +* ( Initialize (( intloc 0 ) .--> 1))), pI = (P +* Mi);

      

       A1: Mi c= pI by FUNCT_4: 25;

      set Is = ( Initialized s);

      set IC1 = ( IC ( Comput ((P +* Mi),sI,1)));

      reconsider Mi as parahalting Program of SCM+FSA ;

      ( IC sI) = 0 by MEMSTR_0:def 11;

      then ( IC sI) in ( dom Mi) by AFINSQ_1: 65;

      then

       A2: IC1 in ( dom Mi) by A1, AMISTD_1: 21;

      

       A3: 1 in ( dom Mi) by COMPOS_1: 60;

      

       A4: 0 in ( dom Mi) by COMPOS_1: 60;

      

       A5: (Mi . 0 ) = i by COMPOS_1: 58;

      

       A6: ( IC sI) = 0 by MEMSTR_0:def 11;

      

       A7: ( Comput ((P +* Mi),sI,( 0 + 1))) = ( Following ((P +* Mi),( Comput ((P +* Mi),sI, 0 )))) by EXTPRO_1: 3

      .= ( Exec ((pI . 0 ),sI)) by A6, PBOOLE: 143

      .= ( Exec (i,sI)) by A5, A1, A4, GRFUNC_1: 2;

      per cases by A2, COMPOS_1: 60;

        suppose

         A8: IC1 = 0 ;

        

        then

         A9: ( CurInstr ((P +* Mi),( Comput ((P +* Mi),sI,1)))) = ((P +* Mi) . 0 ) by PBOOLE: 143

        .= i by A5, A4, FUNCT_4: 13;

        ( IC sI) = 0 by A6;

        then

         A10: ( InsCode i) in { 0 , 6, 7, 8} by A7, A8, SCMFSA6A: 3;

        hereby

          per cases by A10, ENUMSET1:def 2;

            suppose ( InsCode i) = 0 ;

            then

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

            then (P +* Mi) halts_on sI by A9, EXTPRO_1: 29;

            hence thesis by A7, A9, A11, EXTPRO_1:def 9;

          end;

            suppose

             A12: ( InsCode i) = 6 or ( InsCode i) = 7 or ( InsCode i) = 8;

             A13:

            now

              let a;

              per cases by A12;

                suppose ( InsCode i) = 6;

                then ex l st i = ( goto l) by SCMFSA_2: 35;

                hence (sI . a) = (( Exec (i,sI)) . a);

              end;

                suppose ( InsCode i) = 7;

                then ex l, b st i = (b =0_goto l) by SCMFSA_2: 36;

                hence (sI . a) = (( Exec (i,sI)) . a);

              end;

                suppose ( InsCode i) = 8;

                then ex l, b st i = (b >0_goto l) by SCMFSA_2: 37;

                hence (sI . a) = (( Exec (i,sI)) . a);

              end;

            end;

             A14:

            now

              let f;

              per cases by A12;

                suppose ( InsCode i) = 6;

                then ex l st i = ( goto l) by SCMFSA_2: 35;

                hence (sI . f) = (( Exec (i,sI)) . f);

              end;

                suppose ( InsCode i) = 7;

                then ex l, a st i = (a =0_goto l) by SCMFSA_2: 36;

                hence (sI . f) = (( Exec (i,sI)) . f);

              end;

                suppose ( InsCode i) = 8;

                then ex l, a st i = (a >0_goto l) by SCMFSA_2: 37;

                hence (sI . f) = (( Exec (i,sI)) . f);

              end;

            end;

            

             A15: ( Following ((P +* Mi),sI)) = ( Following ((P +* Mi),( Comput ((P +* Mi),sI, 0 ))))

            .= ( Exec (i,sI)) by A7, EXTPRO_1: 3;

            

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

            for n be Nat holds ( CurInstr ((P +* Mi),( Comput ((P +* Mi),sI,n)))) <> ( halt SCM+FSA ) by A9, A12, A13, A14, A7, A8, A6, A15, A16, AMISTD_2: 11, SCMFSA_2: 104;

            then

             A17: not (P +* Mi) halts_on sI;

            Mi c= (P +* Mi) by FUNCT_4: 25;

            hence ( Exec (i,( Initialized s))) = ( IExec (( Macro i),P,s)) by A17, AMISTD_1:def 11;

          end;

        end;

      end;

        suppose

         A18: IC1 = 1;

        

         A19: (Mi . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

        

         A20: ( CurInstr ((P +* Mi),( Comput ((P +* Mi),sI,1)))) = ((P +* Mi) . 1) by A18, PBOOLE: 143

        .= ( halt SCM+FSA ) by A19, A1, A3, GRFUNC_1: 2;

        then (P +* Mi) halts_on sI by EXTPRO_1: 29;

        hence thesis by A7, A20, EXTPRO_1:def 9;

      end;

    end;

    theorem :: SCMFSA6C:6

    

     Th5: for I be keeping_0 parahalting really-closed Program of SCM+FSA , j be sequential Instruction of SCM+FSA holds (( IExec ((I ";" j),P,s)) . a) = (( Exec (j,( IExec (I,P,s)))) . a)

    proof

      let I be keeping_0 parahalting really-closed Program of SCM+FSA , j be sequential Instruction of SCM+FSA ;

      set Mj = ( Macro j);

      set SA = ( Start-At ((( IC ( IExec (Mj,P,( IExec (I,P,s))))) + ( card I)), SCM+FSA ));

      

       A1: not a in ( dom SA) by SCMFSA_2: 102;

      

       A2: ( DataPart ( Initialized ( IExec (I,P,s)))) = ( DataPart ( IExec (I,P,s))) by Lm2;

      a in Int-Locations by AMI_2:def 16;

      then

       A3: a in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

      

      thus (( IExec ((I ";" j),P,s)) . a) = (( IncIC (( IExec (Mj,P,( IExec (I,P,s)))),( card I))) . a) by SCMFSA6B: 20

      .= (( IExec (Mj,P,( IExec (I,P,s)))) . a) by A1, FUNCT_4: 11

      .= (( Exec (j,( Initialized ( IExec (I,P,s))))) . a) by Th4

      .= (( DataPart ( Exec (j,( Initialized ( IExec (I,P,s)))))) . a) by A3, FUNCT_1: 49

      .= (( DataPart ( Exec (j,( IExec (I,P,s))))) . a) by A2, Th3

      .= (( Exec (j,( IExec (I,P,s)))) . a) by A3, FUNCT_1: 49;

    end;

    theorem :: SCMFSA6C:7

    

     Th6: for I be keeping_0 parahalting really-closed Program of SCM+FSA , j be sequential Instruction of SCM+FSA holds (( IExec ((I ";" j),P,s)) . f) = (( Exec (j,( IExec (I,P,s)))) . f)

    proof

      let I be keeping_0 parahalting really-closed Program of SCM+FSA , j be sequential Instruction of SCM+FSA ;

      set Mj = ( Macro j);

      set SA = ( Start-At ((( IC ( IExec (Mj,P,( IExec (I,P,s))))) + ( card I)), SCM+FSA ));

      

       A1: not f in ( dom SA) by SCMFSA_2: 103;

      

       A2: ( DataPart ( Initialized ( IExec (I,P,s)))) = ( DataPart ( IExec (I,P,s))) by Lm2;

      f in FinSeq-Locations by SCMFSA_2:def 5;

      then

       A3: f in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

      

      thus (( IExec ((I ";" j),P,s)) . f) = (( IncIC (( IExec (Mj,P,( IExec (I,P,s)))),( card I))) . f) by SCMFSA6B: 20

      .= (( IExec (Mj,P,( IExec (I,P,s)))) . f) by A1, FUNCT_4: 11

      .= (( Exec (j,( Initialized ( IExec (I,P,s))))) . f) by Th4

      .= (( DataPart ( Exec (j,( Initialized ( IExec (I,P,s)))))) . f) by A3, FUNCT_1: 49

      .= (( DataPart ( Exec (j,( IExec (I,P,s))))) . f) by A2, Th3

      .= (( Exec (j,( IExec (I,P,s)))) . f) by A3, FUNCT_1: 49;

    end;

    theorem :: SCMFSA6C:8

    

     Th7: for i be keeping_0 sequential Instruction of SCM+FSA , j be sequential Instruction of SCM+FSA holds (( IExec ((i ";" j),P,s)) . a) = (( Exec (j,( Exec (i,( Initialized s))))) . a)

    proof

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

      set Mi = ( Macro i);

      

      thus (( IExec ((i ";" j),P,s)) . a) = (( IExec ((Mi ";" j),P,s)) . a)

      .= (( Exec (j,( IExec (Mi,P,s)))) . a) by Th5

      .= (( Exec (j,( Exec (i,( Initialized s))))) . a) by Th4;

    end;

    theorem :: SCMFSA6C:9

    for i be keeping_0 sequential Instruction of SCM+FSA , j be sequential Instruction of SCM+FSA holds (( IExec ((i ";" j),P,s)) . f) = (( Exec (j,( Exec (i,( Initialized s))))) . f)

    proof

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

      set Mi = ( Macro i);

      

      thus (( IExec ((i ";" j),P,s)) . f) = (( IExec ((Mi ";" j),P,s)) . f)

      .= (( Exec (j,( IExec (Mi,P,s)))) . f) by Th6

      .= (( Exec (j,( Exec (i,( Initialized s))))) . f) by Th4;

    end;

    begin

    definition

      let a,b be Int-Location;

      :: SCMFSA6C:def2

      func swap (a,b) -> Program of SCM+FSA equals (((( FirstNotUsed ( Macro (a := b))) := a) ";" (a := b)) ";" (b := ( FirstNotUsed ( Macro (a := b)))));

      correctness ;

    end

    registration

      let a,b be Int-Location;

      cluster ( swap (a,b)) -> parahalting really-closed;

      coherence ;

    end

    registration

      let a,b be read-write Int-Location;

      cluster ( swap (a,b)) -> keeping_0;

      coherence ;

    end

    theorem :: SCMFSA6C:10

    for a,b be read-write Int-Location holds (( IExec (( swap (a,b)),P,s)) . a) = (s . b) & (( IExec (( swap (a,b)),P,s)) . b) = (s . a)

    proof

      let a,b be read-write Int-Location;

      set i0 = (( FirstNotUsed ( Macro (a := b))) := a);

      set i1 = (a := b);

      set i2 = (b := ( FirstNotUsed ( Macro (a := b))));

      set i01 = (i0 ";" i1);

      ( UsedILoc ( Macro (a := b))) = ( UsedIntLoc (a := b)) by SF_MASTR: 28;

      then ( UsedILoc ( Macro (a := b))) = {a, b} by SF_MASTR: 14;

      then

       A1: not ( FirstNotUsed ( Macro (a := b))) in {a, b} by SF_MASTR: 50;

      then

       A2: ( FirstNotUsed ( Macro (a := b))) <> a by TARSKI:def 2;

      

       A3: ( FirstNotUsed ( Macro (a := b))) <> b by A1, TARSKI:def 2;

      hereby

        per cases ;

          suppose

           A4: a <> b;

          

          thus (( IExec (( swap (a,b)),P,s)) . a) = (( Exec (i2,( IExec (i01,P,s)))) . a) by Th5

          .= (( IExec (i01,P,s)) . a) by A4, SCMFSA_2: 63

          .= (( Exec (i1,( Exec (i0,( Initialized s))))) . a) by Th7

          .= (( Exec (i0,( Initialized s))) . b) by SCMFSA_2: 63

          .= (( Initialized s) . b) by A3, SCMFSA_2: 63

          .= (s . b) by SCMFSA_M: 37;

        end;

          suppose

           A5: a = b;

          

          thus (( IExec (( swap (a,b)),P,s)) . a) = (( Exec (i2,( IExec (i01,P,s)))) . a) by Th5

          .= (( IExec (i01,P,s)) . ( FirstNotUsed ( Macro (a := b)))) by A5, SCMFSA_2: 63

          .= (( Exec (i1,( Exec (i0,( Initialized s))))) . ( FirstNotUsed ( Macro (a := b)))) by Th7

          .= (( Exec (i0,( Initialized s))) . ( FirstNotUsed ( Macro (a := b)))) by A2, SCMFSA_2: 63

          .= (( Initialized s) . a) by SCMFSA_2: 63

          .= (s . b) by A5, SCMFSA_M: 37;

        end;

      end;

      

      thus (( IExec (( swap (a,b)),P,s)) . b) = (( Exec (i2,( IExec (i01,P,s)))) . b) by Th5

      .= (( IExec (i01,P,s)) . ( FirstNotUsed ( Macro (a := b)))) by SCMFSA_2: 63

      .= (( Exec (i1,( Exec (i0,( Initialized s))))) . ( FirstNotUsed ( Macro (a := b)))) by Th7

      .= (( Exec (i0,( Initialized s))) . ( FirstNotUsed ( Macro (a := b)))) by A2, SCMFSA_2: 63

      .= (( Initialized s) . a) by SCMFSA_2: 63

      .= (s . a) by SCMFSA_M: 37;

    end;

    theorem :: SCMFSA6C:11

    ( UsedI*Loc ( swap (a,b))) = {}

    proof

      set i0 = (( FirstNotUsed ( Macro (a := b))) := a);

      set i1 = (a := b);

      set i2 = (b := ( FirstNotUsed ( Macro (a := b))));

      

      thus ( UsedI*Loc ( swap (a,b))) = (( UsedI*Loc (i0 ";" i1)) \/ ( UsedInt*Loc i2)) by SF_MASTR: 46

      .= (( UsedI*Loc (i0 ";" i1)) \/ {} ) by SF_MASTR: 32

      .= (( UsedInt*Loc i0) \/ ( UsedInt*Loc i1)) by SF_MASTR: 47

      .= (( UsedInt*Loc i0) \/ {} ) by SF_MASTR: 32

      .= {} by SF_MASTR: 32;

    end;

    registration

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

      cluster (i ';' j) -> really-closed;

      coherence ;

    end

    registration

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

      cluster (I ';' j) -> really-closed;

      coherence ;

    end

    registration

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

      cluster (i ';' J) -> really-closed;

      coherence ;

    end