:: SFMASTR1 semantic presentation

begin


definition
let i be Instruction of SCM+FSA;
attri is good  means :Def1: :: SFMASTR1:def 1
 Macro i is good ;
end;

:: deftheorem Def1 defines good SFMASTR1:def_1_:_
 for i being Instruction of SCM+FSA holds
( i is good iff Macro i is good );

registration
let a be read-write Int-Location;
let b be Int-Location;
clustera := b ->  good ;
coherence
 a := b is good
proof
thus  Macro (a := b) is good by SCMFSA7B:6, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
cluster AddTo (a,b) ->  good ;
coherence
 AddTo (a,b) is good
proof
thus  Macro (AddTo (a,b)) is good by SCMFSA7B:7, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
cluster SubFrom (a,b) ->  good ;
coherence
 SubFrom (a,b) is good
proof
thus  Macro (SubFrom (a,b)) is good by SCMFSA7B:8, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
cluster MultBy (a,b) ->  good ;
coherence
 MultBy (a,b) is good
proof
thus  Macro (MultBy (a,b)) is good by SCMFSA7B:9, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
cluster parahalting with_explicit_jumps IC-relocable good for Element of the InstructionsF of SCM+FSA;
existence
 ex b1 being Instruction of SCM+FSA st
( b1 is good & b1 is parahalting )
proof
set a = the read-write Int-Location;
 ( the read-write Int-Location := the read-write Int-Location is good & the read-write Int-Location := the read-write Int-Location is parahalting ) ;
hence  ex b1 being Instruction of SCM+FSA st
( b1 is good & b1 is parahalting ) ; ::_thesis: verum
end;
end;

registration
let a, b be read-write Int-Location;
cluster Divide (a,b) ->  good ;
coherence
 Divide (a,b) is good
proof
thus  Macro (Divide (a,b)) is good by SCMFSA7B:10, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
let l be Element of NAT ;
cluster goto l ->  good ;
coherence
 goto l is good
proof
thus  Macro (goto l) is good by SCMFSA7B:11, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
let a be Int-Location;
let l be Element of NAT ;
clustera =0_goto l ->  good ;
coherence
 a =0_goto l is good
proof
thus  Macro (a =0_goto l) is good by SCMFSA7B:12, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
clustera >0_goto l ->  good ;
coherence
 a >0_goto l is good
proof
thus  Macro (a >0_goto l) is good by SCMFSA7B:13, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
let b be read-write Int-Location;
clusterb := (f,a) ->  good ;
coherence
 b := (f,a) is good
proof
thus  Macro (b := (f,a)) is good by SCMFSA7B:14, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
let f be FinSeq-Location ;
let b be read-write Int-Location;
clusterb :=len f ->  good ;
coherence
 b :=len f is good
proof
thus  Macro (b :=len f) is good by SCMFSA7B:16, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
let f be FinSeq-Location ;
let a be Int-Location;
clusterf :=<0,...,0> a ->  good ;
coherence
 f :=<0,...,0> a is good
proof
thus  Macro (f :=<0,...,0> a) is good by SCMFSA7B:17, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
let b be Int-Location;
cluster(f,a) := b ->  good ;
coherence
 (f,a) := b is good
proof
thus  Macro ((f,a) := b) is good by SCMFSA7B:15, SCMFSA8C:70; :: according to SFMASTR1:def_1 ::_thesis: verum
end;
end;

registration
let i be good Instruction of SCM+FSA;
cluster Macro i ->  good ;
coherence
 Macro i is good by Def1;
end;

registration
let i, j be good Instruction of SCM+FSA;
clusteri ";" j ->  good ;
coherence
 i ";" j is good ;
end;

registration
let i be good Instruction of SCM+FSA;
let I be good Program of SCM+FSA;
clusteri ";" I ->  good ;
coherence
 i ";" I is good ;
clusterI ";" i ->  good ;
coherence
 I ";" i is good ;
end;

registration
let a, b be read-write Int-Location;
cluster swap (a,b) ->  good ;
coherence
 swap (a,b) is good
proof
 swap (a,b) = (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b)))) by SCMFSA6C:def_3;
hence  swap (a,b) is good ; ::_thesis: verum
end;
end;

registration
let I be good Program of SCM+FSA;
let a be read-write Int-Location;
cluster Times (a,I) ->  good ;
coherence
 Times (a,I) is good
proof
reconsider J = if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) as good Program of SCM+FSA ;
 if>0 (a,(loop J),(Stop SCM+FSA)) is good ;
hence  Times (a,I) is good by SCMFSA8C:def_2; ::_thesis: verum
end;
end;

theorem Th1: :: SFMASTR1:1
for a being Int-Location
for I being Program of SCM+FSA st not a in UsedIntLoc I holds
not I destroys a
proof
let aa be Int-Location; ::_thesis: for I being Program of SCM+FSA st not aa in UsedIntLoc I holds
not I destroys aa
let I be Program of SCM+FSA; ::_thesis: ( not aa in UsedIntLoc I implies not I destroys aa )
assume A1: not aa in UsedIntLoc I ; ::_thesis: not I destroys aa
let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def_4 ::_thesis: ( not i in rng I or not i destroys aa )
assume  i in rng I ; ::_thesis: not i destroys aa
then  UsedIntLoc i c= UsedIntLoc I by SF_MASTR:19;
then A2: not aa in UsedIntLoc i by A1;
A3: InsCode i <= 12 by SCMFSA_2:16;
percases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A3, NAT_1:36;
suppose InsCode i = 0 ; ::_thesis: not i destroys aa
then  i = halt SCM+FSA by SCMFSA_2:95;
hence  not i destroys aa by SCMFSA7B:5; ::_thesis: verum
end;
suppose InsCode i = 1 ; ::_thesis: not i destroys aa
then consider a, b being Int-Location such that
A4: i = a := b by SCMFSA_2:30;
 UsedIntLoc i = {a,b} by A4, SF_MASTR:14;
then  a in UsedIntLoc i by TARSKI:def_2;
hence  not i destroys aa by A2, A4, SCMFSA7B:6; ::_thesis: verum
end;
suppose InsCode i = 2 ; ::_thesis: not i destroys aa
then consider a, b being Int-Location such that
A5: i = AddTo (a,b) by SCMFSA_2:31;
 UsedIntLoc i = {a,b} by A5, SF_MASTR:14;
then  a in UsedIntLoc i by TARSKI:def_2;
hence  not i destroys aa by A2, A5, SCMFSA7B:7; ::_thesis: verum
end;
suppose InsCode i = 3 ; ::_thesis: not i destroys aa
then consider a, b being Int-Location such that
A6: i = SubFrom (a,b) by SCMFSA_2:32;
 UsedIntLoc i = {a,b} by A6, SF_MASTR:14;
then  a in UsedIntLoc i by TARSKI:def_2;
hence  not i destroys aa by A2, A6, SCMFSA7B:8; ::_thesis: verum
end;
suppose InsCode i = 4 ; ::_thesis: not i destroys aa
then consider a, b being Int-Location such that
A7: i = MultBy (a,b) by SCMFSA_2:33;
 UsedIntLoc i = {a,b} by A7, SF_MASTR:14;
then  a in UsedIntLoc i by TARSKI:def_2;
hence  not i destroys aa by A2, A7, SCMFSA7B:9; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: not i destroys aa
then consider a, b being Int-Location such that
A8: i = Divide (a,b) by SCMFSA_2:34;
A9: UsedIntLoc i = {a,b} by A8, SF_MASTR:14;
then A10: b in UsedIntLoc i by TARSKI:def_2;
 a in UsedIntLoc i by A9, TARSKI:def_2;
hence  not i destroys aa by A2, A8, A10, SCMFSA7B:10; ::_thesis: verum
end;
suppose InsCode i = 6 ; ::_thesis: not i destroys aa
then  ex l being Element of NAT st i = goto l by SCMFSA_2:35;
hence  not i destroys aa by SCMFSA7B:11; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: not i destroys aa
then  ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36;
hence  not i destroys aa by SCMFSA7B:12; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: not i destroys aa
then  ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37;
hence  not i destroys aa by SCMFSA7B:13; ::_thesis: verum
end;
suppose InsCode i = 9 ; ::_thesis: not i destroys aa
then consider a, b being Int-Location, f being FinSeq-Location  such that
A11: i = b := (f,a) by SCMFSA_2:38;
 UsedIntLoc i = {a,b} by A11, SF_MASTR:17;
