let s be State of SCM+FSA; 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 ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I
set A = NAT ;
let I be paraclosed Program of SCM+FSA; ( 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 ((ProgramPart (s +* I)),(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
; IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(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 ((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 ;
( 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)))))
;
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 ;
( 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 )
;
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;
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 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;
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 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
;
A14:
n <= n + 1
by NAT_1:12;
assume A15:
n + 1
<= k
;
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, COMPOS_1:24, XXREAL_0:2;
n <= k
by A15, A14, 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
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, COMPOS_1:24;
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 COMPOS_1:38;
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 COMPOS_1:38;
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 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 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 Z, AMI_1:54, SCMFSA6A:56;
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;
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 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;
verum end;
then A22:
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 A23: 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 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 ((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 A22, FUNCT_4:14
.=
goto (card I)
by A6, A23, FUNCT_4:112
;
A25: (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
.=
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 A22, A24, Y, T, AMI_1:54
;
hence
IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I
by A7, A25, SCMFSA_2:95; verum