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

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

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

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

let a be read-write Int-Location; :: thesis: ( I is_halting_onInit s,P & s . a > 0 implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) ) )

set D = Data-Locations ;

set s0 = Initialized s;

set s1 = Initialize (Initialized s);

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

set PI = P +* I;

set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1);

set i = a >0_goto 3;

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

defpred S_{1}[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + $1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),$1))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + $1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),$1)) ) );

set loc4 = (card I) + 2;

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

A2: Initialize (Initialized s) = Initialize (Initialized s)

.= Initialize (Initialized s)

.= Initialized s by MEMSTR_0:44 ;

assume I is_halting_onInit s,P ; :: thesis: ( not s . a > 0 or ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) ) )

then A3: P +* I halts_on Initialized s ;

A4: I is_halting_on Initialized s,P by A3, A2;

then A8: (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by A1, GRFUNC_1:2

.= a >0_goto 3 by SCMFSA_X:10 ;

IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

then A9: IC (Initialize (Initialized s)) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

A10: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),0))) by EXTPRO_1:3

.= Following ((P +* (while>0 (a,I))),(Initialize (Initialized s)))

.= Exec ((a >0_goto 3),(Initialize (Initialized s))) by A9, A8, PBOOLE:143 ;

then A11: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f = (Initialize (Initialized s)) . f by SCMFSA_2:71;

for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . c = (Initialize (Initialized s)) . c by A10, SCMFSA_2:71;

then A12: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) = DataPart (Initialize (Initialized s)) by A11, SCMFSA_M:2

.= DataPart (Initialize (Initialized s)) ;

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

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

not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;

then A13: (Initialize (Initialized s)) . a = (Initialized s) . a by FUNCT_4:11;

assume s . a > 0 ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

then A14: (Initialized s) . a > 0 by SCMFSA_M:37;

A15: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A15, A5);

then A17: S_{1}[ LifeSpan ((P +* I),(Initialize (Initialized s)))]
;

A18: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by EXTPRO_1:3

.= Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by A4, A17, SCMFSA_9:40 ;

A19: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) = Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by A18;

then A20: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) . f by SCMFSA_2:69;

for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) . c = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) . c by A18, SCMFSA_2:69;

then A21: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) = DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) by A20, SCMFSA_M:2;

A22: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) by A22;

hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 by A19, SCMFSA_2:69; :: thesis: 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)))))

A23: Initialize (Initialized s) = Initialized s by MEMSTR_0:44;

thus 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 A23, A17, A21; :: thesis: verum

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

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

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

let a be read-write Int-Location; :: thesis: ( I is_halting_onInit s,P & s . a > 0 implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) ) )

set D = Data-Locations ;

set s0 = Initialized s;

set s1 = Initialize (Initialized s);

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

set PI = P +* I;

set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1);

set i = a >0_goto 3;

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

defpred S

set loc4 = (card I) + 2;

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

A2: Initialize (Initialized s) = Initialize (Initialized s)

.= Initialize (Initialized s)

.= Initialized s by MEMSTR_0:44 ;

assume I is_halting_onInit s,P ; :: thesis: ( not s . a > 0 or ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) ) )

then A3: P +* I halts_on Initialized s ;

A4: I is_halting_on Initialized s,P by A3, A2;

A5: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

0 in dom (while>0 (a,I))
by AFINSQ_1:65;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A6: S

now :: thesis: ( k + 1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) ) )

hence
SA7:
k + 0 < k + 1
by XREAL_1:6;

assume k + 1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) )

then k < LifeSpan ((P +* I),(Initialize (Initialized s))) by A7, XXREAL_0:2;

hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) ) by A4, A6, SCMFSA_9:39; :: thesis: verum

end;assume k + 1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) )

then k < LifeSpan ((P +* I),(Initialize (Initialized s))) by A7, XXREAL_0:2;

hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) ) by A4, A6, SCMFSA_9:39; :: thesis: verum

then A8: (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by A1, GRFUNC_1:2

.= a >0_goto 3 by SCMFSA_X:10 ;

IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

then A9: IC (Initialize (Initialized s)) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

A10: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),0))) by EXTPRO_1:3

.= Following ((P +* (while>0 (a,I))),(Initialize (Initialized s)))

.= Exec ((a >0_goto 3),(Initialize (Initialized s))) by A9, A8, PBOOLE:143 ;

then A11: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f = (Initialize (Initialized s)) . f by SCMFSA_2:71;

for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . c = (Initialize (Initialized s)) . c by A10, SCMFSA_2:71;

then A12: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) = DataPart (Initialize (Initialized s)) by A11, SCMFSA_M:2

.= DataPart (Initialize (Initialized s)) ;

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

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

not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;

then A13: (Initialize (Initialized s)) . a = (Initialized s) . a by FUNCT_4:11;

assume s . a > 0 ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & 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))))) )

then A14: (Initialized s) . a > 0 by SCMFSA_M:37;

A15: S

proof

for k being Nat holds S
assume
0 <= LifeSpan ((P +* I),(Initialize (Initialized s)))
; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),0)) )

A16: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

IC (Comput ((P +* I),(Initialize (Initialized s)),0)) = IC (Initialize (Initialized s))

.= IC (Start-At (0,SCM+FSA)) by A16, FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),0)) ) by A14, A10, A13, A12, SCMFSA_2:71; :: thesis: verum

end;A16: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

IC (Comput ((P +* I),(Initialize (Initialized s)),0)) = IC (Initialize (Initialized s))

.= IC (Start-At (0,SCM+FSA)) by A16, FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),0)) ) by A14, A10, A13, A12, SCMFSA_2:71; :: thesis: verum

then A17: S

A18: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by EXTPRO_1:3

.= Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by A4, A17, SCMFSA_9:40 ;

A19: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) = Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by A18;

then A20: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) . f by SCMFSA_2:69;

for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) . c = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) . c by A18, SCMFSA_2:69;

then A21: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) = DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) by A20, SCMFSA_M:2;

A22: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) by A22;

hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 by A19, SCMFSA_2:69; :: thesis: 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)))))

A23: Initialize (Initialized s) = Initialized s by MEMSTR_0:44;

thus 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 A23, A17, A21; :: thesis: verum