then  b in UsedIntLoc i by TARSKI:def_2;
hence  not i destroys aa by A2, A11, SCMFSA7B:14; ::_thesis: verum
end;
suppose InsCode i = 10 ; ::_thesis: not i destroys aa
then  ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39;
hence  not i destroys aa by SCMFSA7B:15; ::_thesis: verum
end;
suppose InsCode i = 11 ; ::_thesis: not i destroys aa
then consider a being Int-Location, f being FinSeq-Location  such that
A12: i = a :=len f by SCMFSA_2:40;
 UsedIntLoc i = {a} by A12, SF_MASTR:18;
then  a in UsedIntLoc i by TARSKI:def_1;
hence  not i destroys aa by A2, A12, SCMFSA7B:16; ::_thesis: verum
end;
suppose InsCode i = 12 ; ::_thesis: not i destroys aa
then  ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41;
hence  not i destroys aa by SCMFSA7B:17; ::_thesis: verum
end;
end;
end;

begin

          set D = Data-Locations ;

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

theorem Th2: :: SFMASTR1:2
for P being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ";" J is_closed_on Initialized S,P
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ";" J is_closed_on Initialized S,P
let S be State of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ";" J is_closed_on Initialized S,P
let I, J be Program of SCM+FSA; ::_thesis: ( I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P implies I ";" J is_closed_on Initialized S,P )
assume that
A1: I is_halting_on Initialized S,P and
A2: I is_closed_on Initialized S,P and
A3: J is_closed_on IExec (I,P,S),P ; ::_thesis: I ";" J is_closed_on Initialized S,P
set IS = Initialized S;
set PS = P;
set s = Initialize (Initialized S);
set p = P +* (I ";" J);
A4: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A5: Directed I c= I ";" J by SCMFSA6A:16;
 I ";" J c= P +* (I ";" J) by FUNCT_4:25;
then  Directed I c= P +* (I ";" J) by A5, XBOOLE_1:1;
then A6: (P +* (I ";" J)) +* (Directed I) = P +* (I ";" J) by FUNCT_4:98;
A7: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A8: I is_closed_on Initialize (Initialized S),P +* (I ";" J) by A2, SCMFSA8B:3;
A9: I is_halting_on Initialize (Initialized S),P +* (I ";" J) by A1, A2, A7, SCMFSA8B:5;
then A10: (P +* (I ";" J)) +* I halts_on Initialize (Initialize (Initialized S)) by SCMFSA7B:def_7;
set s1 = Initialize (Initialize (Initialized S));
set p1 = (P +* (I ";" J)) +* I;
set JAt = Start-At (0,SCM+FSA);
set s3 = Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))));
set p3 = ((P +* (I ";" J)) +* I) +* J;
A11: J c= ((P +* (I ";" J)) +* I) +* J by FUNCT_4:25;
set m1 = LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))));
set IJ = I ";" J;
A12: (Initialized S) . (intloc 0) = 1 by SCMFSA_M:9;
then  (Initialize (Initialized S)) . (intloc 0) = 1 by A7, SCMFSA_M:2;
then A13: Initialized (Initialize (Initialize (Initialized S))) = Initialize (Initialized S) by SCMFSA_M:18;
DataPart (IExec (I,P,S)) = DataPart (IExec (I,P,(Initialized S))) by SCMFSA8C:3
.= DataPart (IExec (I,(P +* (I ";" J)),(Initialize (Initialized S)))) by A1, A2, A7, A12, SCMFSA8C:20
.= DataPart (Result (((P +* (I ";" J)) +* I),(Initialized (Initialize (Initialized S))))) by SCMFSA6B:def_1
.= DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) by A13, A10, EXTPRO_1:23 ;
then  DataPart (IExec (I,P,S)) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by MEMSTR_0:79;
then A14: J is_closed_on Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))),((P +* (I ";" J)) +* I) +* J by A3, SCMFSA8B:3;
set PPR = Reloc (J,(card I));
set s4 = Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1));
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A15: DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) = (DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) +* kk by FUNCT_4:71;
let k be Element of NAT ; :: according to SCMFSA7B:def_6 ::_thesis: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J))
 IC (Comput (((P +* (I ";" J)) +* (Directed I)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A8, A9, SCMFSA8A:22;
then A16: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A6;
 DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
then  DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A15, FUNCT_4:98, XBOOLE_1:2;
then A17: DataPart (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A8, A9, A6, SCMFSA8A:22;
A18: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
A19: Reloc (J,(card I)) c= P +* (I ";" J) by A4, A18, XBOOLE_1:1;
percases ( k <= LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))) or (LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1 <= k ) by NAT_1:13;
supposeA20: k <= LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))) ; ::_thesis: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J))
A21: dom I c= dom (I ";" J) by SCMFSA6A:17;
A22: IC (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),k)) in dom I by A8, SCMFSA7B:def_6;
 Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),k) = Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k) by A8, A9, A20, A6, SCMFSA8A:21;
then  IC (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),k)) = IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) ;
hence  IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J)) by A22, A21; ::_thesis: verum
end;
suppose (LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1 <= k ; ::_thesis: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J))
then consider i being Nat such that
A23: k = ((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
reconsider jloc = IC (Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),i)) as Element of NAT ;
A24: Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) = Initialize (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) ;
 (((P +* (I ";" J)) +* I) +* J) +* J = ((P +* (I ";" J)) +* I) +* J ;
then A25: IC (Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),i)) in dom J by A14, A24, SCMFSA7B:def_6;
 dom (Reloc (J,(card I))) =  {  (j + (card I)) where j is Element of NAT : j in dom J  }  by COMPOS_1:33;
then A26: jloc + (card I) in dom (Reloc (J,(card I))) by A25;
A27: dom (Reloc (J,(card I))) c= dom (I ";" J) by A18, RELAT_1:11;
(IC (Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),i))) + (card I) = IC (Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))),i)) by A16, A17, A14, A11, A19, SCMFSA8C:16
.= IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),(((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + i))) by EXTPRO_1:4 ;
hence  IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),k)) in K389((I ";" J)) by A23, A26, A27; ::_thesis: verum
end;
end;
end;

theorem Th3: :: SFMASTR1:3
for P being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ";" J is_halting_on Initialized S,P
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ";" J is_halting_on Initialized S,P
let S be State of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ";" J is_halting_on Initialized S,P
let I, J be Program of SCM+FSA; ::_thesis: ( I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P implies I ";" J is_halting_on Initialized S,P )
assume that
A1: I is_halting_on Initialized S,P and
A2: J is_halting_on IExec (I,P,S),P and
A3: I is_closed_on Initialized S,P and
A4: J is_closed_on IExec (I,P,S),P ; ::_thesis: I ";" J is_halting_on Initialized S,P
set s = Initialize (Initialized S);
set p = P +* (I ";" J);
A5: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
 Directed I c= I ";" J by SCMFSA6A:16;
then  Directed I c= P +* (I ";" J) by A5, XBOOLE_1:1;
then A6: (P +* (I ";" J)) +* (Directed I) = P +* (I ";" J) by FUNCT_4:98;
A7: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A8: I is_halting_on Initialize (Initialized S),P +* (I ";" J) by A1, A3, SCMFSA8B:5;
then A9: (P +* (I ";" J)) +* I halts_on Initialize (Initialize (Initialized S)) by SCMFSA7B:def_7;
set s1 = Initialize (Initialize (Initialized S));
set p1 = (P +* (I ";" J)) +* I;
A10: (Initialized S) . (intloc 0) = 1 by SCMFSA_M:9;
then  (Initialize (Initialized S)) . (intloc 0) = 1 by A7, SCMFSA_M:2;
then A11: Initialize (Initialize (Initialized S)) = Initialized (Initialize (Initialized S)) by SCMFSA_M:18;
set JAt = Start-At (0,SCM+FSA);
set s3 = Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))));
set p3 = ((P +* (I ";" J)) +* I) +* J;
A12: J c= ((P +* (I ";" J)) +* I) +* J by FUNCT_4:25;
set m3 = LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))));
A13: DataPart (IExec (I,P,S)) = DataPart (IExec (I,P,(Initialized S))) by SCMFSA8C:3
.= DataPart (IExec (I,(P +* (I ";" J)),(Initialize (Initialized S)))) by A1, A3, A7, A10, SCMFSA8C:20
.= DataPart (Result (((P +* (I ";" J)) +* I),(Initialized (Initialize (Initialized S))))) by SCMFSA6B:def_1
.= DataPart (Result (((P +* (I ";" J)) +* I),(Initialized (Initialize (Initialized S)))))
.= DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) by A11, A9, EXTPRO_1:23 ;
then  J is_halting_on Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))),(P +* (I ";" J)) +* I by A2, A4, SCMFSA8B:5;
then A14: ((P +* (I ";" J)) +* I) +* J halts_on Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) by SCMFSA7B:def_7;
 DataPart (IExec (I,P,S)) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A13, MEMSTR_0:79;
