let s be State of SCM+FSA; :: thesis: for I being paraclosed Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I & Directed I c= s & Start-At (0,SCM+FSA) c= s holds
DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))
set A = NAT ;
let I be paraclosed Program of SCM+FSA; :: thesis: ( ProgramPart (s +* I) halts_on s +* I & Directed I c= s & Start-At (0,SCM+FSA) c= s implies DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) )
assume that
A1: ProgramPart (s +* I) halts_on s +* I and
A2: Directed I c= s and
A3: Start-At (0,SCM+FSA) c= s ; :: thesis: DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))
set sISA0 = s +* (I +* (Start-At (0,SCM+FSA)));
set s2 = (s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I);
set IAt = I +* (Start-At (0,SCM+FSA));
A4: dom (Directed I) = dom I by FUNCT_4:105;
set m = LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))));
set l1 = IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))));
A5: I +* (Start-At (0,SCM+FSA)) c= s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A6: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) in dom I by Def2;
A7: s +* (I +* (Start-At (0,SCM+FSA))) = Initialize (s +* I) by FUNCT_4:15
.= (Initialize s) +* I by COMPOS_1:83
.= s +* I by A3, FUNCT_4:79 ;
A8: now
set s1 = (s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I);
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) implies Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),k) equal_outside NAT )
defpred S1[ Nat] means ( $1 <= k implies Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),$1), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),$1) equal_outside NAT );
assume A9: k <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) ; :: thesis: Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),k) equal_outside NAT
A10: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
A11: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
A12: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A13: ( n <= k implies Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n) equal_outside NAT ) ; :: thesis: S1[n + 1]
T: ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)) = ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n)) by AMI_1:123;
A14: Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(n + 1)) = Following ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n)))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) by T ;
T: ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)) = ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n)) by AMI_1:123;
A15: Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),(n + 1)) = Following ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n)))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) by T ;
A16: n <= n + 1 by NAT_1:12;
assume A17: n + 1 <= k ; :: thesis: Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),(n + 1)), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(n + 1)) equal_outside NAT
then A18: IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n)) = IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n)) by A13, A16, COMPOS_1:24, XXREAL_0:2;
n <= k by A17, A16, XXREAL_0:2;
then n <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) by A9, XXREAL_0:2;
then Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n) equal_outside NAT by A1, Th36, A7, A5;
then IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n)) by COMPOS_1:24;
then A19: IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n)) in dom I by A5, Def2;
then A20: IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n)) in dom (Directed I) by A18, FUNCT_4:105;
Y: (ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) /. (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) = (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n)) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) by COMPOS_1:38;
A21: CurInstr ((ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) = ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) by Y, AMI_1:54
.= (Directed I) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),n))) by A20, FUNCT_4:14 ;
Y: (ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) /. (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) = (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n)) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) by COMPOS_1:38;
CurInstr ((ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) = ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) by Y, AMI_1:54
.= (I ';' I) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) by A12, A19, FUNCT_4:14
.= (Directed I) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),n))) by A11, A18, A20, GRFUNC_1:8 ;
hence Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),(n + 1)), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(n + 1)) equal_outside NAT by A13, A17, A16, A18, A21, A15, A14, SCMFSA6A:32, XXREAL_0:2; :: thesis: verum
end;
( Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),0) = (s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I) & Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),0) = (s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I) ) by EXTPRO_1:3;
then Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),0), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),0) equal_outside NAT by FUNCT_7:107, FUNCT_7:133;
then A22: S1[ 0 ] by FUNCT_7:28;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A22, A10);
then A23: Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),k), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),k) equal_outside NAT ;
Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (I ';' I)),k) equal_outside NAT by A1, A7, A9, Th36, FUNCT_4:26;
hence Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),k) equal_outside NAT by A23, FUNCT_7:29; :: thesis: verum
end;
then A24: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) = IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) by COMPOS_1:24;
Y: (ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) /. (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by COMPOS_1:38;
TX: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
dom I misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then I c= I +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
then dom I c= dom (I +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
then (s +* (I +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (I +* (Start-At (0,SCM+FSA))) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by A5, A6, GRFUNC_1:8;
then A25: I . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (s +* (I +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by A6, Th7
.= CurInstr ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by Y, TX, AMI_1:54
.= halt SCM+FSA by A1, A7, EXTPRO_1:def 14 ;
IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) in dom I by A8, A6, COMPOS_1:24;
then IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) in dom (Directed I) by FUNCT_4:105;
then A26: ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (Directed I) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by A24, FUNCT_4:14
.= goto (card I) by A6, A25, FUNCT_4:112 ;
(s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I) = (Initialize (s +* I)) +* (Directed I) by FUNCT_4:15
.= ((Initialize s) +* I) +* (Directed I) by COMPOS_1:83
.= (s +* I) +* (Directed I) by A3, FUNCT_4:79
.= s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A4, FUNCT_4:20 ;
then A27: (s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I) = s by A2, FUNCT_4:79;
Y: (ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) /. (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) = (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . (IC (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by COMPOS_1:38;
T: ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)) = ProgramPart (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1)) = Following ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by EXTPRO_1:4
.= Exec ((goto (card I)),(Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by A24, A26, Y, T, AMI_1:54 ;
then ( ( for a being Int-Location holds (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) . a = (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . a ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) . f = (Comput ((ProgramPart ((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I))),((s +* (I +* (Start-At (0,SCM+FSA)))) +* (Directed I)),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . f ) ) by SCMFSA_2:95;
hence DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by A7, A27, SCMFSA6A:38; :: thesis: verum