begin
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
theorem
canceled;
theorem
canceled;
theorem Th3:
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 Def4 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