then A15: J is_closed_on Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))),((P +* (I ";" J)) +* I) +* J by A4, SCMFSA8B:3;
A16: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
set m1 = LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))));
set s4 = Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1));
set p4 = P +* (I ";" J);
A17: Reloc (J,(card I)) c= P +* (I ";" J) by A5, A16, XBOOLE_1:1;
reconsider m = ((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))) as Element of NAT ;
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A18: DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) = (DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) +* kk by FUNCT_4:71;
take  m ; :: according to EXTPRO_1:def_8,SCMFSA7B:def_7 ::_thesis: ( IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m)) in dom (P +* (I ";" J)) & CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = halt SCM+FSA )
 IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m)) in NAT ;
hence  IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m)) in dom (P +* (I ";" J)) by PARTFUN1:def_2; ::_thesis: CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = halt SCM+FSA
A19: I is_closed_on Initialize (Initialized S),P +* (I ";" J) by A3, A7, SCMFSA8B:3;
then A20: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A8, A6, SCMFSA8A:22;
A21: Comput ((P +* (I ";" J)),(Initialize (Initialized S)),(((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))) = Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))))))) by EXTPRO_1:4;
 DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
then  DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A18, FUNCT_4:98, XBOOLE_1:2;
then  DataPart (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A19, A8, A6, SCMFSA8A:22;
then  IncAddr ((CurInstr ((((P +* (I ";" J)) +* I) +* J),(Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))))),(card I)) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))))))))) by A20, A15, A17, A12, SCMFSA8C:16;
then  IncAddr ((CurInstr ((((P +* (I ";" J)) +* I) +* J),(Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))))),(card I)) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),(((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))))) by A21;
then  CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = IncAddr ((halt SCM+FSA),(card I)) by A14, EXTPRO_1:def_15
.= halt SCM+FSA by COMPOS_0:4 ;
hence  CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = halt SCM+FSA ; ::_thesis: verum
end;

theorem Th4: :: SFMASTR1:4
for p being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being 0 -started State of SCM+FSA st I is_closed_on s,p & I c= p & p halts_on s holds
for m being Element of NAT st m <= LifeSpan (p,s) holds
Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA
for s being 0 -started State of SCM+FSA st I is_closed_on s,p & I c= p & p halts_on s holds
for m being Element of NAT st m <= LifeSpan (p,s) holds
Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)
let I, J be Program of SCM+FSA; ::_thesis: for s being 0 -started State of SCM+FSA st I is_closed_on s,p & I c= p & p halts_on s holds
for m being Element of NAT st m <= LifeSpan (p,s) holds
Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)
let s be 0 -started State of SCM+FSA; ::_thesis: ( I is_closed_on s,p & I c= p & p halts_on s implies for m being Element of NAT st m <= LifeSpan (p,s) holds
Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m) )
assume that
A1: I is_closed_on s,p and
A2: I c= p and
A3: p halts_on s ; ::_thesis: for m being Element of NAT st m <= LifeSpan (p,s) holds
Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)
A4: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
A5: p +* I = p by A2, FUNCT_4:98;
defpred S1[ Element of NAT ] means ( $1 <= LifeSpan (p,s) implies Comput (p,s,$1) = Comput ((p +* (I ";" J)),s,$1) );
A6: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
then A7: dom I c= dom (I ";" J) by XBOOLE_1:7;
set sIJ = s;
set pIJ = p +* (I ";" J);
A8: I ";" J c= p +* (I ";" J) by FUNCT_4:25;
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A9: ( m <= LifeSpan (p,s) implies Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m) ) ; ::_thesis: S1[m + 1]
A10: Comput ((p +* (I ";" J)),s,(m + 1)) = Following ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),s,m))) by EXTPRO_1:3;
A11: Comput (p,s,(m + 1)) = Following (p,(Comput (p,s,m))) by EXTPRO_1:3;
A12: p /. (IC (Comput (p,s,m))) = p . (IC (Comput (p,s,m))) by PBOOLE:143;
assume A13: m + 1 <= LifeSpan (p,s) ; ::_thesis: Comput (p,s,(m + 1)) = Comput ((p +* (I ";" J)),s,(m + 1))
then A14: IC (Comput (p,s,m)) = IC (Comput ((p +* (I ";" J)),s,m)) by A9, NAT_1:13;
 s = Initialize s by A4, FUNCT_4:98;
then A15: IC (Comput (p,s,m)) in dom I by A1, A5, SCMFSA7B:def_6;
A16: CurInstr (p,(Comput (p,s,m))) = I . (IC (Comput (p,s,m))) by A15, A12, A2, GRFUNC_1:2;
A17: (p +* (I ";" J)) /. (IC (Comput ((p +* (I ";" J)),s,m))) = (p +* (I ";" J)) . (IC (Comput ((p +* (I ";" J)),s,m))) by PBOOLE:143;
 m < LifeSpan (p,s) by A13, NAT_1:13;
then  I . (IC (Comput (p,s,m))) <> halt SCM+FSA by A3, A16, EXTPRO_1:def_15;
then  CurInstr (p,(Comput (p,s,m))) = (I ";" J) . (IC (Comput (p,s,m))) by A15, A16, SCMFSA6A:15
.= CurInstr ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),s,m))) by A14, A15, A7, A17, A8, GRFUNC_1:2 ;
hence  Comput (p,s,(m + 1)) = Comput ((p +* (I ";" J)),s,(m + 1)) by A9, A13, A11, A10, NAT_1:13; ::_thesis: verum
end;
A18: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A6); ::_thesis: verum
end;

Lm1:  for p being Instruction-Sequence of SCM+FSA
for I being good Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_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 p be Instruction-Sequence of SCM+FSA; ::_thesis: for I being good Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_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 ) )
let I be good Program of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_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 ) )
let J be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_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 ) )
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p implies ( 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 ) ) )
assume 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 and
A4: I is_closed_on s,p and
A5: J is_closed_on IExec (I,p,s),p ; ::_thesis: ( not Initialize ((intloc 0) .--> 1) c= s or not I ";" J c= p or ( 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 ) ) )
set s1 = s;
set p1 = p +* I;
set m1 = LifeSpan ((p +* I),s);
set s4 = Comput (p,s,((LifeSpan ((p +* I),s)) + 1));
set p4 = p;
assume A6: Initialize ((intloc 0) .--> 1) c= s ; ::_thesis: ( not I ";" J c= p or ( 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 ) ) )
then  Start-At (0,SCM+FSA) c= s by MEMSTR_0:50;
then A7: Start-At (0,SCM+FSA) c= s ;
A8: s = s +* (Start-At (0,SCM+FSA)) by A7, FUNCT_4:98
.= Initialize s ;
then A9: p +* I halts_on s by A2, SCMFSA7B:def_7;
assume A10: I ";" J c= p ; ::_thesis: ( 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 ) )
 Directed I c= I ";" J by SCMFSA6A:16;
then  Directed I c= p by A10, XBOOLE_1:1;
then A11: p +* (Directed I) = p by FUNCT_4:98;
 Start-At (0,SCM+FSA) c= s by A6, MEMSTR_0:50;
then  Start-At (0,SCM+FSA) c= s ;
then  s = Initialize s by FUNCT_4:98;
hence A12: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by A2, A4, A11, SCMFSA8A:22; ::_thesis: ( 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 ) )
set JAt = Start-At (0,SCM+FSA);
set InJ = Initialize ((intloc 0) .--> 1);
set s3 = Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))));
set p3 = (p +* I) +* J;
A13: J c= (p +* I) +* J by FUNCT_4:25;
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A14: DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
 (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) . (intloc 0) = s . (intloc 0) by A4, A8, SCMFSA8C:68;
then A15: Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = Initialize (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A1, SCMFSA_M:18;
then  DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) +* kk by FUNCT_4:71;
then  DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A14, FUNCT_4:98, XBOOLE_1:2;
hence A16: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A2, A4, A8, A11, SCMFSA8A:22; ::_thesis: ( 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 ) )
A17: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
A18: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:10;
A19: s = s +* (Initialize ((intloc 0) .--> 1)) by A6, FUNCT_4:98;
A20: DataPart (IExec (I,p,s)) = DataPart (Result ((p +* I),(Initialized s))) by SCMFSA6B:def_1
.= DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A9, A19, EXTPRO_1:23 ;
then  J is_halting_on Comput ((p +* I),s,(LifeSpan ((p +* I),s))),p +* I by A3, A5, SCMFSA8B:5;
then A21: (p +* I) +* J halts_on Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A15, SCMFSA7B:def_7;
 I ";" J c= p by A10;
