sfmastr1.miz



    begin

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

    definition

      let i be Instruction of SCM+FSA ;

      :: SFMASTR1:def1

      attr i is good means

      : Def1: ( Macro i) is good;

    end

    registration

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

      cluster (a := b) -> good;

      coherence by SCMFSA7B: 6, SCMFSA8C: 70;

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

      coherence by SCMFSA7B: 7, SCMFSA8C: 70;

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

      coherence by SCMFSA7B: 8, SCMFSA8C: 70;

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

      coherence by SCMFSA7B: 9, SCMFSA8C: 70;

    end

    registration

      cluster good sequential for Instruction of SCM+FSA ;

      existence

      proof

        set a = the read-write Int-Location;

        take (a := a);

        thus thesis;

      end;

    end

    registration

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

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

      coherence by SCMFSA7B: 10, SCMFSA8C: 70;

    end

    registration

      let l be Element of NAT ;

      cluster ( goto l) -> good;

      coherence by SCMFSA7B: 11, SCMFSA8C: 70;

    end

    registration

      let a be Int-Location, l be Element of NAT ;

      cluster (a =0_goto l) -> good;

      coherence by SCMFSA7B: 12, SCMFSA8C: 70;

      cluster (a >0_goto l) -> good;

      coherence by SCMFSA7B: 13, SCMFSA8C: 70;

    end

    registration

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

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

      coherence by SCMFSA7B: 14, SCMFSA8C: 70;

    end

    registration

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

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

      coherence by SCMFSA7B: 16, SCMFSA8C: 70;

    end

    registration

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

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

      coherence by SCMFSA7B: 17, SCMFSA8C: 70;

      let b be Int-Location;

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

      coherence by SCMFSA7B: 15, SCMFSA8C: 70;

    end

    registration

      let i be good Instruction of SCM+FSA ;

      cluster ( Macro i) -> good;

      coherence by Def1;

    end

    registration

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

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

      coherence ;

    end

    registration

      let i be good Instruction of SCM+FSA , I be good Program of SCM+FSA ;

      cluster (i ";" I) -> good;

      coherence ;

      cluster (I ";" i) -> good;

      coherence ;

    end

    registration

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

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

      coherence

      proof

        ( swap (a,b)) = (((( FirstNotUsed ( Macro (a := b))) := a) ";" (a := b)) ";" (b := ( FirstNotUsed ( Macro (a := b))))) by SCMFSA6C:def 3;

        hence thesis;

      end;

    end

    registration

      let I be good MacroInstruction of SCM+FSA , a be read-write Int-Location;

      cluster ( Times (a,I)) -> good;

      coherence ;

    end

    theorem :: SFMASTR1:1

    for a be Int-Location, I be Program of SCM+FSA st not a in ( UsedILoc I) holds not I destroys a

    proof

      let aa be Int-Location, I be Program of SCM+FSA such that

       A1: not aa in ( UsedILoc I);

      let i be Instruction of SCM+FSA ;

      assume i in ( rng I);

      then ( UsedIntLoc i) c= ( UsedILoc I) by SF_MASTR: 19;

      then

       A2: not aa in ( UsedIntLoc i) by A1;

      ( InsCode i) <= 12 by SCMFSA_2: 16;

      then ( InsCode i) = 0 or ... or ( InsCode i) = 12;

      per cases ;

        suppose ( InsCode i) = 0 ;

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

        hence thesis;

      end;

        suppose ( InsCode i) = 1;

        then

        consider a,b be Int-Location such that

         A3: i = (a := b) by SCMFSA_2: 30;

        ( UsedIntLoc i) = {a, b} by A3, SF_MASTR: 14;

        then a in ( UsedIntLoc i) by TARSKI:def 2;

        hence thesis by A2, A3, SCMFSA7B: 6;

      end;

        suppose ( InsCode i) = 2;

        then

        consider a,b be Int-Location such that

         A4: i = ( AddTo (a,b)) by SCMFSA_2: 31;

        ( UsedIntLoc i) = {a, b} by A4, SF_MASTR: 14;

        then a in ( UsedIntLoc i) by TARSKI:def 2;

        hence thesis by A2, A4, SCMFSA7B: 7;

      end;

        suppose ( InsCode i) = 3;

        then

        consider a,b be Int-Location such that

         A5: i = ( SubFrom (a,b)) by SCMFSA_2: 32;

        ( UsedIntLoc i) = {a, b} by A5, SF_MASTR: 14;

        then a in ( UsedIntLoc i) by TARSKI:def 2;

        hence thesis by A2, A5, SCMFSA7B: 8;

      end;

        suppose ( InsCode i) = 4;

        then

        consider a,b be Int-Location such that

         A6: i = ( MultBy (a,b)) by SCMFSA_2: 33;

        ( UsedIntLoc i) = {a, b} by A6, SF_MASTR: 14;

        then a in ( UsedIntLoc i) by TARSKI:def 2;

        hence thesis by A2, A6, SCMFSA7B: 9;

      end;

        suppose ( InsCode i) = 5;

        then

        consider a,b be Int-Location such that

         A7: i = ( Divide (a,b)) by SCMFSA_2: 34;

        

         A8: ( UsedIntLoc i) = {a, b} by A7, SF_MASTR: 14;

        then

         A9: b in ( UsedIntLoc i) by TARSKI:def 2;

        a in ( UsedIntLoc i) by A8, TARSKI:def 2;

        hence thesis by A2, A7, A9, SCMFSA7B: 10;

      end;

        suppose ( InsCode i) = 6;

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

        hence thesis;

      end;

        suppose ( InsCode i) = 7;

        then ex l be Nat, a be Int-Location st i = (a =0_goto l) by SCMFSA_2: 36;

        hence thesis;

      end;

        suppose ( InsCode i) = 8;

        then ex l be Nat, a be Int-Location st i = (a >0_goto l) by SCMFSA_2: 37;

        hence thesis;

      end;

        suppose ( InsCode i) = 9;

        then

        consider a,b be Int-Location, f be FinSeq-Location such that

         A10: i = (b := (f,a)) by SCMFSA_2: 38;

        ( UsedIntLoc i) = {a, b} by A10, SF_MASTR: 17;

        then b in ( UsedIntLoc i) by TARSKI:def 2;

        hence thesis by A2, A10, SCMFSA7B: 14;

      end;

        suppose ( InsCode i) = 10;

        then ex a,b be Int-Location, f be FinSeq-Location st i = ((f,a) := b) by SCMFSA_2: 39;

        hence thesis by SCMFSA7B: 15;

      end;

        suppose ( InsCode i) = 11;

        then

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

         A11: i = (a :=len f) by SCMFSA_2: 40;

        ( UsedIntLoc i) = {a} by A11, SF_MASTR: 18;

        then a in ( UsedIntLoc i) by TARSKI:def 1;

        hence thesis by A2, A11, SCMFSA7B: 16;

      end;

        suppose ( InsCode i) = 12;

        then ex a be Int-Location, f be FinSeq-Location st i = (f :=<0,...,0> a) by SCMFSA_2: 41;

        hence thesis by SCMFSA7B: 17;

      end;

    end;

    begin

    reserve s,S for State of SCM+FSA ,

