let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA

for I being really-closed good InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

let s be State of SCM+FSA; :: thesis: for I being really-closed good InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

let I be really-closed good InitHalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

let a be read-write Int-Location; :: thesis: ( s . a > 0 & while>0 (a,I) is InitHalting implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) )

set D = Data-Locations ;

assume that

A1: s . a > 0 and

A2: while>0 (a,I) is InitHalting ; :: thesis: DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

set sI = Initialized s;

set PI = P +* I;

set PW = P +* (while>0 (a,I));

set s3 = Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))));

set P3 = (P +* I) +* (while>0 (a,I));

set m1 = LifeSpan ((P +* I),(Initialized s));

set m3 = LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))));

A3: I c= P +* I by FUNCT_4:25;

A4: while>0 (a,I) c= (P +* I) +* (while>0 (a,I)) by FUNCT_4:25;

A5: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:25;

Initialize ((intloc 0) .--> 1) c= Initialized s by SCMFSA_M:13;

then A6: P +* (while>0 (a,I)) halts_on Initialized s by A2, A5;

set mW = LifeSpan ((P +* (while>0 (a,I))),(Initialized s));

A7: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by SCMFSA_M:13;

then A8: (P +* I) +* (while>0 (a,I)) halts_on Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A2, A4;

A9: DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) = DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))))

then A23: P +* I halts_on Initialized s by A3, Def1;

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

.= Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))) by A23, EXTPRO_1:23 ;

then Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) by A2, A7, Lm5, A5, A4;

then A24: Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) ;

A25: IExec ((while>0 (a,I)),P,(IExec (I,P,s))) = Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) by SCMFSA6B:def 1

.= Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))) by A8, A24, EXTPRO_1:23 ;

A26: LifeSpan ((P +* (while>0 (a,I))),(Initialized s)) <= (((LifeSpan ((P +* I),(Initialized s))) + 2) + (LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s))) by NAT_1:11;

IExec ((while>0 (a,I)),P,s) = Result ((P +* (while>0 (a,I))),(Initialized s)) by SCMFSA6B:def 1

.= Comput ((P +* (while>0 (a,I))),(Initialized s),(LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))) by A6, EXTPRO_1:23

.= Comput ((P +* (while>0 (a,I))),(Initialized s),(((LifeSpan ((P +* I),(Initialized s))) + 2) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) by A6, A26, EXTPRO_1:25 ;

then DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(((LifeSpan ((P +* I),(Initialized s))) + 2) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))))

.= DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))))) by A9, EXTPRO_1:4

.= DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) by A25 ;

hence DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) ; :: thesis: verum

for I being really-closed good InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

let s be State of SCM+FSA; :: thesis: for I being really-closed good InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

let I be really-closed good InitHalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

let a be read-write Int-Location; :: thesis: ( s . a > 0 & while>0 (a,I) is InitHalting implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) )

set D = Data-Locations ;

assume that

A1: s . a > 0 and

A2: while>0 (a,I) is InitHalting ; :: thesis: DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

set sI = Initialized s;

set PI = P +* I;

set PW = P +* (while>0 (a,I));

set s3 = Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))));

set P3 = (P +* I) +* (while>0 (a,I));

set m1 = LifeSpan ((P +* I),(Initialized s));

set m3 = LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))));

A3: I c= P +* I by FUNCT_4:25;

A4: while>0 (a,I) c= (P +* I) +* (while>0 (a,I)) by FUNCT_4:25;

A5: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:25;

Initialize ((intloc 0) .--> 1) c= Initialized s by SCMFSA_M:13;

then A6: P +* (while>0 (a,I)) halts_on Initialized s by A2, A5;

set mW = LifeSpan ((P +* (while>0 (a,I))),(Initialized s));

A7: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by SCMFSA_M:13;

then A8: (P +* I) +* (while>0 (a,I)) halts_on Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A2, A4;

A9: DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) = DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))))

proof

Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA_M:13;
reconsider Wg = while>0 (a,I) as good InitHalting MacroInstruction of SCM+FSA by A2;

set Cm3 = Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2));

A10: I is_halting_onInit s,P by Th23;

A11: IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 by A1, A10, Lm7;

A12: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, A10, Lm7

.= DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ;

A16: (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . (intloc 0) = 1 by A15, A5, Def2;

then Initialize ((intloc 0) .--> 1) c= Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) by SCMFSA_M:13;

then A20: P +* (while>0 (a,I)) halts_on Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) by A2, A5;

IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = IC (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) by A11, MEMSTR_0:28, SCMFSA_M:13;

then A21: Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) = Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A13, A17, SCMFSA_2:61;

then A22: Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) by A2, A7, Lm5, A5, A4;

LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)))) = LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) by A2, A7, Lm5, A5, A4, A21;

hence DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) = DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),(LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))))))) by A20, EXTPRO_1:25, NAT_1:11

.= DataPart (Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))))) by A20, EXTPRO_1:23

.= DataPart (Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) by A22

.= DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))))) by A8, EXTPRO_1:23 ;

:: thesis: verum

end;set Cm3 = Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2));

A10: I is_halting_onInit s,P by Th23;

A11: IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 by A1, A10, Lm7;

A12: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, A10, Lm7

.= DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ;

A13: now :: thesis: for f being FinSeq-Location holds (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . f

A15:
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA_M:13;let f be FinSeq-Location ; :: thesis: (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . f

A14: dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )} by SCMFSA_M:11;

( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58;

then not f in dom (Initialize ((intloc 0) .--> 1)) by A14, TARSKI:def 2;

hence (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f = (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) . f by FUNCT_4:11

.= (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . f by A12, SCMFSA_M:2 ;

:: thesis: verum

end;A14: dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )} by SCMFSA_M:11;

( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58;

then not f in dom (Initialize ((intloc 0) .--> 1)) by A14, TARSKI:def 2;

hence (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f = (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) . f by FUNCT_4:11

.= (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . f by A12, SCMFSA_M:2 ;

:: thesis: verum

A16: (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . (intloc 0) = 1 by A15, A5, Def2;

A17: now :: thesis: for b being Int-Location holds (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b

Initialized (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))
by A11, A16, SCMFSA_M:8;let b be Int-Location; :: thesis: (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b_{1} = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b_{1}

end;per cases
( b <> intloc 0 or b = intloc 0 )
;

end;

suppose A18:
b <> intloc 0
; :: thesis: (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b_{1} = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b_{1}

A19:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA_M:11;

b <> IC by SCMFSA_2:56;

then not b in dom (Initialize ((intloc 0) .--> 1)) by A18, A19, TARSKI:def 2;

hence (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b = (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) . b by FUNCT_4:11

.= (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b by A12, SCMFSA_M:2 ;

:: thesis: verum

end;b <> IC by SCMFSA_2:56;

then not b in dom (Initialize ((intloc 0) .--> 1)) by A18, A19, TARSKI:def 2;

hence (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b = (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) . b by FUNCT_4:11

.= (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b by A12, SCMFSA_M:2 ;

:: thesis: verum

suppose
b = intloc 0
; :: thesis: (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b_{1} = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b_{1}

hence
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . b
by A16, SCMFSA_M:13, SCMFSA_M:30; :: thesis: verum

end;then Initialize ((intloc 0) .--> 1) c= Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) by SCMFSA_M:13;

then A20: P +* (while>0 (a,I)) halts_on Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) by A2, A5;

IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = IC (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) by A11, MEMSTR_0:28, SCMFSA_M:13;

then A21: Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) = Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A13, A17, SCMFSA_2:61;

then A22: Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) by A2, A7, Lm5, A5, A4;

LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)))) = LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) by A2, A7, Lm5, A5, A4, A21;

hence DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) = DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),(LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))))))) by A20, EXTPRO_1:25, NAT_1:11

.= DataPart (Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))))) by A20, EXTPRO_1:23

.= DataPart (Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) by A22

.= DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))))) by A8, EXTPRO_1:23 ;

:: thesis: verum

then A23: P +* I halts_on Initialized s by A3, Def1;

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

.= Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))) by A23, EXTPRO_1:23 ;

then Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) by A2, A7, Lm5, A5, A4;

then A24: Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))) ;

A25: IExec ((while>0 (a,I)),P,(IExec (I,P,s))) = Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) by SCMFSA6B:def 1

.= Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))) by A8, A24, EXTPRO_1:23 ;

A26: LifeSpan ((P +* (while>0 (a,I))),(Initialized s)) <= (((LifeSpan ((P +* I),(Initialized s))) + 2) + (LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s))) by NAT_1:11;

IExec ((while>0 (a,I)),P,s) = Result ((P +* (while>0 (a,I))),(Initialized s)) by SCMFSA6B:def 1

.= Comput ((P +* (while>0 (a,I))),(Initialized s),(LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))) by A6, EXTPRO_1:23

.= Comput ((P +* (while>0 (a,I))),(Initialized s),(((LifeSpan ((P +* I),(Initialized s))) + 2) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) by A6, A26, EXTPRO_1:25 ;

then DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(((LifeSpan ((P +* I),(Initialized s))) + 2) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))))

.= DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))))) by A9, EXTPRO_1:4

.= DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) by A25 ;

hence DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) ; :: thesis: verum