then  Reloc (J,(card I)) c= p by A17, XBOOLE_1:1;
then  Reloc (J,(card I)) c= p ;
hence  Reloc (J,(card I)) c= p ; ::_thesis: ( (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 ) )
A22: Reloc (J,(card I)) c= p by A10, A17, XBOOLE_1:1;
 intloc 0 in Int-Locations by AMI_2:def_16;
then A23: intloc 0 in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
hence (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = (DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))) . (intloc 0) by A16, FUNCT_1:49
.= (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . (intloc 0) by A23, FUNCT_1:49
.= 1 by A18, FUNCT_4:13, SCMFSA_M:12 ;
::_thesis: ( 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 ) )
set m3 = LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))));
reconsider m = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))) as Element of NAT ;
A24: DataPart (IExec (I,p,s)) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A15, A20, MEMSTR_0:79;
then A25: J is_closed_on Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))),(p +* I) +* J by A5, SCMFSA8B:3;
A26: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))))) by EXTPRO_1:4;
 IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))))),(card I)) = CurInstr (p,(Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))))))) by A25, A12, A16, A22, A13, SCMFSA8C:16;
then  IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))))) by A26;
then A27: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A21, EXTPRO_1:def_15
.= halt SCM+FSA by COMPOS_0:4 ;
hence A28: p halts_on s by EXTPRO_1:29; ::_thesis: ( 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 ) )
A29: now__::_thesis:_for_k_being_Element_of_NAT_st_((LifeSpan_((p_+*_I),s))_+_1)_+_k_<_m_holds_
not_CurInstr_(p,(Comput_(p,s,(((LifeSpan_((p_+*_I),s))_+_1)_+_k))))_=_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( ((LifeSpan ((p +* I),s)) + 1) + k < m implies not CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)))) = halt SCM+FSA )
assume  ((LifeSpan ((p +* I),s)) + 1) + k < m ; ::_thesis: not CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)))) = halt SCM+FSA
then A30: k < LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))) by XREAL_1:6;
A31: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),k) by EXTPRO_1:4;
assume A32: CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)))) = halt SCM+FSA ; ::_thesis: contradiction
A33: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
 IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k)))),(card I)) = halt SCM+FSA by A32, A31, A25, A12, A16, A22, A13, SCMFSA8C:16;
then  InsCode (CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k)))) = 0 by COMPOS_0:def_9, A33;
then  CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k))) = halt SCM+FSA by SCMFSA_2:95;
hence  contradiction by A21, A30, EXTPRO_1:def_15; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_m_holds_
CurInstr_(p,(Comput_(p,s,k)))_<>_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( k < m implies CurInstr (p,(Comput (p,s,b1))) <> halt SCM+FSA )
assume A34: k < m ; ::_thesis: CurInstr (p,(Comput (p,s,b1))) <> halt SCM+FSA
percases ( k <= LifeSpan ((p +* I),s) or LifeSpan ((p +* I),s) < k ) ;
suppose k <= LifeSpan ((p +* I),s) ; ::_thesis: CurInstr (p,(Comput (p,s,b1))) <> halt SCM+FSA
hence  CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A2, A4, A8, A11, SCMFSA8A:21; ::_thesis: verum
end;
suppose LifeSpan ((p +* I),s) < k ; ::_thesis: CurInstr (p,(Comput (p,s,b1))) <> halt SCM+FSA
then  (LifeSpan ((p +* I),s)) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A35: ((LifeSpan ((p +* I),s)) + 1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def_12;
 ((LifeSpan ((p +* I),s)) + 1) + kk = k by A35;
hence  CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A29, A34; ::_thesis: verum
end;
end;
end;
then  for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA holds
m <= k ;
then A36: LifeSpan (p,s) = m by A27, A28, EXTPRO_1:def_15;
 Comput ((p +* I),s,(LifeSpan ((p +* I),s))) = Result ((p +* I),s) by A9, EXTPRO_1:23;
hence  LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) by A36; ::_thesis: ( J is good implies (Result (p,s)) . (intloc 0) = 1 )
 Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:25, MEMSTR_0:50;
then A37: Initialize (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) = Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:98;
A38: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:25;
hereby  ::_thesis: verum
A39: DataPart (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) = DataPart (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) by A25, A12, A16, A22, A13, SCMFSA8C:16;
assume A40: J is good ; ::_thesis: (Result (p,s)) . (intloc 0) = 1
thus (Result (p,s)) . (intloc 0) = (Comput (p,s,m)) . (intloc 0) by A28, A36, EXTPRO_1:23
.= (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) . (intloc 0) by EXTPRO_1:4
.= (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) . (intloc 0) by A39, SCMFSA_M:2
.= (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . (intloc 0) by A5, A24, A37, A40, SCMFSA8B:3, SCMFSA8C:68
.= 1 by A18, A38, GRFUNC_1:2, SCMFSA_M:12 ; ::_thesis: verum
end;
end;

theorem Th5: :: SFMASTR1:5
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
let J be Program of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
let Ig be good Program of SCM+FSA; ::_thesis: ( Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_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)))))) )
set I = Ig;
assume that
A1: Ig is_halting_on Initialized s,p and
A2: J is_halting_on IExec (Ig,p,s),p and
A3: Ig is_closed_on Initialized s,p and
A4: J is_closed_on IExec (Ig,p,s),p ; ::_thesis: LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
set Is = Initialized s;
A5: (Initialized s) . (intloc 0) = 1 by SCMFSA_M:9;
set s1 = Initialized s;
set p1 = p +* Ig;
set m1 = LifeSpan ((p +* Ig),(Initialized s));
set s3 = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))));
set p3 = (p +* Ig) +* J;
A6: ((p +* Ig) +* J) +* J = (p +* Ig) +* J ;
 Initialized s = Initialized (Initialized s) ;
then A7: Initialized s = Initialize (Initialized s) by A5, SCMFSA_M:18;
then A8: p +* Ig halts_on Initialized s by A1, SCMFSA7B:def_7;
then A9: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by EXTPRO_1:23;
set s2 = Initialized s;
set p2 = p +* (Ig ";" J);
A10: Ig ";" J c= p +* (Ig ";" J) by FUNCT_4:25;
A11: DataPart (Initialized s) = DataPart (Initialized s) ;
A12: (Initialized s) . (intloc 0) = 1 by A5;
set JAt = Start-At (0,SCM+FSA);
 (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) . (intloc 0) = 1 by A3, A5, A7, SCMFSA8C:68;
then A13: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by SCMFSA_M:18;
then  Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by FUNCT_4:25;
then A14: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) by FUNCT_4:98;
DataPart (IExec (Ig,p,s)) = DataPart (Result ((p +* Ig),(Initialized s))) by SCMFSA6B:def_1
.= DataPart (Result ((p +* Ig),(Initialized s)))
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A8, EXTPRO_1:23 ;
then A15: DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) by A13, MEMSTR_0:79;
then A16: J is_halting_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J by A2, A4, SCMFSA8B:5;
 Initialize (Initialized s) = Initialized s by MEMSTR_0:44;
then  Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = Result ((p +* Ig),(Initialized s)) by A1, A3, A11, SCMFSA8C:72;
then  Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A9;
then A17: DataPart (Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) ;
A18: DataPart (IExec (Ig,p,s)) = DataPart (IExec (Ig,p,(Initialized s))) by SCMFSA8C:3
.= DataPart (IExec (Ig,(p +* (Ig ";" J)),(Initialized s))) by A1, A3, A5, A11, SCMFSA8C:20 ;
then A19: J is_closed_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J) by A2, A4, SCMFSA8B:5;
A20: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
A21: Ig is_closed_on Initialized s,p +* (Ig ";" J) by A3, A11, SCMFSA8B:3;
A22: J is_halting_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J) by A2, A4, A18, SCMFSA8B:5;
 Ig is_halting_on Initialized s,p +* (Ig ";" J) by A1, A3, A11, SCMFSA8B:5;
then A23: LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s))) + 1) + (LifeSpan ((((p +* (Ig ";" J)) +* Ig) +* J),(Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))))) by A21, A12, A19, A22, A20, Lm1, A10;
 Start-At (0,SCM+FSA) c= Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) by FUNCT_4:25, MEMSTR_0:50;