I,J for Program of SCM+FSA ,

Ig for good Program of SCM+FSA ,

i for good sequential Instruction of SCM+FSA ,

j for sequential Instruction of SCM+FSA ,

a,b for Int-Location,

f for FinSeq-Location;

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

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

    ::$Canceled

    theorem :: SFMASTR1:3

    

     Th2: for I,J be really-closed Program of SCM+FSA holds I is_halting_on (( Initialized S),P) & J is_halting_on (( IExec (I,P,S)),P) implies (I ";" J) is_halting_on (( Initialized S),P)

    proof

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

      assume that

       A1: I is_halting_on (( Initialized S),P) and

       A2: J is_halting_on (( IExec (I,P,S)),P);

      set s = ( Initialize ( Initialized S)), p = (P +* (I ";" J));

      

       A3: (I ";" J) c= p by FUNCT_4: 25;

      ( Directed I) c= (I ";" J) by SCMFSA6A: 16;

      then ( Directed I) c= p by A3, XBOOLE_1: 1;

      then

       A4: (p +* ( Directed I)) = p by FUNCT_4: 98;

      

       A5: ( DataPart ( Initialized S)) = ( DataPart s) by MEMSTR_0: 79;

      then

       A6: I is_halting_on (s,p) by A1, SCMFSA8B: 5;

      then

       A7: (p +* I) halts_on ( Initialize s);

      set s1 = ( Initialize s), p1 = (p +* I);

      

       A8: (( Initialized S) . ( intloc 0 )) = 1 by SCMFSA_M: 9;

      then (s . ( intloc 0 )) = 1 by A5, SCMFSA_M: 2;

      then

       A9: s1 = ( Initialized s) by SCMFSA_M: 18;

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

      set s3 = ( Initialize ( Comput (p1,s1,( LifeSpan (p1,s1))))), p3 = (p1 +* J);

      

       A10: J c= p3 by FUNCT_4: 25;

      set m3 = ( LifeSpan (p3,s3));

      ( DataPart ( IExec (I,P,S))) = ( DataPart ( IExec (I,P,( Initialized S)))) by SCMFSA8C: 3

      .= ( DataPart ( IExec (I,p,s))) by A1, A5, A8, SCMFSA8C: 20

      .= ( DataPart ( Result ((p +* I),( Initialized s)))) by SCMFSA6B:def 1

      .= ( DataPart ( Result ((p +* I),( Initialized s))))

      .= ( DataPart ( Comput (p1,s1,( LifeSpan (p1,s1))))) by A9, A7, EXTPRO_1: 23;

      then J is_halting_on (( Comput (p1,s1,( LifeSpan (p1,s1)))),p1) by A2, SCMFSA8B: 5;

      then

       A11: p3 halts_on s3;

      

       A12: ( Reloc (J,( card I))) c= (I ";" J) by SCMFSA6A: 38;

      set m1 = ( LifeSpan (p1,s1));

      set s4 = ( Comput (p,s,(m1 + 1))), p4 = p;

      

       A13: ( Reloc (J,( card I))) c= p by A3, A12, XBOOLE_1: 1;

      reconsider m = ((m1 + 1) + m3) as Element of NAT by ORDINAL1:def 12;

      reconsider kk = ( DataPart JAt) as Function;

      

       A14: ( DataPart s3) = (( DataPart ( Comput (p1,s1,m1))) +* kk) by FUNCT_4: 71;

      take m;

      ( IC ( Comput (p,s,m))) in NAT ;

      hence ( IC ( Comput (p,s,m))) in ( dom p) by PARTFUN1:def 2;

      

       A15: ( IC s4) = ( card I) by A6, A4, SCMFSA8A: 22;

      

       A16: ( Comput (p,s,((m1 + 1) + m3))) = ( Comput (p,( Comput (p,s,(m1 + 1))),m3)) by EXTPRO_1: 4;

      ( DataPart JAt) = {} by MEMSTR_0: 20;

      then ( DataPart ( Comput (p1,s1,m1))) = ( DataPart s3) by A14, FUNCT_4: 98, XBOOLE_1: 2;

      then ( DataPart s4) = ( DataPart s3) by A6, A4, SCMFSA8A: 22;

      then ( IncAddr (( CurInstr (p3,( Comput (p3,s3,m3)))),( card I))) = ( CurInstr (p,( Comput (p,s4,m3)))) by A15, A13, A10, SCMFSA8C: 16;

      then ( IncAddr (( CurInstr (p3,( Comput (p3,s3,m3)))),( card I))) = ( CurInstr (p,( Comput (p,s,((m1 + 1) + m3))))) by A16;

      

      then ( CurInstr (p,( Comput (p,s,m)))) = ( IncAddr (( halt SCM+FSA ),( card I))) by A11, EXTPRO_1:def 15

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

      hence thesis;

    end;

    theorem :: SFMASTR1:4

    

     Th3: for I be really-closed Program of SCM+FSA holds for s be 0 -started State of SCM+FSA st I c= p & p halts_on s holds for m be Nat st m <= ( LifeSpan (p,s)) holds ( Comput (p,s,m)) = ( Comput ((p +* (I ";" J)),s,m))

    proof

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

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

      assume that

       A1: I c= p and

       A2: p halts_on s;

      defpred X[ Nat] means $1 <= ( LifeSpan (p,s)) implies ( Comput (p,s,$1)) = ( Comput ((p +* (I ";" J)),s,$1));

      

       A3: for m be Nat st X[m] holds X[(m + 1)]

      proof

        ( dom (I ";" J)) = (( dom I) \/ ( dom ( Reloc (J,( card I))))) by SCMFSA6A: 39;

        then

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

        set sIJ = s, pIJ = (p +* (I ";" J));

        

         A5: (I ";" J) c= pIJ by FUNCT_4: 25;

        let m be Nat;

        assume

         A6: m <= ( LifeSpan (p,s)) implies ( Comput (p,s,m)) = ( Comput ((p +* (I ";" J)),s,m));

        

         A7: ( Comput (pIJ,sIJ,(m + 1))) = ( Following (pIJ,( Comput (pIJ,sIJ,m)))) by EXTPRO_1: 3;

        

         A8: ( Comput (p,s,(m + 1))) = ( Following (p,( Comput (p,s,m)))) by EXTPRO_1: 3;

        

         A9: (p /. ( IC ( Comput (p,s,m)))) = (p . ( IC ( Comput (p,s,m)))) by PBOOLE: 143;

        assume

         A10: (m + 1) <= ( LifeSpan (p,s));

        then

         A11: ( IC ( Comput (p,s,m))) = ( IC ( Comput (pIJ,sIJ,m))) by A6, NAT_1: 13;

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

        then ( IC s) in ( dom I) by AFINSQ_1: 65;

        then

         A12: ( IC ( Comput (p,s,m))) in ( dom I) by A1, AMISTD_1: 21;

        

         A13: ( CurInstr (p,( Comput (p,s,m)))) = (I . ( IC ( Comput (p,s,m)))) by A12, A9, A1, GRFUNC_1: 2;

        

         A14: (pIJ /. ( IC ( Comput (pIJ,sIJ,m)))) = (pIJ . ( IC ( Comput (pIJ,sIJ,m)))) by PBOOLE: 143;

        m < ( LifeSpan (p,s)) by A10, NAT_1: 13;

        then (I . ( IC ( Comput (p,s,m)))) <> ( halt SCM+FSA ) by A2, A13, EXTPRO_1:def 15;

        

        then ( CurInstr (p,( Comput (p,s,m)))) = ((I ";" J) . ( IC ( Comput (p,s,m)))) by A12, A13, SCMFSA6A: 15

        .= ( CurInstr (pIJ,( Comput (pIJ,sIJ,m)))) by A11, A12, A4, A14, A5, GRFUNC_1: 2;

        hence thesis by A6, A10, A8, A7, NAT_1: 13;

      end;

      

       A15: X[ 0 ];

      thus for n be Nat holds X[n] from NAT_1:sch 2( A15, A3);

    end;

    

     Lm1: for I be good really-closed Program of SCM+FSA , J be really-closed Program of SCM+FSA , s be State of SCM+FSA st (s . ( intloc 0 )) = 1 & I is_halting_on (s,p) & J is_halting_on (( IExec (I,p,s)),p) & ( Initialize (( intloc 0 ) .--> 1)) c= s & (I ";" J) c= p holds ( IC ( Comput (p,s,(( LifeSpan ((p +* I),s)) + 1)))) = ( card I) & ( DataPart ( Comput (p,s,(( LifeSpan ((p +* I),s)) + 1)))) = ( DataPart ( Initialized ( Comput ((p +* I),s,( LifeSpan ((p +* I),s)))))) & ( Reloc (J,( card I))) c= p & (( Comput (p,s,(( LifeSpan ((p +* I),s)) + 1))) . ( intloc 0 )) = 1 & p halts_on s & ( LifeSpan (p,s)) = ((( LifeSpan ((p +* I),s)) + 1) + ( LifeSpan (((p +* I) +* J),( Initialized ( Result ((p +* I),s)))))) & (J is good implies (( Result (p,s)) . ( intloc 0 )) = 1)

    proof

      let I be good really-closed Program of SCM+FSA , J be really-closed Program of SCM+FSA , s be State of SCM+FSA such that

       A1: (s . ( intloc 0 )) = 1 and

       A2: I is_halting_on (s,p) and

       A3: J is_halting_on (( IExec (I,p,s)),p);

      set s1 = s, p1 = (p +* I);

      set m1 = ( LifeSpan (p1,s1));

      set s4 = ( Comput (p,s,(m1 + 1))), p4 = p;

      assume

       A4: ( Initialize (( intloc 0 ) .--> 1)) c= s;

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

      then

       A5: SAt c= s;

      

       A6: s = (s +* SAt) by A5, FUNCT_4: 98

      .= ( Initialize s);

      then

       A7: (p +* I) halts_on s by A2;

      assume

       A8: (I ";" J) c= p;

      ( Directed I) c= (I ";" J) by SCMFSA6A: 16;

      then ( Directed I) c= p by A8, XBOOLE_1: 1;

      then

       A9: (p +* ( Directed I)) = p by FUNCT_4: 98;

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

      then ( Start-At ( 0 , SCM+FSA )) c= s;

      then s = ( Initialize s) by FUNCT_4: 98;

      hence

       A10: ( IC s4) = ( card I) by A2, A9, SCMFSA8A: 22;

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

      set InJ = ( Initialize (( intloc 0 ) .--> 1));

      set s3 = ( Initialized ( Comput (p1,s1,m1))), p3 = (p1 +* J);

      

       A11: J c= p3 by FUNCT_4: 25;

      reconsider kk = ( DataPart JAt) as Function;

      

       A12: ( DataPart JAt) = {} by MEMSTR_0: 20;

      (( Comput (p1,s1,m1)) . ( intloc 0 )) = (s . ( intloc 0 )) by A6, SCMFSA8C: 68;

      then

       A13: s3 = ( Initialize ( Comput (p1,s1,m1))) by A1, SCMFSA_M: 18;

      then ( DataPart s3) = (( DataPart ( Comput (p1,s1,m1))) +* kk) by FUNCT_4: 71;

      then ( DataPart ( Comput (p1,s1,m1))) = ( DataPart s3) by A12, FUNCT_4: 98, XBOOLE_1: 2;

      hence

       A14: ( DataPart s4) = ( DataPart s3) by A2, A6, A9, SCMFSA8A: 22;

      

       A15: ( Reloc (J,( card I))) c= (I ";" J) by SCMFSA6A: 38;

      

       A16: ( intloc 0 ) in ( dom InJ) by SCMFSA_M: 10;

      

       A17: s1 = (s +* ( Initialize (( intloc 0 ) .--> 1))) by A4, FUNCT_4: 98;

      ( DataPart ( IExec (I,p,s))) = ( DataPart ( Result ((p +* I),( Initialized s)))) by SCMFSA6B:def 1

      .= ( DataPart ( Comput (p1,s1,( LifeSpan (p1,s1))))) by A7, A17, EXTPRO_1: 23;

      then J is_halting_on (( Comput (p1,s1,( LifeSpan (p1,s1)))),p1) by A3, SCMFSA8B: 5;

      then

       A18: p3 halts_on s3 by A13;

      (I ";" J) c= p by A8;

      then ( Reloc (J,( card I))) c= p by A15, XBOOLE_1: 1;

      then ( Reloc (J,( card I))) c= p;

      hence ( Reloc (J,( card I))) c= p;

      

       A19: ( Reloc (J,( card I))) c= p by A8, A15, XBOOLE_1: 1;

      ( intloc 0 ) in Int-Locations by AMI_2:def 16;

      then

       A20: ( intloc 0 ) in D by SCMFSA_2: 100, XBOOLE_0:def 3;

      

      hence (s4 . ( intloc 0 )) = (( DataPart s3) . ( intloc 0 )) by A14, FUNCT_1: 49

      .= (s3 . ( intloc 0 )) by A20, FUNCT_1: 49

      .= 1 by A16, FUNCT_4: 13, SCMFSA_M: 12;

      set m3 = ( LifeSpan (p3,s3));

      reconsider m = ((m1 + 1) + m3) as Element of NAT by ORDINAL1:def 12;

      

       A21: ( Comput (p,s,((m1 + 1) + m3))) = ( Comput (p,( Comput (p,s,(m1 + 1))),m3)) by EXTPRO_1: 4;

      ( IncAddr (( CurInstr (p3,( Comput (p3,s3,m3)))),( card I))) = ( CurInstr (p,( Comput (p,s4,m3)))) by A10, A14, A19, A11, SCMFSA8C: 16;

      then ( IncAddr (( CurInstr (p3,( Comput (p3,s3,m3)))),( card I))) = ( CurInstr (p,( Comput (p,s,((m1 + 1) + m3))))) by A21;

      

      then

       A22: ( CurInstr (p,( Comput (p,s,m)))) = ( IncAddr (( halt SCM+FSA ),( card I))) by A18, EXTPRO_1:def 15

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

      hence

       A23: p halts_on s by EXTPRO_1: 29;

       A24:

      now

        let k be Element of NAT ;

        assume ((m1 + 1) + k) < m;

        then

         A25: k < m3 by XREAL_1: 6;

        

         A26: ( Comput (p,s,((m1 + 1) + k))) = ( Comput (p,( Comput (p,s,(m1 + 1))),k)) by EXTPRO_1: 4;

        assume

         A27: ( CurInstr (p,( Comput (p,s,((m1 + 1) + k))))) = ( halt SCM+FSA );

        

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

        ( IncAddr (( CurInstr (p3,( Comput (p3,s3,k)))),( card I))) = ( halt SCM+FSA ) by A27, A26, A10, A14, A19, A11, SCMFSA8C: 16;

        then ( InsCode ( CurInstr (p3,( Comput (p3,s3,k))))) = 0 by A28, COMPOS_0:def 9;

        then ( CurInstr (p3,( Comput (p3,s3,k)))) = ( halt SCM+FSA ) by SCMFSA_2: 95;

        hence contradiction by A18, A25, EXTPRO_1:def 15;

      end;

      now

        let k be Nat;

        assume

         A29: k < m;

        per cases ;

          suppose k <= m1;

          hence ( CurInstr (p,( Comput (p,s,k)))) <> ( halt SCM+FSA ) by A2, A6, A9, SCMFSA8A: 21;

        end;

          suppose m1 < k;

          then (m1 + 1) <= k by NAT_1: 13;

          then

          consider kk be Nat such that

           A30: ((m1 + 1) + kk) = k by NAT_1: 10;

          reconsider kk as Element of NAT by ORDINAL1:def 12;

          ((m1 + 1) + kk) = k by A30;

          hence ( CurInstr (p,( Comput (p,s,k)))) <> ( halt SCM+FSA ) by A24, A29;

        end;

      end;

      then for k be Nat st ( CurInstr (p,( Comput (p,s,k)))) = ( halt SCM+FSA ) holds m <= k;

      then

       A31: ( LifeSpan (p,s)) = m by A22, A23, EXTPRO_1:def 15;

      ( Comput ((p +* I),s,m1)) = ( Result ((p +* I),s)) by A7, EXTPRO_1: 23;

      hence ( LifeSpan (p,s)) = ((( LifeSpan ((p +* I),s)) + 1) + ( LifeSpan (((p +* I) +* J),( Initialized ( Result ((p +* I),s)))))) by A31;

      ( Start-At ( 0 , SCM+FSA )) c= s3 by FUNCT_4: 25, MEMSTR_0: 50;

      then

       A32: ( Initialize s3) = s3 by FUNCT_4: 98;

      

       A33: InJ c= s3 by FUNCT_4: 25;

      hereby

        

         A34: ( DataPart ( Comput (p3,s3,m3))) = ( DataPart ( Comput (p,s4,m3))) by A10, A14, A19, A11, SCMFSA8C: 16;

        assume

         A35: J is good;

        

        thus (( Result (p,s)) . ( intloc 0 )) = (( Comput (p,s,m)) . ( intloc 0 )) by A23, A31, EXTPRO_1: 23

        .= (( Comput (p,s4,m3)) . ( intloc 0 )) by EXTPRO_1: 4

        .= (( Comput (p3,s3,m3)) . ( intloc 0 )) by A34, SCMFSA_M: 2

        .= (s3 . ( intloc 0 )) by A32, A35, SCMFSA8C: 68

        .= 1 by A16, A33, GRFUNC_1: 2, SCMFSA_M: 12;

      end;

    end;

    theorem :: SFMASTR1:5

    

     Th4: for Ig be good really-closed Program of SCM+FSA holds for J be really-closed Program of SCM+FSA holds Ig is_halting_on (( Initialized s),p) & J is_halting_on (( IExec (Ig,p,s)),p) implies ( LifeSpan ((p +* (Ig ";" J)),( Initialized s))) = ((( LifeSpan ((p +* Ig),( Initialized s))) + 1) + ( LifeSpan (((p +* Ig) +* J),( Initialized ( Result ((p +* Ig),( Initialized s)))))))

    proof

      let Ig be good really-closed Program of SCM+FSA ;

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

      set I = Ig;

      assume that

       A1: I is_halting_on (( Initialized s),p) and

       A2: J is_halting_on (( IExec (I,p,s)),p);

      set Is = ( Initialized s);

      

       A3: (( Initialized s) . ( intloc 0 )) = 1 by SCMFSA_M: 9;

      set s1 = ( Initialized s), p1 = (p +* I);

      set m1 = ( LifeSpan (p1,s1));

      set s3 = ( Initialized ( Comput (p1,s1,m1))), p3 = (p1 +* J);

      s1 = ( Initialized Is);

      then

       A4: s1 = ( Initialize Is) by A3, SCMFSA_M: 18;

      then

       A5: p1 halts_on s1 by A1;

      then

       A6: s3 = ( Initialized ( Result (p1,s1))) by EXTPRO_1: 23;

      set s2 = ( Initialized s), p2 = (p +* (I ";" J));

      

       A7: (I ";" J) c= p2 by FUNCT_4: 25;

      

       A8: ( DataPart Is) = ( DataPart s2);

      

       A9: (s2 . ( intloc 0 )) = 1 by A3;

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

      (( Comput (p1,s1,m1)) . ( intloc 0 )) = 1 by A3, A4, SCMFSA8C: 68;

      then

       A10: ( Initialized ( Comput (p1,s1,m1))) = ( Initialize ( Comput (p1,s1,m1))) by SCMFSA_M: 18;

      then JAt c= s3 by FUNCT_4: 25;

      then

       A11: s3 = ( Initialize s3) by FUNCT_4: 98;

      ( DataPart ( IExec (I,p,s))) = ( DataPart ( Result ((p +* I),( Initialized s)))) by SCMFSA6B:def 1

      .= ( DataPart ( Result ((p +* I),( Initialized s))))

      .= ( DataPart ( Comput (p1,s1,( LifeSpan (p1,s1))))) by A5, EXTPRO_1: 23;

      then ( DataPart ( IExec (I,p,s))) = ( DataPart s3) by A10, MEMSTR_0: 79;

      then

       A12: J is_halting_on (s3,p3) by A2, SCMFSA8B: 5;

      ( Initialize s2) = s2 by MEMSTR_0: 44;

      then ( Result ((p2 +* I),s2)) = ( Result (p1,s1)) by A1, A8, SCMFSA8C: 72;

      then ( Initialized ( Result ((p2 +* I),s2))) = s3 by A6;

      then

       A13: ( DataPart ( Initialized ( Result ((p2 +* I),s2)))) = ( DataPart s3);

      

       A14: ( DataPart ( IExec (I,p,s))) = ( DataPart ( IExec (I,p,Is))) by SCMFSA8C: 3

      .= ( DataPart ( IExec (I,p2,s2))) by A1, A3, A8, SCMFSA8C: 20;

      

       A15: ( Initialize (( intloc 0 ) .--> 1)) c= ( Initialized s) by FUNCT_4: 25;

      

       A16: J is_halting_on (( IExec (I,p2,s2)),p2) by A2, A14, SCMFSA8B: 5;

      I is_halting_on (s2,p2) by A1, A8, SCMFSA8B: 5;

      then

       A17: ( LifeSpan (p2,s2)) = ((( LifeSpan ((p2 +* I),s2)) + 1) + ( LifeSpan (((p2 +* I) +* J),( Initialized ( Result ((p2 +* I),s2)))))) by A9, A16, A15, Lm1, A7;

      ( Start-At ( 0 , SCM+FSA )) c= ( Initialized ( Result ((p2 +* I),s2))) by FUNCT_4: 25, MEMSTR_0: 50;

      then

       A18: ( Initialized ( Result ((p2 +* I),s2))) = ( Initialize ( Initialized ( Result ((p2 +* I),s2)))) by FUNCT_4: 98;

      

       A19: ( LifeSpan ((p2 +* I),s2)) = m1 by A1, A4, A8, SCMFSA8C: 72;

      ( LifeSpan (((p2 +* I) +* J),( Initialized ( Result ((p2 +* I),s2))))) = ( LifeSpan (p3,s3)) by A12, A11, A18, A13, SCMFSA8C: 72;

      hence thesis by A6, A17, A19;

    end;

    theorem :: SFMASTR1:6

    

     Th5: for Ig be good really-closed Program of SCM+FSA holds for J be really-closed Program of SCM+FSA holds Ig is_halting_on (( Initialized s),p) & J is_halting_on (( IExec (Ig,p,s)),p) implies ( IExec ((Ig ";" J),p,s)) = (( IExec (J,p,( IExec (Ig,p,s)))) +* ( Start-At ((( IC ( IExec (J,p,( IExec (Ig,p,s))))) + ( card Ig)), SCM+FSA )))

    proof

      let Ig be good really-closed Program of SCM+FSA ;

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

      set I = Ig;

      assume that

       A1: I is_halting_on (( Initialized s),p) and

       A2: J is_halting_on (( IExec (I,p,s)),p);

      set Is = ( Initialized s), Ip = p;

      

       A3: (( Initialized s) . ( intloc 0 )) = 1 by SCMFSA_M: 9;

      set s1 = ( Initialized s), p1 = (p +* I);

      

       A4: I c= p1 by FUNCT_4: 25;

      set m1 = ( LifeSpan (p1,s1));

      s1 = ( Initialized Is);

      then

       A5: s1 = ( Initialize Is) by A3, SCMFSA_M: 18;

      set s3 = ( Initialized ( Comput (p1,s1,m1))), p3 = (p1 +* J);

      

       A6: J c= p3 by FUNCT_4: 25;

      

       A7: p1 halts_on s1 by A1, A5;

      then

       A8: s3 = ( Initialized ( Result (p1,s1))) by EXTPRO_1: 23;

      set s2 = ( Initialized s), p2 = (p +* (I ";" J));

      

       A9: (I ";" J) c= p2 by FUNCT_4: 25;

      s2 = ( Initialized Is);

      then

       A10: s2 = ( Initialize Is) by A3, SCMFSA_M: 18;

      

       A11: ( DataPart Is) = ( DataPart s2);

      

       A12: (s2 . ( intloc 0 )) = 1 by A3;

      

       A13: ( DataPart ( IExec (I,p,s))) = ( DataPart ( IExec (I,p,Is))) by SCMFSA8C: 3

      .= ( DataPart ( IExec (I,p2,s2))) by A1, A3, A11, SCMFSA8C: 20;

      s2 = ( Initialize s2) by MEMSTR_0: 44;

      then

       A14: ( LifeSpan ((p2 +* I),s2)) = m1 by A1, A11, SCMFSA8C: 72;

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

      (( Comput (p1,s1,m1)) . ( intloc 0 )) = 1 by A3, A5, SCMFSA8C: 68;

      then

       A15: s3 = ( Initialize ( Comput (p1,s1,m1))) by SCMFSA_M: 18;

      set m3 = ( LifeSpan (p3,s3));

      (I ";" J) is_halting_on (Is,Ip) by A1, A2, Th2;

      then

       A16: p2 halts_on s2 by A10;

      

       A17: ( IExec ((I ";" J),p,s)) = ( Result ((p +* (I ";" J)),( Initialized s))) by SCMFSA6B:def 1

      .= ( Comput (p2,s2,( LifeSpan (p2,s2)))) by A16, EXTPRO_1: 23

      .= ( Comput (p2,s2,((m1 + 1) + m3))) by A1, A2, A8, Th4;

      

       A18: ( DataPart ( IExec (I,p,s))) = ( DataPart ( Result ((p +* I),( Initialized s)))) by SCMFSA6B:def 1

      .= ( DataPart ( Result ((p +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))))

      .= ( DataPart ( Comput (p1,s1,( LifeSpan (p1,s1))))) by A7, EXTPRO_1: 23;

      then J is_halting_on (( Comput (p1,s1,( LifeSpan (p1,s1)))),p1) by A2, SCMFSA8B: 5;

      then

       A19: p3 halts_on s3 by A15;

      set IEJIs = ( IExec (J,p,( IExec (I,p,s))));

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

      

       A20: ( Initialize (( intloc 0 ) .--> 1)) c= s2 by FUNCT_4: 25;

      (( IExec (I,p,s)) . ( intloc 0 )) = 1 by A1, SCMFSA8C: 67;

      then

       A21: ( Initialized ( IExec (I,p,s))) = ( Initialize ( IExec (I,p,s))) by SCMFSA_M: 18;

      then ( Result ((p1 +* J),(( Result (p1,s1)) +* ( Initialize (( intloc 0 ) .--> 1))))) = ( Result ((p +* J),(( IExec (I,p,s)) +* ( Initialize (( intloc 0 ) .--> 1))))) by A2, A15, A18, A8, SCMFSA8C: 72;

      then

       A22: ( IC ( Result ((p1 +* J),( Initialized ( Result (p1,s1)))))) = ( IC ( Result ((p +* J),( Initialized ( IExec (I,p,s))))));

      

       A23: ( Result ((p +* J),( Initialized ( IExec (I,p,s))))) = ( Result (p3,s3)) by A2, A15, A18, A21, SCMFSA8C: 72;

      

       A24: IEJIs = ( Result ((p +* J),( Initialized ( IExec (I,p,s))))) by SCMFSA6B:def 1

      .= ( Comput (p3,s3,m3)) by A19, A23, EXTPRO_1: 23;

      

       A25: I is_halting_on (s2,p2) by A1, A11, SCMFSA8B: 5;

      reconsider l = (( IC IEJIs) + ( card I)) as Element of NAT ;

      reconsider s2t = (s +* (( intloc 0 ) .--> 1)) as State of SCM+FSA ;

      

       A27: (I +* (I ";" J)) = (I ";" J) by SCMFSA6A: 18;

      

       A28: ((p2 +* I) +* (I ";" J)) = (p2 +* (I +* (I ";" J))) by FUNCT_4: 14;

      

       A29: I c= (p2 +* I) by FUNCT_4: 25;

      

       A30: (p1 +* (I ";" J)) = p2 by A27, FUNCT_4: 14;

      

       A31: ( Comput (p1,s1,m1)) = ( Comput (p2,s2,m1)) by A7, Th3, A4, A30;

      s2 = ( Initialize s2) by MEMSTR_0: 44;

      then (p2 +* I) halts_on s2 by A25;

      then ( Comput ((p2 +* I),s2,m1)) = ( Comput (((p2 +* I) +* (I ";" J)),s2,m1)) by A14, Th3, A29;

      

      then ( DataPart ( Comput ((p2 +* I),s2,m1))) = ( DataPart ( Comput (((p2 +* I) +* (I ";" J)),s2,m1)))

      .= ( DataPart ( Comput (((p2 +* I) +* (I ";" J)),s2,m1)))

      .= ( DataPart ( Comput ((p2 +* (I ";" J)),s2,m1))) by A27, A28

      .= ( DataPart ( Comput (p2,s2,m1)))

      .= ( DataPart ( Comput (p1,s1,m1))) by A31;

      

      then

       A32: ( DataPart (( Comput ((p2 +* I),s2,m1)) +* ( Initialize (( intloc 0 ) .--> 1)))) = (( DataPart ( Comput (p1,s1,m1))) +* ( DataPart ( Initialize (( intloc 0 ) .--> 1)))) by FUNCT_4: 71

      .= ( DataPart (( Comput (p1,s1,m1)) +* ( Initialize (( intloc 0 ) .--> 1)))) by FUNCT_4: 71;

      

       A33: J is_halting_on (( IExec (I,p2,s2)),p2) by A2, A13, SCMFSA8B: 5;

      then

       A34: ( DataPart ( Comput (p2,s2,(m1 + 1)))) = ( DataPart ( Initialized ( Comput ((p2 +* I),s2,m1)))) by A20, A25, A14, A12, Lm1, A9;

      ( Reloc (J,( card I))) c= (I ";" J) by SCMFSA6A: 38;

      then

       A35: ( Reloc (J,( card I))) c= p2 by A9, XBOOLE_1: 1;

      

       A36: ( IC ( Comput (p2,s2,(m1 + 1)))) = ( card I) by A20, A25, A14, A12, A33, Lm1, A9;

      then

       A37: ( DataPart ( Comput (p2,( Comput (p2,s2,(m1 + 1))),m3))) = ( DataPart ( Comput (p3,s3,m3))) by A32, A34, A6, A35, SCMFSA8C: 16;

      

       A38: ( DataPart ( IExec ((I ";" J),p,s))) = ( DataPart ( Comput (p2,s2,((m1 + 1) + m3)))) by A17

      .= ( DataPart ( Comput (p3,s3,m3))) by A37, EXTPRO_1: 4

      .= ( DataPart IEJIs) by A24;

      

       A39: ( IC ( Comput (p2,( Comput (p2,s2,(m1 + 1))),m3))) = (( IC ( Comput (p3,s3,m3))) + ( card I)) by A32, A36, A34, A6, A35, SCMFSA8C: 16;

      

       A40: s3 = ( Initialized ( Result (p1,s1))) by A7, EXTPRO_1: 23;

      

       A41: ( IC ( IExec ((I ";" J),p,s))) = ( IC ( Result ((p +* (I ";" J)),( Initialized s)))) by SCMFSA6B:def 1

      .= ( IC ( Comput (p2,s2,( LifeSpan (p2,s2))))) by A16, EXTPRO_1: 23

      .= ( IC ( Comput (p2,s2,((m1 + 1) + m3)))) by A1, A2, A8, Th4

      .= (( IC ( Comput (p3,s3,m3))) + ( card I)) by A39, EXTPRO_1: 4

      .= (( IC ( Result (p3,s3))) + ( card I)) by A19, EXTPRO_1: 23

      .= (( IC IEJIs) + ( card I)) by A22, A40, SCMFSA6B:def 1;

       A42:

      now

        let x be object;

        assume

         A43: x in ( dom ( IExec ((I ";" J),p,s)));

        per cases by A43, SCMFSA_M: 1;

          suppose

           A44: x is Int-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 56;

          then

           A45: not x in ( dom ( Start-At (l, SCM+FSA ))) by TARSKI:def 1;

          (( IExec ((I ";" J),p,s)) . x) = (IEJIs . x) by A38, A44, SCMFSA_M: 2;

          hence (( IExec ((I ";" J),p,s)) . x) = ((IEJIs +* ( Start-At ((( IC IEJIs) + ( card I)), SCM+FSA ))) . x) by A45, FUNCT_4: 11;

        end;

          suppose

           A46: x is FinSeq-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 57;

          then

           A47: not x in ( dom ( Start-At (l, SCM+FSA ))) by TARSKI:def 1;

          (( IExec ((I ";" J),p,s)) . x) = (IEJIs . x) by A38, A46, SCMFSA_M: 2;

          hence (( IExec ((I ";" J),p,s)) . x) = ((IEJIs +* ( Start-At ((( IC IEJIs) + ( card I)), SCM+FSA ))) . x) by A47, FUNCT_4: 11;

        end;

          suppose

           A48: x = ( IC SCM+FSA );

          then x in {( IC SCM+FSA )} by TARSKI:def 1;

          then

           A49: x in ( dom ( Start-At (l, SCM+FSA )));

          

          thus (( IExec ((I ";" J),p,s)) . x) = (( Start-At (l, SCM+FSA )) . ( IC SCM+FSA )) by A41, A48, FUNCOP_1: 72

          .= ((IEJIs +* ( Start-At ((( IC IEJIs) + ( card I)), SCM+FSA ))) . x) by A48, A49, FUNCT_4: 13;

        end;

      end;

      ( dom ( IExec ((I ";" J),p,s))) = the carrier of SCM+FSA by PARTFUN1:def 2

      .= ( dom (IEJIs +* ( Start-At ((( IC IEJIs) + ( card I)), SCM+FSA )))) by PARTFUN1:def 2;

      hence thesis by A42, FUNCT_1: 2;

    end;

    theorem :: SFMASTR1:7

    

     Th6: for Ig be good really-closed Program of SCM+FSA holds for J be really-closed Program of SCM+FSA holds (Ig is parahalting or Ig is_halting_on (( Initialized s),p)) & (J is parahalting or J is_halting_on (( IExec (Ig,p,s)),p)) implies (( IExec ((Ig ";" J),p,s)) . a) = (( IExec (J,p,( IExec (Ig,p,s)))) . a)

    proof

      let Ig be good really-closed Program of SCM+FSA ;

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

      set I = Ig;

      assume that

       A1: I is parahalting or I is_halting_on (( Initialized s),p) and

       A2: J is parahalting or J is_halting_on (( IExec (I,p,s)),p);

      

       A3: J is_halting_on (( IExec (I,p,s)),p) by A2, SCMFSA7B: 19;

      

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

      I is_halting_on (( Initialized s),p) by A1, SCMFSA7B: 19;

      then ( IExec ((I ";" J),p,s)) = (( IExec (J,p,( IExec (I,p,s)))) +* ( Start-At ((( IC ( IExec (J,p,( IExec (I,p,s))))) + ( card I)), SCM+FSA ))) by A3, Th5;

      hence thesis by A4, FUNCT_4: 11;

    end;

    theorem :: SFMASTR1:8

    

     Th7: for Ig be good really-closed Program of SCM+FSA holds for J be really-closed Program of SCM+FSA holds (Ig is parahalting or Ig is_halting_on (( Initialized s),p)) & (J is parahalting or J is_halting_on (( IExec (Ig,p,s)),p)) implies (( IExec ((Ig ";" J),p,s)) . f) = (( IExec (J,p,( IExec (Ig,p,s)))) . f)

    proof

      let Ig be good really-closed Program of SCM+FSA ;

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

      set I = Ig;

      assume that

       A1: I is parahalting or I is_halting_on (( Initialized s),p) and

       A2: J is parahalting or J is_halting_on (( IExec (I,p,s)),p);

      

       A3: J is_halting_on (( IExec (I,p,s)),p) by A2, SCMFSA7B: 19;

      

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

      I is_halting_on (( Initialized s),p) by A1, SCMFSA7B: 19;

      then ( IExec ((I ";" J),p,s)) = (( IExec (J,p,( IExec (I,p,s)))) +* ( Start-At ((( IC ( IExec (J,p,( IExec (I,p,s))))) + ( card I)), SCM+FSA ))) by A3, Th5;

      hence thesis by A4, FUNCT_4: 11;

    end;

    theorem :: SFMASTR1:9

    for Ig be good really-closed Program of SCM+FSA holds for J be really-closed Program of SCM+FSA holds (Ig is parahalting or Ig is_halting_on (( Initialized s),p)) & (J is parahalting or J is_halting_on (( IExec (Ig,p,s)),p)) implies ( DataPart ( IExec ((Ig ";" J),p,s))) = ( DataPart ( IExec (J,p,( IExec (Ig,p,s)))))

    proof

      let Ig be good really-closed Program of SCM+FSA ;

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

      set I = Ig;

      assume that

       A1: I is parahalting or I is_halting_on (( Initialized s),p) and

       A2: J is parahalting or J is_halting_on (( IExec (I,p,s)),p);

      

       A3: for f holds (( IExec ((I ";" J),p,s)) . f) = (( IExec (J,p,( IExec (I,p,s)))) . f) by A1, A2, Th7;

      for a holds (( IExec ((I ";" J),p,s)) . a) = (( IExec (J,p,( IExec (I,p,s)))) . a) by A1, A2, Th6;

      hence thesis by A3, SCMFSA_M: 2;

    end;

    theorem :: SFMASTR1:10

    

     Th9: for Ig be good really-closed Program of SCM+FSA holds Ig is parahalting or Ig is_halting_on (( Initialized s),p) implies ( DataPart ( Initialized ( IExec (Ig,p,s)))) = ( DataPart ( IExec (Ig,p,s)))

    proof

      let Ig be good really-closed Program of SCM+FSA ;

      set I = Ig;

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

      assume that

       A1: I is parahalting or I is_halting_on (( Initialized s),p);

      

       A2: I is_halting_on (( Initialized s),p) by A1, SCMFSA7B: 19;

      now

        

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

        

         A4: ( dom ( Initialized IE)) = (D \/ {( IC SCM+FSA )}) by MEMSTR_0: 13

        .= (D \/ {( IC SCM+FSA )});

        

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

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

        then

         A6: ( dom ( DataPart ( Initialized IE))) = D by A3, A5, A4, XBOOLE_1: 21;

        let x be object;

        assume

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

        per cases by A7, A6, SCMFSA_2: 100, XBOOLE_0:def 3;

          suppose x in Int-Locations ;

          then

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

          hereby

            per cases ;

              suppose

               A8: x9 is read-write;

              

              thus (( DataPart ( Initialized IE)) . x) = (( Initialized IE) . x) by A7, A6, FUNCT_1: 49

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

            end;

              suppose x9 is read-only;

              then

               A9: x9 = ( intloc 0 );

              

              thus (( DataPart ( Initialized IE)) . x) = (( Initialized IE) . x9) by A7, A6, FUNCT_1: 49

              .= 1 by A9, SCMFSA_M: 9

              .= (IE . x) by A2, A9, SCMFSA8C: 67;

            end;

          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 A7, A6, FUNCT_1: 49

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

        end;

      end;

      hence thesis by FUNCT_1: 46;

    end;

    theorem :: SFMASTR1:11

    

     Th10: for Ig be good really-closed Program of SCM+FSA holds Ig is parahalting or Ig is_halting_on (( Initialized s),p) implies (( IExec ((Ig ";" j),p,s)) . a) = (( Exec (j,( IExec (Ig,p,s)))) . a)

    proof

      let Ig be good really-closed Program of SCM+FSA ;

      set I = Ig;

      set Mj = ( Macro j);

      a in Int-Locations by AMI_2:def 16;

      then

       A1: a in D by SCMFSA_2: 100, XBOOLE_0:def 3;

      assume that

       A2: I is parahalting or I is_halting_on (( Initialized s),p);

      

       A3: ( DataPart ( Initialized ( IExec (I,p,s)))) = ( DataPart ( IExec (I,p,s))) by A2, Th9;

      

      thus (( IExec ((I ";" j),p,s)) . a) = (( IExec (Mj,p,( IExec (I,p,s)))) . a) by A2, Th6

      .= (( IExec (Mj,p,( IExec (I,p,s)))) . a)

      .= (( Exec (j,( Initialized ( IExec (I,p,s))))) . a) by SCMFSA6C: 5

      .= (( Exec (j,( Initialized ( IExec (I,p,s))))) . a)

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

      .= (( DataPart ( Exec (j,( IExec (I,p,s))))) . a) by A3, SCMFSA6C: 4

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

    end;

    theorem :: SFMASTR1:12

    

     Th11: for Ig be good really-closed Program of SCM+FSA holds Ig is parahalting or Ig is_halting_on (( Initialized s),p) implies (( IExec ((Ig ";" j),p,s)) . f) = (( Exec (j,( IExec (Ig,p,s)))) . f)

    proof

      let Ig be good really-closed Program of SCM+FSA ;

      set I = Ig;

      set Mj = ( Macro j);

      f in FinSeq-Locations by SCMFSA_2:def 5;

      then

       A1: f in D by SCMFSA_2: 100, XBOOLE_0:def 3;

      assume that

       A2: I is parahalting or I is_halting_on (( Initialized s),p);

      

       A3: ( DataPart ( Initialized ( IExec (I,p,s)))) = ( DataPart ( IExec (I,p,s))) by A2, Th9;

      

      thus (( IExec ((I ";" j),p,s)) . f) = (( IExec (Mj,p,( IExec (I,p,s)))) . f) by A2, Th7

      .= (( IExec (Mj,p,( IExec (I,p,s)))) . f)

      .= (( Exec (j,( Initialized ( IExec (I,p,s))))) . f) by SCMFSA6C: 5

      .= (( Exec (j,( Initialized ( IExec (I,p,s))))) . f)

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

      .= (( DataPart ( Exec (j,( IExec (I,p,s))))) . f) by A3, SCMFSA6C: 4

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

    end;

    theorem :: SFMASTR1:13

    for Ig be good really-closed Program of SCM+FSA holds Ig is parahalting or Ig is_halting_on (( Initialized s),p) implies ( DataPart ( IExec ((Ig ";" j),p,s))) = ( DataPart ( Exec (j,( IExec (Ig,p,s)))))

    proof

      let Ig be good really-closed Program of SCM+FSA ;

      set I = Ig;

      assume

       A1: I is parahalting or I is_halting_on (( Initialized s),p);

      then

       A2: for f holds (( IExec ((I ";" j),p,s)) . f) = (( Exec (j,( IExec (I,p,s)))) . f) by Th11;

      for a holds (( IExec ((I ";" j),p,s)) . a) = (( Exec (j,( IExec (I,p,s)))) . a) by A1, Th10;

      hence thesis by A2, SCMFSA_M: 2;

    end;

    theorem :: SFMASTR1:14

    

     Th13: for J be really-closed Program of SCM+FSA holds J is parahalting or J is_halting_on (( Exec (i,( Initialized s))),p) implies (( IExec ((i ";" J),p,s)) . a) = (( IExec (J,p,( Exec (i,( Initialized s))))) . a)

    proof

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

      set Mi = ( Macro i);

      

       A1: ( IExec (Mi,p,s)) = ( Exec (i,( Initialized s))) by SCMFSA6C: 5;

      assume J is parahalting or J is_halting_on (( Exec (i,( Initialized s))),p);

      then

       A2: J is_halting_on (( Exec (i,( Initialized s))),p) by SCMFSA7B: 19;

      J is_halting_on (( IExec (Mi,p,s)),p) by A2, A1;

      

      hence (( IExec ((i ";" J),p,s)) . a) = (( IExec (J,p,( IExec (Mi,p,s)))) . a) by Th6

      .= (( IExec (J,p,( IExec (Mi,p,s)))) . a)

      .= (( IExec (J,p,( Exec (i,( Initialized s))))) . a) by A1

      .= (( IExec (J,p,( Exec (i,( Initialized s))))) . a);

    end;

    theorem :: SFMASTR1:15

    

     Th14: for J be really-closed Program of SCM+FSA holds J is parahalting or J is_halting_on (( Exec (i,( Initialized s))),p) implies (( IExec ((i ";" J),p,s)) . f) = (( IExec (J,p,( Exec (i,( Initialized s))))) . f)

    proof

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

      set Mi = ( Macro i);

      

       A1: ( IExec (Mi,p,s)) = ( Exec (i,( Initialized s))) by SCMFSA6C: 5;

      assume J is parahalting or J is_halting_on (( Exec (i,( Initialized s))),p);

      then

       A2: J is_halting_on (( Exec (i,( Initialized s))),p) by SCMFSA7B: 19;

      J is_halting_on (( IExec (Mi,p,s)),p) by A2, A1;

      

      hence (( IExec ((i ";" J),p,s)) . f) = (( IExec (J,p,( IExec (Mi,p,s)))) . f) by Th7

      .= (( IExec (J,p,( IExec (Mi,p,s)))) . f)

      .= (( IExec (J,p,( Exec (i,( Initialized s))))) . f) by A1

      .= (( IExec (J,p,( Exec (i,( Initialized s))))) . f);

    end;

    theorem :: SFMASTR1:16

    for J be really-closed Program of SCM+FSA holds J is parahalting or J is_halting_on (( Exec (i,( Initialized s))),p) implies ( DataPart ( IExec ((i ";" J),p,s))) = ( DataPart ( IExec (J,p,( Exec (i,( Initialized s))))))

    proof

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

      assume

       A1: J is parahalting or J is_halting_on (( Exec (i,( Initialized s))),p);

      then

       A2: for f holds (( IExec ((i ";" J),p,s)) . f) = (( IExec (J,p,( Exec (i,( Initialized s))))) . f) by Th14;

      for a holds (( IExec ((i ";" J),p,s)) . a) = (( IExec (J,p,( Exec (i,( Initialized s))))) . a) by A1, Th13;

      hence thesis by A2, SCMFSA_M: 2;

    end;

    begin

    reserve L for finite Subset of Int-Locations ,

m,n for Nat;

    definition

      ::$Canceled

      let n be Element of NAT , p be preProgram of SCM+FSA ;

      :: SFMASTR1:def4

      func n -thNotUsed p -> Int-Location equals (n -thRWNotIn ( UsedILoc p));

      correctness ;

    end

    notation

      let n be Element of NAT , p be preProgram of SCM+FSA ;

      synonym n -stNotUsed p for n -thNotUsed p;

      synonym n -ndNotUsed p for n -thNotUsed p;

      synonym n -rdNotUsed p for n -thNotUsed p;

    end

    registration

      let n be Element of NAT , p be preProgram of SCM+FSA ;

      cluster (n -thNotUsed p) -> read-write;

      coherence ;

    end