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_on s,P & s . a = 0 holds

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

set D = Int-Locations \/ FinSeq-Locations;

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_on s,P & s . a = 0 holds

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

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

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

let a be read-write Int-Location; :: thesis: ( I is_halting_on s,P & s . a = 0 implies ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) ) )

set sI = Initialize s;

set PI = P +* I;

set s1 = Initialize s;

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

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

assume A1: I is_halting_on s,P ; :: thesis: ( not s . a = 0 or ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) ) )

set loc4 = (card I) + 3;

set i = a =0_goto 3;

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

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

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

.= 0 by FUNCOP_1:72 ;

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

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

assume A7: s . a = 0 ; :: thesis: ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

A8: 0 in dom (while=0 (a,I)) by AFINSQ_1:65;

A9: (P +* (while=0 (a,I))) /. (IC (Initialize s)) = (P +* (while=0 (a,I))) . (IC (Initialize s)) by PBOOLE:143;

(P +* (while=0 (a,I))) . 0 = (while=0 (a,I)) . 0 by A8, FUNCT_4:13

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

then A10: CurInstr ((P +* (while=0 (a,I))),(Initialize s)) = a =0_goto 3 by A5, A9;

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

.= Exec ((a =0_goto 3),(Initialize s)) by A10 ;

then ( ( for c being Int-Location holds (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) . c = (Initialize s) . c ) & ( for f being FinSeq-Location holds (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) . f = (Initialize s) . f ) ) by SCMFSA_2:70;

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

A13: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = 3 by A7, A11, A6, SCMFSA_2:70;

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

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

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

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

S_{1}[l]
by A16;

then A17: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0 by A1, Th3;

A18: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0 by A17;

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

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

A20: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1))) = 0 by A19, SCMFSA_2:69;

hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 ; :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ; :: thesis: verum

for I being really-closed MacroInstruction of SCM+FSA

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

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

set D = Int-Locations \/ FinSeq-Locations;

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_on s,P & s . a = 0 holds

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

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

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

let a be read-write Int-Location; :: thesis: ( I is_halting_on s,P & s . a = 0 implies ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) ) )

set sI = Initialize s;

set PI = P +* I;

set s1 = Initialize s;

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

defpred S

assume A1: I is_halting_on s,P ; :: thesis: ( not s . a = 0 or ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) ) )

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

S_{1}[k + 1]

reconsider l = LifeSpan ((P +* I),(Initialize s)) as Element of NAT by ORDINAL1:def 12;S

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

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

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

end;assume A3: S

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

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

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

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

hence ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) by A1, A3, Th2; :: thesis: verum

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

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

hence ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) by A1, A3, Th2; :: thesis: verum

set loc4 = (card I) + 3;

set i = a =0_goto 3;

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

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

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

.= 0 by FUNCOP_1:72 ;

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

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

assume A7: s . a = 0 ; :: thesis: ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

A8: 0 in dom (while=0 (a,I)) by AFINSQ_1:65;

A9: (P +* (while=0 (a,I))) /. (IC (Initialize s)) = (P +* (while=0 (a,I))) . (IC (Initialize s)) by PBOOLE:143;

(P +* (while=0 (a,I))) . 0 = (while=0 (a,I)) . 0 by A8, FUNCT_4:13

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

then A10: CurInstr ((P +* (while=0 (a,I))),(Initialize s)) = a =0_goto 3 by A5, A9;

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

.= Exec ((a =0_goto 3),(Initialize s)) by A10 ;

then ( ( for c being Int-Location holds (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) . c = (Initialize s) . c ) & ( for f being FinSeq-Location holds (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) . f = (Initialize s) . f ) ) by SCMFSA_2:70;

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

A13: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = 3 by A7, A11, A6, SCMFSA_2:70;

A14: S

proof

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

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

IC (Comput ((P +* I),(Initialize s),0)) = IC (Start-At (0,SCM+FSA)) by A15, FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

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

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

IC (Comput ((P +* I),(Initialize s),0)) = IC (Start-At (0,SCM+FSA)) by A15, FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

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

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

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

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

S

then A17: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0 by A1, Th3;

A18: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0 by A17;

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

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

A20: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1))) = 0 by A19, SCMFSA_2:69;

hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 ; :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))

A21: now :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 & k <> 0 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))

let k be Nat; :: thesis: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 2 & k <> 0 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I)) )

assume A22: k <= (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis: ( k <> 0 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I)) )

assume k <> 0 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I))

then consider n being Nat such that

A23: k = n + 1 by NAT_1:6;

( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 ) by NAT_1:13;

then A24: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k = (LifeSpan ((P +* I),(Initialize s))) + 2 ) by A22, XXREAL_0:1;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

end;assume A22: k <= (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis: ( k <> 0 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b

assume k <> 0 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b

then consider n being Nat such that

A23: k = n + 1 by NAT_1:6;

( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 ) by NAT_1:13;

then A24: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k = (LifeSpan ((P +* I),(Initialize s))) + 2 ) by A22, XXREAL_0:1;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

per cases
( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= (LifeSpan ((P +* I),(Initialize s))) + 2 )
by A24;

end;

suppose
k <= (LifeSpan ((P +* I),(Initialize s))) + 1
; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I))

then
n <= LifeSpan ((P +* I),(Initialize s))
by A23, XREAL_1:6;

then A25: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + n))) = (IC (Comput ((P +* I),(Initialize s),n))) + 3 by A16;

reconsider m = IC (Comput ((P +* I),(Initialize s),n)) as Element of NAT ;

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

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

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

then m in dom I by AMISTD_1:21, A26;

then m < card I by AFINSQ_1:66;

then A27: m + 3 < (card I) + 5 by XREAL_1:8;

card (while=0 (a,I)) = (card I) + 5 by SCMFSA_X:3;

hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A23, A25, A27, AFINSQ_1:66; :: thesis: verum

end;then A25: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + n))) = (IC (Comput ((P +* I),(Initialize s),n))) + 3 by A16;

reconsider m = IC (Comput ((P +* I),(Initialize s),n)) as Element of NAT ;

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

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

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

then m in dom I by AMISTD_1:21, A26;

then m < card I by AFINSQ_1:66;

then A27: m + 3 < (card I) + 5 by XREAL_1:8;

card (while=0 (a,I)) = (card I) + 5 by SCMFSA_X:3;

hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A23, A25, A27, AFINSQ_1:66; :: thesis: verum

suppose
k >= (LifeSpan ((P +* I),(Initialize s))) + 2
; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I))

then
k = (LifeSpan ((P +* I),(Initialize s))) + 2
by A22, XXREAL_0:1;

hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A20, AFINSQ_1:65; :: thesis: verum

end;hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A20, AFINSQ_1:65; :: thesis: verum

now :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))

hence
for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))

let k be Nat; :: thesis: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 2 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I)) )

assume A28: k <= (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b_{1})) in dom (while=0 (a,I))

end;assume A28: k <= (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ; :: thesis: verum