then A24: Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) = Initialize (Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))) by FUNCT_4:98;
A25: J is_closed_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J by A4, A15, SCMFSA8B:3;
A26: LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s)) by A1, A3, A7, A11, SCMFSA8C:72;
 LifeSpan ((((p +* (Ig ";" J)) +* Ig) +* J),(Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))))) = LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))) by A25, A16, A14, A24, A17, A6, SCMFSA8C:72;
hence  LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) by A9, A23, A26; ::_thesis: verum
end;

theorem Th6: :: SFMASTR1:6
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
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 p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
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))
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
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))
let J be Program of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
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))
let Ig be good Program of SCM+FSA; ::_thesis: ( Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_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)) )
set I = Ig;
assume that
A1: Ig is_halting_on Initialized s,p and
A2: J is_halting_on IExec (Ig,p,s),p and
A3: Ig is_closed_on Initialized s,p and
A4: J is_closed_on IExec (Ig,p,s),p ; ::_thesis: 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))
set Is = Initialized s;
set Ip = p;
A5: (Initialized s) . (intloc 0) = 1 by SCMFSA_M:9;
set s1 = Initialized s;
set p1 = p +* Ig;
A6: Ig c= p +* Ig by FUNCT_4:25;
set m1 = LifeSpan ((p +* Ig),(Initialized s));
 Initialized s = Initialized (Initialized s) ;
then A7: Initialized s = Initialize (Initialized s) by A5, SCMFSA_M:18;
 DataPart (Initialized s) = DataPart (Initialized s) ;
then A8: Ig is_closed_on Initialized s,p +* Ig by A3, SCMFSA8B:3;
set s3 = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))));
set p3 = (p +* Ig) +* J;
A9: J c= (p +* Ig) +* J by FUNCT_4:25;
A10: p +* Ig halts_on Initialized s by A1, A7, SCMFSA7B:def_7;
then A11: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by EXTPRO_1:23;
set s2 = Initialized s;
set p2 = p +* (Ig ";" J);
A12: Ig ";" J c= p +* (Ig ";" J) by FUNCT_4:25;
 Initialized s = Initialized (Initialized s) ;
then A13: Initialized s = Initialize (Initialized s) by A5, SCMFSA_M:18;
A14: DataPart (Initialized s) = DataPart (Initialized s) ;
A15: (Initialized s) . (intloc 0) = 1 by A5;
A16: DataPart (IExec (Ig,p,s)) = DataPart (IExec (Ig,p,(Initialized s))) by SCMFSA8C:3
.= DataPart (IExec (Ig,(p +* (Ig ";" J)),(Initialized s))) by A1, A3, A5, A14, SCMFSA8C:20 ;
then A17: J is_closed_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J) by A2, A4, SCMFSA8B:5;
 Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then A18: LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s)) by A1, A3, A14, SCMFSA8C:72;
set JAt = Start-At (0,SCM+FSA);
 (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) . (intloc 0) = 1 by A3, A5, A7, SCMFSA8C:68;
then A19: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by SCMFSA_M:18;
set m3 = LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))));
 Ig ";" J is_halting_on Initialized s,p by A1, A2, A3, A4, Th3;
then A20: p +* (Ig ";" J) halts_on Initialized s by A13, SCMFSA7B:def_7;
A21: IExec ((Ig ";" J),p,s) = Result ((p +* (Ig ";" J)),(Initialized s)) by SCMFSA6B:def_1
.= Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* (Ig ";" J)),(Initialized s)))) by A20, EXTPRO_1:23
.= Comput ((p +* (Ig ";" J)),(Initialized s),(((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) by A1, A2, A3, A4, A11, Th5 ;
A22: DataPart (IExec (Ig,p,s)) = DataPart (Result ((p +* Ig),(Initialized s))) by SCMFSA6B:def_1
.= DataPart (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A10, EXTPRO_1:23 ;
then  J is_halting_on Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))),p +* Ig by A2, A4, SCMFSA8B:5;
then A23: (p +* Ig) +* J halts_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A19, SCMFSA7B:def_7;
set IEJIs = IExec (J,p,(IExec (Ig,p,s)));
set IAt = Start-At (0,SCM+FSA);
 DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) by A19, A22, MEMSTR_0:79;
then A24: J is_closed_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J by A4, SCMFSA8B:3;
A25: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
 (IExec (Ig,p,s)) . (intloc 0) = 1 by A1, A3, SCMFSA8C:67;
then A26: Initialized (IExec (Ig,p,s)) = Initialize (IExec (Ig,p,s)) by SCMFSA_M:18;
then  Result (((p +* Ig) +* J),((Result ((p +* Ig),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))) = Result ((p +* J),((IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1)))) by A2, A4, A19, A22, A11, SCMFSA8C:72;
then A27: IC (Result (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) = IC (Result ((p +* J),(Initialized (IExec (Ig,p,s))))) ;
A28: Result ((p +* J),(Initialized (IExec (Ig,p,s)))) = Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))) by A2, A4, A19, A22, A26, SCMFSA8C:72;
A29: IExec (J,p,(IExec (Ig,p,s))) = Result ((p +* J),(Initialized (IExec (Ig,p,s)))) by SCMFSA6B:def_1
.= Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))) by A23, A28, EXTPRO_1:23 ;
A30: Ig is_halting_on Initialized s,p +* (Ig ";" J) by A1, A3, A14, SCMFSA8B:5;
reconsider l = (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) as Element of NAT ;
reconsider s2t = s +* ((intloc 0) .--> 1) as State of SCM+FSA ;
 DataPart (Initialized s) = DataPart (Initialized s) ;
then A31: Ig is_closed_on Initialized s,(p +* (Ig ";" J)) +* Ig by A3, SCMFSA8B:3;
A32: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
A33: Ig +* (Ig ";" J) = Ig ";" J by SCMFSA6A:18;
A34: ((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J) = (p +* (Ig ";" J)) +* (Ig +* (Ig ";" J)) by FUNCT_4:14;
A35: Ig c= (p +* (Ig ";" J)) +* Ig by FUNCT_4:25;
A36: (p +* Ig) +* (Ig ";" J) = p +* (Ig ";" J) by A33, FUNCT_4:14;
A37: Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) = Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) by A10, A8, Th4, A6, A36;
 Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then  (p +* (Ig ";" J)) +* Ig halts_on Initialized s by A30, SCMFSA7B:def_7;
