let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st I is_closed_on s,p & I is_halting_on s,p & s . a = 0 holds
DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I))))))
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st I is_closed_on s,p & I is_halting_on s,p & s . a = 0 holds
DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I))))))
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,p & I is_halting_on s,p & s . a = 0 holds
DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I))))))
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,p & I is_halting_on s,p & s . a = 0 implies DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I)))))) )
assume that
A1: ( I is_closed_on s,p & I is_halting_on s,p ) and
A2: s . a = 0 ; :: thesis: DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I))))))
set sI = s +* (Initialize I);
set pI = p +* I;
set s1 = s +* (Initialize (while=0 (a,I)));
set p1 = p +* (while=0 (a,I));
A3: while=0 (a,I) c= p +* (while=0 (a,I)) by FUNCT_4:26;
defpred S1[ Nat] means ( $1 <= LifeSpan ((p +* I),(s +* (Initialize I))) implies ( IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + $1))) = (IC (Comput ((p +* I),(s +* (Initialize I)),$1))) + 4 & DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + $1))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),$1)) ) );
A4: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
now
A6: k + 0 < k + 1 by XREAL_1:8;
assume k + 1 <= LifeSpan ((p +* I),(s +* (Initialize I))) ; :: thesis: ( IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + k) + 1))) = (IC (Comput ((p +* I),(s +* (Initialize I)),(k + 1)))) + 4 & DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + k) + 1))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(k + 1))) )
then k < LifeSpan ((p +* I),(s +* (Initialize I))) by A6, XXREAL_0:2;
hence ( IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + k) + 1))) = (IC (Comput ((p +* I),(s +* (Initialize I)),(k + 1)))) + 4 & DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + k) + 1))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),(k + 1))) ) by A1, A5, SCMFSA_9:19; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
set i = a =0_goto 4;
set s2 = Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),1);
set p2 = p +* (while=0 (a,I));
A7: IC in dom (Initialize (while=0 (a,I))) by COMPOS_1:141;
A8: IC (s +* (Initialize (while=0 (a,I)))) = IC (Initialize (while=0 (a,I))) by A7, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
not a in dom (Initialize (while=0 (a,I))) by SCMFSA6B:12;
then A9: (s +* (Initialize (while=0 (a,I)))) . a = s . a by FUNCT_4:12;
set loc4 = (card I) + 4;
A10: (p +* (while=0 (a,I))) /. (IC (s +* (Initialize (while=0 (a,I))))) = (p +* (while=0 (a,I))) . (IC (s +* (Initialize (while=0 (a,I))))) by PBOOLE:158;
0 in dom (while=0 (a,I)) by SCMFSA_9:10;
then (p +* (while=0 (a,I))) . 0 = (while=0 (a,I)) . 0 by FUNCT_4:14
.= (while=0 (a,I)) . 0
.= a =0_goto 4 by SCMFSA_9:11 ;
then A11: CurInstr ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I))))) = a =0_goto 4 by A8, A10;
A12: Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(0 + 1)) = Following ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),0))) by EXTPRO_1:4
.= Following ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I))))) by EXTPRO_1:3
.= Exec ((a =0_goto 4),(s +* (Initialize (while=0 (a,I))))) by A11 ;
then ( ( for c being Int-Location holds (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),1)) . c = (s +* (Initialize (while=0 (a,I)))) . c ) & ( for f being FinSeq-Location holds (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),1)) . f = (s +* (Initialize (while=0 (a,I)))) . f ) ) by SCMFSA_2:96;
then A13: DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),1)) = DataPart (s +* (Initialize (while=0 (a,I)))) by SCMFSA6A:38
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* (Initialize I)) by SCMFSA8A:11 ;
A14: IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),1)) = (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),1)) . (IC )
.= 4 by A2, A12, A9, SCMFSA_2:96 ;
A15: S1[ 0 ]
proof
assume 0 <= LifeSpan ((p +* I),(s +* (Initialize I))) ; :: thesis: ( IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + 0))) = (IC (Comput ((p +* I),(s +* (Initialize I)),0))) + 4 & DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + 0))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),0)) )
A16: IC in dom (Initialize I) by COMPOS_1:141;
IC (Comput ((p +* I),(s +* (Initialize I)),0)) = IC (s +* (Initialize I)) by EXTPRO_1:3
.= IC (Initialize I) by A16, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
hence ( IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + 0))) = (IC (Comput ((p +* I),(s +* (Initialize I)),0))) + 4 & DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + 0))) = DataPart (Comput ((p +* I),(s +* (Initialize I)),0)) ) by A14, A13, EXTPRO_1:3; :: thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A15, A4);
 then A17: S1[ LifeSpan ((p +* I),(s +* (Initialize I)))] ;
set s4 = Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1) + 1));
set p4 = p +* (while=0 (a,I));
set s3 = Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1));
set p3 = p +* (while=0 (a,I));
A18: (card I) + 4 in dom (while=0 (a,I)) by SCMFSA_9:13;
set s2 = Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + (LifeSpan ((p +* I),(s +* (Initialize I))))));
A19: CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + (LifeSpan ((p +* I),(s +* (Initialize I)))))))) = goto ((card I) + 4) by A1, A17, SCMFSA_9:20;
A20: Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1)) = Following ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + (LifeSpan ((p +* I),(s +* (Initialize I)))))))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 4)),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + (LifeSpan ((p +* I),(s +* (Initialize I)))))))) by A19 ;
then A21: ( ( for c being Int-Location holds (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) . c = (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + (LifeSpan ((p +* I),(s +* (Initialize I))))))) . c ) & ( for f being FinSeq-Location holds (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) . f = (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(1 + (LifeSpan ((p +* I),(s +* (Initialize I))))))) . f ) ) by SCMFSA_2:95;
A22: (p +* (while=0 (a,I))) . ((card I) + 4) = (p +* (while=0 (a,I))) . ((card I) + 4)
.= (while=0 (a,I)) . ((card I) + 4) by A18, A3, GRFUNC_1:8
.= goto 0 by SCMFSA_9:21 ;
A23: (p +* (while=0 (a,I))) /. (IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1)))) = (p +* (while=0 (a,I))) . (IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1)))) by PBOOLE:158;
IC (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) = (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) . (IC )
.= (card I) + 4 by A20, SCMFSA_2:95 ;
then A24: CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1)))) = goto 0 by A22, A23;
Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1) + 1)) = Following ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1)))) by EXTPRO_1:4
.= Exec ((goto 0),(Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1)))) by A24 ;
then ( ( for c being Int-Location holds (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1) + 1))) . c = (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) . c ) & ( for f being FinSeq-Location holds (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),(((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1) + 1))) . f = (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) . f ) ) by SCMFSA_2:95;
hence DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((LifeSpan ((p +* I),(s +* (Initialize I)))) + 3))) = DataPart (Comput ((p +* (while=0 (a,I))),(s +* (Initialize (while=0 (a,I)))),((1 + (LifeSpan ((p +* I),(s +* (Initialize I))))) + 1))) by SCMFSA6A:38
.= DataPart (Comput ((p +* I),(s +* (Initialize I)),(LifeSpan ((p +* I),(s +* (Initialize I)))))) by A17, A21, SCMFSA6A:38 ;
:: thesis: verum