begin
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
Lm1:
for l being Element of NAT holds
( dom (0 .--> (goto l)) = {0} & 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
:: deftheorem SCMFSA8A:def 1 :
canceled;
:: deftheorem defines Goto SCMFSA8A:def 2 :
for l being Element of NAT holds Goto l = 0 .--> (goto l);
:: deftheorem Def3 defines is_pseudo-closed_on SCMFSA8A:def 3 :
for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA holds
( P is_pseudo-closed_on s iff ex k being Element of NAT st
( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),k)) = card (ProgramPart P) & ( for n being Element of NAT st n < k holds
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P ) ) );
:: deftheorem defines pseudo-paraclosed SCMFSA8A:def 4 :
for P being initial FinPartState of SCM+FSA holds
( P is pseudo-paraclosed iff for s being State of SCM+FSA holds P is_pseudo-closed_on s );
definition
let s be
State of
SCM+FSA;
let P be
initial FinPartState of
SCM+FSA;
assume A1:
P is_pseudo-closed_on s
;
func pseudo-LifeSpan (
s,
P)
-> Element of
NAT means :
Def5:
(
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),it)) = card (ProgramPart P) & ( for
n being
Element of
NAT st not
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P holds
it <= n ) );
existence
ex b1 being Element of NAT st
( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),b1)) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P holds
b1 <= n ) )
uniqueness
for b1, b2 being Element of NAT st IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),b1)) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P holds
b1 <= n ) & IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),b2)) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P holds
b2 <= n ) holds
b1 = b2
end;
:: deftheorem Def5 defines pseudo-LifeSpan SCMFSA8A:def 5 :
for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for b3 being Element of NAT holds
( b3 = pseudo-LifeSpan (s,P) iff ( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),b3)) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P holds
b3 <= n ) ) );
theorem Th28:
theorem
theorem
theorem Th31:
for
s being
State of
SCM+FSA for
P being
initial FinPartState of
SCM+FSA st
P is_pseudo-closed_on s holds
for
n being
Element of
NAT st
n < pseudo-LifeSpan (
s,
P) holds
(
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P &
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),
(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)))
<> halt SCM+FSA )
theorem Th32:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA st
I is_pseudo-closed_on s holds
for
k being
Element of
NAT st
k <= pseudo-LifeSpan (
s,
I) holds
Comput (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA)))),
k),
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
k)
equal_outside NAT
theorem Th33:
theorem
theorem Th35:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s holds
for
k being
Element of
NAT st
k <= LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) holds
(
Comput (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA)))),
k),
Comput (
(ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),
(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),
k)
equal_outside NAT &
CurInstr (
(ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),
(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)))
<> halt SCM+FSA )
theorem Th36:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s holds
(
IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = card I &
DataPart (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)))))))) = DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) )
Lm2:
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( Directed I is_pseudo-closed_on s & pseudo-LifeSpan (s,(Directed I)) = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 )
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th41:
theorem Th42:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s holds
( ( for
k being
Element of
NAT st
k <= LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) holds
(
IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k)) &
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),
(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)))
= CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))) ) ) &
DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = DataPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) &
IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) )
theorem Th43:
for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA st
I is_closed_on Initialized s &
I is_halting_on Initialized s holds
( ( for
k being
Element of
NAT st
k <= LifeSpan (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I))) holds
(
IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k)) = IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k)) &
CurInstr (
(ProgramPart (s +* (Initialized (Directed I)))),
(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k)))
= CurInstr (
(ProgramPart (s +* (Initialized (I ';' J)))),
(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k))) ) ) &
DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) &
IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) )
theorem Th44:
theorem Th45:
Lm3:
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = card I & DataPart (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)))))))) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) & ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) & LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s & I ';' (Stop SCM+FSA) is_halting_on s )
theorem
theorem
Lm4:
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s & I is_halting_on Initialized s holds
( IC (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) & ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA)))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA))) & LifeSpan ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1 )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
Lm5:
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (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)))))))) = DataPart (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2 holds
CurInstr ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) holds
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) ) & IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = card I & ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) & LifeSpan ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2 )
theorem
theorem
Lm6:
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s & I is_halting_on Initialized s holds
( IC (Comput ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 2 holds
CurInstr ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(Comput ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
IC (Comput ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) ) & IC (Comput ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))) halts_on s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) & LifeSpan ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 2 )
theorem
theorem
theorem