then  Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) = Comput ((((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) by A31, A18, Th4, A35;
then  DataPart (Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = DataPart (Comput ((((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput ((((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput (((p +* (Ig ";" J)) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A33, A34
.= DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A37 ;
then A38: DataPart ((Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71
.= DataPart ((Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71 ;
A39: Ig is_closed_on Initialized s,p +* (Ig ";" J) by A3, A14, SCMFSA8B:3;
A40: J is_halting_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J) by A2, A4, A16, SCMFSA8B:5;
then A41: DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))) = DataPart (Initialized (Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) by A25, A39, A30, A18, A15, A17, Lm1, A12;
 Reloc (J,(card Ig)) c= Ig ";" J by FUNCT_4:25;
then A42: Reloc (J,(card Ig)) c= p +* (Ig ";" J) by A12, XBOOLE_1:1;
A43: IC (Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))) = card Ig by A25, A39, A30, A18, A15, A17, A40, Lm1, A12;
then A44: DataPart (Comput ((p +* (Ig ";" J)),(Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) = DataPart (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) by A24, A38, A41, A9, A42, SCMFSA8C:16;
A45: DataPart (IExec ((Ig ";" J),p,s)) = DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),(((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) by A21
.= DataPart (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) by A44, EXTPRO_1:4
.= DataPart (IExec (J,p,(IExec (Ig,p,s)))) by A29 ;
A46: IC (Comput ((p +* (Ig ";" J)),(Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) = (IC (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) + (card Ig) by A24, A38, A43, A41, A9, A42, SCMFSA8C:16;
A47: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by A10, EXTPRO_1:23;
A48: IC (IExec ((Ig ";" J),p,s)) = IC (Result ((p +* (Ig ";" J)),(Initialized s))) by SCMFSA6B:def_1
.= IC (Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* (Ig ";" J)),(Initialized s))))) by A20, EXTPRO_1:23
.= IC (Comput ((p +* (Ig ";" J)),(Initialized s),(((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) by A1, A2, A3, A4, A11, Th5
.= (IC (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) + (card Ig) by A46, EXTPRO_1:4
.= (IC (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))) + (card Ig) by A23, EXTPRO_1:23
.= (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) by A27, A47, SCMFSA6B:def_1 ;
A49: now__::_thesis:_for_x_being_set_st_x_in_dom_(IExec_((Ig_";"_J),p,s))_holds_
(IExec_((Ig_";"_J),p,s))_._x_=_((IExec_(J,p,(IExec_(Ig,p,s))))_+*_(Start-At_(((IC_(IExec_(J,p,(IExec_(Ig,p,s)))))_+_(card_Ig)),SCM+FSA)))_._x
let x be set ; ::_thesis: ( x in dom (IExec ((Ig ";" J),p,s)) implies (IExec ((Ig ";" J),p,s)) . b1 = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . b1 )
assume A50: x in dom (IExec ((Ig ";" J),p,s)) ; ::_thesis: (IExec ((Ig ";" J),p,s)) . b1 = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . b1
percases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A50, SCMFSA_M:1;
supposeA51: x is Int-Location ; ::_thesis: (IExec ((Ig ";" J),p,s)) . b1 = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . b1
then  x <> IC by SCMFSA_2:56;
then A52: not x in dom (Start-At (l,SCM+FSA)) by A32, TARSKI:def_1;
 (IExec ((Ig ";" J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A45, A51, SCMFSA_M:2;
hence  (IExec ((Ig ";" J),p,s)) . x = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A52, FUNCT_4:11; ::_thesis: verum
end;
supposeA53: x is FinSeq-Location ; ::_thesis: (IExec ((Ig ";" J),p,s)) . b1 = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . b1
then  x <> IC by SCMFSA_2:57;
then A54: not x in dom (Start-At (l,SCM+FSA)) by A32, TARSKI:def_1;
 (IExec ((Ig ";" J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A45, A53, SCMFSA_M:2;
hence  (IExec ((Ig ";" J),p,s)) . x = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A54, FUNCT_4:11; ::_thesis: verum
end;
supposeA55: x = IC ; ::_thesis: (IExec ((Ig ";" J),p,s)) . b1 = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . b1
then  x in {(IC )} by TARSKI:def_1;
then A56: x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:13;
thus (IExec ((Ig ";" J),p,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A48, A55, FUNCOP_1:72
.= ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A55, A56, FUNCT_4:13 ; ::_thesis: verum
end;
end;
end;
dom (IExec ((Ig ";" J),p,s)) = the carrier of SCM+FSA by PARTFUN1:def_2
.= dom ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) by PARTFUN1:def_2 ;
hence  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)) by A49, FUNCT_1:2; ::_thesis: verum
end;

theorem Th7: :: SFMASTR1:7
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
let J be Program of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
let Ig be good Program of SCM+FSA; ::_thesis: for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
let a be Int-Location; ::_thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) implies (IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a )
set I = Ig;
assume that
A1: ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) and
A2: ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) ; ::_thesis: (IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
A3: J is_halting_on IExec (Ig,p,s),p by A2, SCMFSA7B:19;
A4: Ig is_closed_on Initialized s,p by A1, SCMFSA7B:18;
A5: not a in dom (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA)) by SCMFSA_2:102;
A6: J is_closed_on IExec (Ig,p,s),p by A2, SCMFSA7B:18;
 Ig is_halting_on Initialized s,p by A1, SCMFSA7B:19;
then  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)) by A3, A4, A6, Th6;
hence  (IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a by A5, FUNCT_4:11; ::_thesis: verum
end;

theorem Th8: :: SFMASTR1:8
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
let J be Program of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
let Ig be good Program of SCM+FSA; ::_thesis: for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
let f be FinSeq-Location ; ::_thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) implies (IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f )
set I = Ig;
assume that
A1: ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) and
A2: ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) ; ::_thesis: (IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
A3: J is_halting_on IExec (Ig,p,s),p by A2, SCMFSA7B:19;
A4: Ig is_closed_on Initialized s,p by A1, SCMFSA7B:18;
A5: not f in dom (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA)) by SCMFSA_2:103;
A6: J is_closed_on IExec (Ig,p,s),p by A2, SCMFSA7B:18;
 Ig is_halting_on Initialized s,p by A1, SCMFSA7B:19;
then  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)) by A3, A4, A6, Th6;
hence  (IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f by A5, FUNCT_4:11; ::_thesis: verum
end;

theorem :: SFMASTR1:9
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))
let J be Program of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))
let Ig be good Program of SCM+FSA; ::_thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) implies DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s)))) )
set I = Ig;
assume that
A1: ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) and
A2: ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) ; ::_thesis: DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))
A3: for f being FinSeq-Location holds (IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f by A1, A2, Th8;
 for a being Int-Location holds (IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a by A1, A2, Th7;
hence  DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s)))) by A3, SCMFSA_M:2; ::_thesis: verum
end;

theorem Th10: :: SFMASTR1:10
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
let s be State of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
let Ig be good Program of SCM+FSA; ::_thesis: ( ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) implies DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) )
set I = Ig;
set IE = IExec (Ig,p,s);
assume A1: ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) ; ::_thesis: DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
A2: Ig is_halting_on Initialized s,p by A1, SCMFSA7B:19;
A3: Ig is_closed_on Initialized s,p by A1, SCMFSA7B:18;
now__::_thesis:_(_dom_(DataPart_(Initialized_(IExec_(Ig,p,s))))_=_(dom_(IExec_(Ig,p,s)))_/\_(Data-Locations_)_&_(_for_x_being_set_st_x_in_dom_(DataPart_(Initialized_(IExec_(Ig,p,s))))_holds_
(DataPart_(Initialized_(IExec_(Ig,p,s))))_._x_=_(IExec_(Ig,p,s))_._x_)_)
A4: dom (Initialized (IExec (Ig,p,s))) = the carrier of SCM+FSA by PARTFUN1:def_2;
A5: dom (Initialized (IExec (Ig,p,s))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13
.= (Data-Locations ) \/ {(IC )} ;
A6: dom (IExec (Ig,p,s)) = the carrier of SCM+FSA by PARTFUN1:def_2;
hence  dom (DataPart (Initialized (IExec (Ig,p,s)))) = (dom (IExec (Ig,p,s))) /\ (Data-Locations ) by A4, RELAT_1:61; ::_thesis: for x being set st x in dom (DataPart (Initialized (IExec (Ig,p,s)))) holds
(DataPart (Initialized (IExec (Ig,p,s)))) . b2 = (IExec (Ig,p,s)) . b2
then A7: dom (DataPart (Initialized (IExec (Ig,p,s)))) = Data-Locations by A4, A6, A5, XBOOLE_1:21;
let x be set ; ::_thesis: ( x in dom (DataPart (Initialized (IExec (Ig,p,s)))) implies (DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1 )
assume A8: x in dom (DataPart (Initialized (IExec (Ig,p,s)))) ; ::_thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1
percases ( x in Int-Locations or x in FinSeq-Locations ) by A8, A7, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1
then reconsider x9 = x as Int-Location by AMI_2:def_16;
hereby  ::_thesis: verum
percases ( x9 is read-write or x9 is read-only ) ;
supposeA9: x9 is read-write ; ::_thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . x = (IExec (Ig,p,s)) . x
thus (DataPart (Initialized (IExec (Ig,p,s)))) . x = (Initialized (IExec (Ig,p,s))) . x by A8, A7, FUNCT_1:49
.= (IExec (Ig,p,s)) . x by A9, SCMFSA_M:37 ; ::_thesis: verum
end;
suppose x9 is read-only ; ::_thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . x = (IExec (Ig,p,s)) . x
then A10: x9 = intloc 0 by SCMFSA_M:def_2;
thus (DataPart (Initialized (IExec (Ig,p,s)))) . x = (Initialized (IExec (Ig,p,s))) . x9 by A8, A7, FUNCT_1:49
.= 1 by A10, SCMFSA_M:9
.= (IExec (Ig,p,s)) . x by A3, A2, A10, SCMFSA8C:67 ; ::_thesis: verum
end;
end;
end;
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5;
thus (DataPart (Initialized (IExec (Ig,p,s)))) . x = (Initialized (IExec (Ig,p,s))) . x9 by A8, A7, FUNCT_1:49
.= (IExec (Ig,p,s)) . x by SCMFSA_M:37 ; ::_thesis: verum
end;
end;
end;
hence  DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) by FUNCT_1:46; ::_thesis: verum
end;

theorem Th11: :: SFMASTR1:11
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a
let s be State of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a
let Ig be good Program of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a
let j be parahalting Instruction of SCM+FSA; ::_thesis: for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a
let a be Int-Location; ::_thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) implies (IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a )
set I = Ig;
set Mj = Macro j;
 a in Int-Locations by AMI_2:def_16;
