let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location st I is_closed_on s,P & I is_halting_on s,P & s . a = 0 holds
( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 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 Program of
for a being read-write Int-Location st I is_closed_on s,P & I is_halting_on s,P & s . a = 0 holds
( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )
let I be Program of ; :: thesis: for a being read-write Int-Location st I is_closed_on s,P & I is_halting_on s,P & s . a = 0 holds
( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 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_closed_on s,P & I is_halting_on s,P & s . a = 0 implies ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) ) )
assume A1: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or not s . a = 0 or ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 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 S1[ 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))) + 4 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + $1))) = DataPart (Comput ((P +* I),(Initialize s),$1)) ) );
assume A2: 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))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) ) )
A3: now :: thesis: for k being Element of NAT st S1[k] holds
S1[k + 1]
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
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)))) + 4 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) )
A5: 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)))) + 4 & 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 A5, XXREAL_0:2;
hence ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 4 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) by A1, A2, A4, Th19; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider l = LifeSpan ((P +* I),(Initialize s)) as Element of NAT ;
set loc4 = (card I) + 4;
set i = a =0_goto 4;
set s2 = Comput ((P +* (while=0 (a,I))),(Initialize s),1);
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A6: 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 A7: (Initialize s) . a = s . a by FUNCT_4:11;
assume A8: s . a = 0 ; :: thesis: ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )
A9: 0 in dom (while=0 (a,I)) by Th10;
A10: (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 A9, FUNCT_4:13
.= a =0_goto 4 by Th11 ;
then A11: CurInstr ((P +* (while=0 (a,I))),(Initialize s)) = a =0_goto 4 by A6, A10;
A12: 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
.= Following ((P +* (while=0 (a,I))),(Initialize s))
.= Exec ((a =0_goto 4),(Initialize s)) by A11 ;
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 A13: DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = DataPart (Initialize s) by SCMFSA_M:2
.= DataPart (Initialize s) ;
A14: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = 4 by A8, A12, A7, SCMFSA_2:70;
A15: S1[ 0 ]
proof
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))) + 4 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize s),0)) )
A16: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
IC (Comput ((P +* I),(Initialize s),0)) = IC (Initialize 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 s),(1 + 0))) = (IC (Comput ((P +* I),(Initialize s),0))) + 4 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize s),0)) ) by A14, A13; :: thesis: verum
end;
A17: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A15, A3);
 set s4 = Comput ((P +* (while=0 (a,I))),(Initialize s),(((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1) + 1));
set s3 = Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1));
A18: (card I) + 4 in dom (while=0 (a,I)) by Th13;
set s2 = Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))));
S1[l] by A17;
then A19: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto ((card I) + 4) by A1, A2, Th20;
A20: 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 ((card I) + 4)),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) by A19 ;
A21: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1))) = (card I) + 4 by A20, SCMFSA_2:69;
A22: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1)))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1)))) by PBOOLE:143;
(P +* (while=0 (a,I))) . ((card I) + 4) = (while=0 (a,I)) . ((card I) + 4) by A18, FUNCT_4:13
.= goto 0 by Th21 ;
then A23: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1)))) = goto 0 by A21, A22;
A24: Comput ((P +* (while=0 (a,I))),(Initialize s),(((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1) + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1)))) by EXTPRO_1:3
.= Exec ((goto 0),(Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1)))) by A23 ;
A25: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1) + 1))) = 0 by A24, SCMFSA_2:69;
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 ; :: thesis: for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))
A26: (((LifeSpan ((P +* I),(Initialize s))) + 1) + 1) + 1 = (LifeSpan ((P +* I),(Initialize s))) + (2 + 1) ;
A27: now :: thesis: for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 & k <> 0 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))
let k be Element of NAT ; :: thesis: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 3 & k <> 0 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I)) )
assume A28: k <= (LifeSpan ((P +* I),(Initialize s))) + 3 ; :: thesis: ( k <> 0 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I)) )
assume k <> 0 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
then consider n being Nat such that
A29: 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 A30: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k = ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 or k > ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 ) by 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))) + 1) + 1 or k >= (LifeSpan ((P +* I),(Initialize s))) + 3 ) by A26, A30, NAT_1:13;
suppose k <= (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
then n <= LifeSpan ((P +* I),(Initialize s)) by A29, XREAL_1:6;
then A31: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + n))) = (IC (Comput ((P +* I),(Initialize s),n))) + 4 by A17;
reconsider m = IC (Comput ((P +* I),(Initialize s),n)) as Element of NAT ;
m in dom I by A1, SCMFSA7B:def 6;
then m < card I by AFINSQ_1:66;
then A32: m + 4 < (card I) + 6 by XREAL_1:8;
card (while=0 (a,I)) = (card I) + 6 by Th4;
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A29, A31, A32, AFINSQ_1:66; :: thesis: verum
end;
suppose k = ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A21, Th13; :: thesis: verum
end;
suppose k >= (LifeSpan ((P +* I),(Initialize s))) + 3 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
then k = (LifeSpan ((P +* I),(Initialize s))) + 3 by A28, XXREAL_0:1;
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A25, Th10; :: thesis: verum
end;
end;
end;
now :: thesis: for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I))
let k be Element of NAT ; :: thesis: ( k <= (LifeSpan ((P +* I),(Initialize s))) + 3 implies IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I)) )
assume A33: k <= (LifeSpan ((P +* I),(Initialize s))) + 3 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A9, A6, EXTPRO_1:2; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),b1)) in dom (while=0 (a,I))
hence IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) by A27, A33; :: thesis: verum
end;
end;
end;
hence for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ; :: thesis: verum