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
IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I
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 IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I )
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: IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I
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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA ))))) in dom I by Def2;
A7: s +* (I +* (Start-At 0 ,SCM+FSA )) = (s +* I) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:15
.= (s +* (Start-At 0 ,SCM+FSA )) +* I by Th14
.= 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 (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 (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
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A11: ( 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:144;
A12: 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 AMI_1:14
.= 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:144;
A13: 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 AMI_1:14
.= 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 ;
A14: n <= n + 1 by NAT_1:12;
assume A15: 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 A16: 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 A11, A14, AMI_1:121, XXREAL_0:2;
n <= k by A15, A14, XXREAL_0:2;
then n <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) by A9, XXREAL_0:2;
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 A1, A5, A7, Th36, AMI_1:121;
then A17: 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 A18: 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 A16, 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 AMI_1:150;
Z: (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 AMI_1:150;
A19: 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 AMI_1:54, Y
.= (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 A18, FUNCT_4:14 ;
( dom I c= dom (I ';' I) & 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 AMI_1:54, SCMFSA6A:56, Z;
then ( Directed I c= I ';' I & 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) = (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 A17, FUNCT_4:14, SCMFSA6A:55;
then 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) = (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 A16, A18, 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 A11, A15, A14, A16, A19, A13, A12, 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 AMI_1:13;
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, SCMFSA6A:42;
then A20: S1[ 0 ] by FUNCT_7:28;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A20, A10);
then A21: 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 A21, FUNCT_7:29; :: thesis: verum
end;
then A22: IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA ))))) by AMI_1:121;
Y: (ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))))) = (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by AMI_1:150;
dom I misses dom (Start-At 0 ,SCM+FSA ) by SF_MASTR:64;
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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by A5, A6, GRFUNC_1:8;
then A23: I . (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by A6, Th7
.= CurInstr (ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) by AMI_1:54, Y
.= halt SCM+FSA by A1, A7, AMI_1:def 46 ;
IC (Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I)),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) in dom I by A8, A6, AMI_1:121;
then IC (Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I)),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) in dom (Directed I) by FUNCT_4:105;
then A24: ((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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by A22, FUNCT_4:14
.= goto (card I) by A6, A23, FUNCT_4:112 ;
A25: (s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I) = ((s +* I) +* (Start-At 0 ,SCM+FSA )) +* (Directed I) by FUNCT_4:15
.= ((s +* (Start-At 0 ,SCM+FSA )) +* I) +* (Directed I) by Th14
.= (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
.= 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 (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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by AMI_1:150;
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 (s +* (I +* (Start-At 0 ,SCM+FSA ))))) by AMI_1:144;
Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (Directed I)),((LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA ))))) by AMI_1:14
.= 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 (s +* (I +* (Start-At 0 ,SCM+FSA ))))) by A22, A24, AMI_1:54, Y, T ;
hence IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I by A7, A25, SCMFSA_2:95; :: thesis: verum