then A1: a in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
assume A2: ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) ; ::_thesis: (IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a
A3: DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) by A2, Th10;
thus (IExec ((Ig ";" j),p,s)) . a = (IExec ((Macro j),p,(IExec (Ig,p,s)))) . a by A2, Th7
.= (IExec ((Macro j),p,(IExec (Ig,p,s)))) . a
.= (Exec (j,(Initialized (IExec (Ig,p,s))))) . a by SCMFSA6C:5
.= (Exec (j,(Initialized (IExec (Ig,p,s))))) . a
.= (DataPart (Exec (j,(Initialized (IExec (Ig,p,s)))))) . a by A1, FUNCT_1:49
.= (DataPart (Exec (j,(IExec (Ig,p,s))))) . a by A3, SCMFSA6C:4
.= (Exec (j,(IExec (Ig,p,s)))) . a by A1, FUNCT_1:49 ; ::_thesis: verum
end;

theorem Th12: :: SFMASTR1:12
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let s be State of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let Ig be good Program of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let j be parahalting Instruction of SCM+FSA; ::_thesis: for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
let f be FinSeq-Location ; ::_thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) implies (IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f )
set I = Ig;
set Mj = Macro j;
 f in FinSeq-Locations by SCMFSA_2:def_5;
then A1: f in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
assume A2: ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) ; ::_thesis: (IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f
A3: DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) by A2, Th10;
thus (IExec ((Ig ";" j),p,s)) . f = (IExec ((Macro j),p,(IExec (Ig,p,s)))) . f by A2, Th8
.= (IExec ((Macro j),p,(IExec (Ig,p,s)))) . f
.= (Exec (j,(Initialized (IExec (Ig,p,s))))) . f by SCMFSA6C:5
.= (Exec (j,(Initialized (IExec (Ig,p,s))))) . f
.= (DataPart (Exec (j,(Initialized (IExec (Ig,p,s)))))) . f by A1, FUNCT_1:49
.= (DataPart (Exec (j,(IExec (Ig,p,s))))) . f by A3, SCMFSA6C:4
.= (Exec (j,(IExec (Ig,p,s)))) . f by A1, FUNCT_1:49 ; ::_thesis: verum
end;

theorem :: SFMASTR1:13
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))
let s be State of SCM+FSA; ::_thesis: for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))
let Ig be good Program of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))
let j be parahalting Instruction of SCM+FSA; ::_thesis: ( ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) implies DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s)))) )
set I = Ig;
assume A1: ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) ; ::_thesis: DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))
then A2: for f being FinSeq-Location holds (IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f by Th12;
 for a being Int-Location holds (IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a by A1, Th11;
hence  DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s)))) by A2, SCMFSA_M:2; ::_thesis: verum
end;

theorem Th14: :: SFMASTR1:14
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA
for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA
for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA
for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
let J be Program of SCM+FSA; ::_thesis: for i being parahalting good Instruction of SCM+FSA
for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
let i be parahalting good Instruction of SCM+FSA; ::_thesis: for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
let a be Int-Location; ::_thesis: ( ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) implies (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a )
set Mi = Macro i;
A1: IExec ((Macro i),p,s) = Exec (i,(Initialized s)) by SCMFSA6C:5;
assume  ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) ; ::_thesis: (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
then A2: ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) by SCMFSA7B:18, SCMFSA7B:19;
A3: J is_closed_on IExec ((Macro i),p,s),p by A2, A1;
 J is_halting_on IExec ((Macro i),p,s),p by A2, A1;
hence (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(IExec ((Macro i),p,s)))) . a by A3, Th7
.= (IExec (J,p,(IExec ((Macro i),p,s)))) . a
.= (IExec (J,p,(Exec (i,(Initialized s))))) . a by A1
.= (IExec (J,p,(Exec (i,(Initialized s))))) . a ;
::_thesis: verum
end;

theorem Th15: :: SFMASTR1:15
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA
for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA
for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA
for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
let J be Program of SCM+FSA; ::_thesis: for i being parahalting good Instruction of SCM+FSA
for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
let i be parahalting good Instruction of SCM+FSA; ::_thesis: for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
let f be FinSeq-Location ; ::_thesis: ( ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) implies (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f )
set Mi = Macro i;
A1: IExec ((Macro i),p,s) = Exec (i,(Initialized s)) by SCMFSA6C:5;
assume  ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) ; ::_thesis: (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
then A2: ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) by SCMFSA7B:18, SCMFSA7B:19;
A3: J is_closed_on IExec ((Macro i),p,s),p by A2, A1;
 J is_halting_on IExec ((Macro i),p,s),p by A2, A1;
hence (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(IExec ((Macro i),p,s)))) . f by A3, Th8
.= (IExec (J,p,(IExec ((Macro i),p,s)))) . f
.= (IExec (J,p,(Exec (i,(Initialized s))))) . f by A1
.= (IExec (J,p,(Exec (i,(Initialized s))))) . f ;
::_thesis: verum
end;

theorem :: SFMASTR1:16
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let s be State of SCM+FSA; ::_thesis: for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let J be Program of SCM+FSA; ::_thesis: for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let i be parahalting good Instruction of SCM+FSA; ::_thesis: ( ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) implies DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) )
assume A1: ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) ; ::_thesis: DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
then A2: for f being FinSeq-Location holds (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f by Th15;
 for a being Int-Location holds (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a by A1, Th14;
hence  DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) by A2, SCMFSA_M:2; ::_thesis: verum
end;

begin


definition
canceled;
canceled;
let n be Element of NAT ;
let p be preProgram of SCM+FSA;
funcn -thNotUsed p ->  Int-Location equals :: SFMASTR1:def 4
n -thRWNotIn (UsedIntLoc p);
correctness
coherence
n -thRWNotIn (UsedIntLoc p) is Int-Location;
;
end;

:: deftheorem  SFMASTR1:def_2_:_
canceled;

:: deftheorem  SFMASTR1:def_3_:_
canceled;

:: deftheorem  defines -thNotUsed SFMASTR1:def_4_:_
 for n being Element of NAT
for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedIntLoc p);

notation
let n be Element of NAT ;
let 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 ;
let p be preProgram of SCM+FSA;
clustern -thNotUsed p ->  read-write ;
coherence
 not n -thNotUsed p is read-only ;
end;

begin

theorem :: SFMASTR1:17
canceled;

theorem :: SFMASTR1:18
canceled;

theorem :: SFMASTR1:19
canceled;

theorem :: SFMASTR1:20
canceled;

theorem :: SFMASTR1:21
canceled;

theorem Th22: :: SFMASTR1:22
for a, b being Int-Location holds
( a in UsedIntLoc (swap (a,b)) & b in UsedIntLoc (swap (a,b)) )
proof
let a, b be Int-Location; ::_thesis: ( a in UsedIntLoc (swap (a,b)) & b in UsedIntLoc (swap (a,b)) )
set FNU = FirstNotUsed (Macro (a := b));
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
A1: UsedIntLoc (swap (a,b)) = UsedIntLoc ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))))) by SCMFSA6C:def_3
.= (UsedIntLoc (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b))) \/ (UsedIntLoc (b := (FirstNotUsed (Macro (a := b))))) by SF_MASTR:30
.= (UsedIntLoc (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b))) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:14
.= ((UsedIntLoc ((FirstNotUsed (Macro (a := b))) := a)) \/ (UsedIntLoc (a := b))) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:31
.= ((UsedIntLoc ((FirstNotUsed (Macro (a := b))) := a)) \/ {a,b}) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:14
.= ({(FirstNotUsed (Macro (a := b))),a} \/ {a,b}) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:14
.= {(FirstNotUsed (Macro (a := b))),a,a,b} \/ {b,(FirstNotUsed (Macro (a := b)))} by ENUMSET1:5
.= {(FirstNotUsed (Macro (a := b))),a,a,b,b,(FirstNotUsed (Macro (a := b)))} by ENUMSET1:14 ;
hence  a in UsedIntLoc (swap (a,b)) by ENUMSET1:def_4; ::_thesis: b in UsedIntLoc (swap (a,b))
thus  b in UsedIntLoc (swap (a,b)) by A1, ENUMSET1:def_4; ::_thesis: verum
end;

definition
let N, result be Int-Location;
func Fib_macro (N,result) ->  Program of SCM+FSA equals :: SFMASTR1:def 5
((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
correctness
coherence
((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is Program of SCM+FSA;
;
end;

:: deftheorem  defines Fib_macro SFMASTR1:def_5_:_
 for N, result being Int-Location holds Fib_macro (N,result) = ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),((AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))))))) ";" (N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));

theorem :: SFMASTR1:23
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
proof
let p be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
let s be State of SCM+FSA; ::_thesis: for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
let N, result be read-write Int-Location; ::_thesis: ( N <> result implies for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N ) )
assume A1: N <> result ; ::_thesis: for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
set i0 = SubFrom (result,result);
set next = 1 -stRWNotIn {N,result};
set aux = 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))));
set Nsave = 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))));
set i00 = (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N;
set i1 = (1 -stRWNotIn {N,result}) := (intloc 0);
set i2 = (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))));
set i30 = AddTo (result,(1 -stRWNotIn {N,result}));
set I31 = swap (result,(1 -stRWNotIn {N,result}));
set i02 = ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
set s1 = IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s);
set p1 = p;
reconsider I301 = (AddTo (result,(1 -stRWNotIn {N,result}))) ";" (swap (result,(1 -stRWNotIn {N,result}))) as good parahalting Program of SCM+FSA ;
set I3 = Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301);
set i4 = N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))));
defpred S1[ Element of NAT ] means  for s1 being State of SCM+FSA st $1 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & s1 . (intloc 0) = 1 holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + $1) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + $1) ) ) );
let n be Element of NAT ; ::_thesis: ( n = s . N implies ( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N ) )
assume A2: n = s . N ; ::_thesis: ( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
 not 1 -stRWNotIn {N,result} in {N,result} by SCMFSA_M:25;
then A3: result <> 1 -stRWNotIn {N,result} by TARSKI:def_2;
A4: 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) <> 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by SCMFSA_M:26;
A5: 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) <> 1 -stRWNotIn {N,result} by Th22, SCMFSA_M:25;
A6: 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) <> result by Th22, SCMFSA_M:25;
A7: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A5, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A6, SCMFSA_2:65
.= (Initialized s) . N by SCMFSA_2:63
.= s . N by SCMFSA_M:37 ;
A8: not swap (result,(1 -stRWNotIn {N,result})) destroys 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by Th1, SCMFSA_M:25;
A9: ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is_closed_on Initialized s,p by SCMFSA7B:18;
A10: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A4, SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A5, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A6, SCMFSA_2:65
.= (Initialized s) . N by SCMFSA_2:63
.= s . N by SCMFSA_M:37 ;
A11: ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is_halting_on Initialized s,p by SCMFSA7B:19;
reconsider i02 = ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) as good Program of SCM+FSA ;
A12: not 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) in UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))) by SCMFSA_M:25;
A13: result in UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))) by Th22;
then  not Macro (AddTo (result,(1 -stRWNotIn {N,result}))) destroys 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by A12, SCMFSA7B:7, SCMFSA8C:48;
then A14: not I301 destroys 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by A8, SCMFSA8C:52;
A15: 1 -stRWNotIn {N,result} in UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))) by Th22;
A16: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A17: S1[n] ; ::_thesis: S1[n + 1]
thus  S1[n + 1] ::_thesis: verum
proof
let s1 be State of SCM+FSA; ::_thesis: ( n + 1 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & s1 . (intloc 0) = 1 implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) ) ) ) )
assume that
A18: n + 1 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) and
 s1 . (intloc 0) = 1 ; ::_thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) ) ) )
set s2 = IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1);
set p2 = p;
A19: s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) > 0 by A18, NAT_1:3;
then A20: (IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (n + 1) - 1 by A14, A18, SCMFSA8C:91
.= n ;
A21: (IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (intloc 0) = (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . (intloc 0) by SCMFSA6C:6
.= (IExec (I301,p,s1)) . (intloc 0) by SCMFSA_2:65
.= 1 by SCMFSA6B:11 ;
A22: DataPart (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) = DataPart (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) by A14, A19, SCMFSA8C:91;
hence (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_M:2
.= (IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A17, A20, A21
.= (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec (I301,p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A4, SCMFSA_2:65
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),p,(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6B:3, SCMFSA_M:25
.= (Initialized s1) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A6, SCMFSA_2:64
.= s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_M:37 ;
::_thesis: for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) )
let m be Element of NAT ; ::_thesis: ( s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) ) )
assume that
A23: s1 . result = Fib m and
A24: s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) ; ::_thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) )
A25: (IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (1 -stRWNotIn {N,result}) = (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec (I301,p,s1)) . (1 -stRWNotIn {N,result}) by A12, A15, SCMFSA_2:65
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),p,(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))))) . (1 -stRWNotIn {N,result}) by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))) . result by SCMFSA6C:10
.= ((Initialized s1) . result) + ((Initialized s1) . (1 -stRWNotIn {N,result})) by SCMFSA_2:64
.= (s1 . result) + ((Initialized s1) . (1 -stRWNotIn {N,result})) by SCMFSA_M:37
.= (s1 . result) + (s1 . (1 -stRWNotIn {N,result})) by SCMFSA_M:37
.= Fib ((m + 1) + 1) by A23, A24, PRE_FF:1 ;
A26: (IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . result = (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . result by SCMFSA6C:6
.= (IExec (I301,p,s1)) . result by A12, A13, SCMFSA_2:65
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),p,(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))))) . result by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:10
.= (Initialized s1) . (1 -stRWNotIn {N,result}) by A3, SCMFSA_2:64
.= Fib (m + 1) by A24, SCMFSA_M:37 ;
thus (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) . result by A22, SCMFSA_M:2
.= Fib ((m + 1) + n) by A17, A20, A21, A26, A25
.= Fib (m + (n + 1)) ; ::_thesis: (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1))
thus (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ";" (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) . (1 -stRWNotIn {N,result}) by A22, SCMFSA_M:2
.= Fib (((m + 1) + 1) + n) by A17, A20, A21, A26, A25
.= Fib ((m + 1) + (n + 1)) ; ::_thesis: verum
end;
end;
A27: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . result = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . result by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . result by A12, A13, SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)))) . result by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)) . result by A3, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . result by SCMFSA6C:8
.= ((Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . result) - ((Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . result) by SCMFSA_2:65
.= Fib 0 by PRE_FF:1 ;
A28: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (1 -stRWNotIn {N,result}) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stRWNotIn {N,result}) by A12, A15, SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= Fib (0 + 1) by PRE_FF:1, SCMFSA_M:9 ;
A29: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (intloc 0) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA_M:9 ;
then A30: Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301) is_closed_on IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s),p by A14, SCMFSA8C:86;
A31: S1[ 0 ]
proof
let s1 be State of SCM+FSA; ::_thesis: ( 0 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & s1 . (intloc 0) = 1 implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) ) ) ) )
assume that
A32: 0 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) and
A33: s1 . (intloc 0) = 1 ; ::_thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) ) ) )
A34: DataPart (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) = DataPart s1 by A32, A33, SCMFSA8C:90;
hence  (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_M:2; ::_thesis: for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) )
let m be Element of NAT ; ::_thesis: ( s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) ) )
assume that
A35: s1 . result = Fib m and
A36: s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) ; ::_thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) )
thus  (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) by A34, A35, SCMFSA_M:2; ::_thesis: (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0)
thus  (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) by A34, A36, SCMFSA_M:2; ::_thesis: verum
end;
A37: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A31, A16);
A38: Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301) is_halting_on IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s),p by A14, A29, SCMFSA8C:86;
A39: i02 ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)) is_closed_on Initialized s,p by A11, A30, A9, Th2;
hence (IExec ((Fib_macro (N,result)),p,s)) . result = (Exec ((N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec ((i02 ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)))) . result by A11, A30, A38, A9, Th3, Th11
.= (IExec ((i02 ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)) . result by A1, SCMFSA_2:63
.= (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . result by A30, A38, Th7
.= Fib (0 + n) by A37, A29, A27, A28, A7, A2
.= Fib n ;
::_thesis: (IExec ((Fib_macro (N,result)),p,s)) . N = s . N
thus (IExec ((Fib_macro (N,result)),p,s)) . N = (Exec ((N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec ((i02 ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)))) . N by A11, A30, A38, A9, A39, Th3, Th11
.= (IExec ((i02 ";" (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_2:63
.= (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ";" (SubFrom (result,result))) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A30, A38, Th7
.= s . N by A37, A29, A10, A7, A2 ; ::_thesis: verum
end;