let I, J be 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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (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)),(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 (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
let s be State of SCM+FSA ; ( I is_closed_on s & I is_halting_on s implies ( 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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (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)),(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 (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 ) )
assume A1:
I is_closed_on s
; ( not I is_halting_on s or ( 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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (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)),(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 (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 ) )
A2: card ((Goto ((card J) + 1)) ';' J) =
(card (Goto ((card J) + 1))) + (card J)
by SCMFSA6A:61
.=
1 + (card J)
by Lm1
;
A3:
ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1)) c= Relocated (Stop SCM+FSA ),((card J) + 1)
by RELAT_1:88;
x:
0 in dom (Stop SCM+FSA )
by SCMNORM:2;
A4: card ((Goto ((card J) + 1)) ';' J) =
(card (Goto ((card J) + 1))) + (card J)
by SCMFSA6A:61
.=
(card J) + 1
by Lm1
;
A5:
((card I) + (card J)) + 1 = ((card J) + 1) + (card I)
;
A6:
0 in dom (ProgramPart (Stop SCM+FSA ))
by x, AMI_1:105;
set J2 = (Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ));
set s2 = s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
set s1 = s +* (I +* (Start-At 0 ,SCM+FSA ));
assume A7:
I is_halting_on s
; ( 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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (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)),(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 (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
dom (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) = { (m + ((card J) + 1)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA )) }
by SCMFSA_5:3;
then A8:
0 + ((card J) + 1) in dom (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1)))
by A6;
A9:
dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ';' J)
by SCMFSA6A:56;
A10:
0 in dom (Goto ((card J) + 1))
by Lm1;
A11: ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) . 0 =
(((Goto ((card J) + 1)) ';' J) ';' (Stop SCM+FSA )) . 0
by SCMFSA6A:67
.=
(Directed ((Goto ((card J) + 1)) ';' J)) . 0
by A10, A9, Th28
.=
((Goto ((card J) + 1)) ';' (Directed J)) . 0
by SCMFSA6A:66
.=
(Directed (Goto ((card J) + 1))) . 0
by A10, Th28
.=
(Goto ((card J) + 1)) . 0
by SCMFSA6A:63
.=
goto ((card J) + 1)
by Lm1
;
A12:
ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)) c= Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)
by RELAT_1:88;
A13: ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ) =
(I ';' (Goto ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))
by SCMFSA6A:67
.=
I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))
by SCMFSA6A:67
;
then A14:
DataPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = 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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))
by A1, A7, Th42;
I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) c= (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At 0 ,SCM+FSA )
by Th9;
then A15:
dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) c= dom ((I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) c= (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At 0 ,SCM+FSA )
by Th9;
then A16:
dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) c= dom ((I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
A17: card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) =
(card (Goto ((card J) + 1))) + (card (J ';' (Stop SCM+FSA )))
by SCMFSA6A:61
.=
1 + (card (J ';' (Stop SCM+FSA )))
by Lm1
;
then A18:
0 + 1 <= card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))
by NAT_1:11;
A19:
card (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) = (card I) + (card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by SCMFSA6A:61;
then
(card I) + 0 < card (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by A18, XREAL_1:8;
then A20:
card I in dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by SCMFSA6A:15;
x:
card (Stop SCM+FSA ) = 1
by SCMNORM:3;
card (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) =
(card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCM+FSA )))
by A19, SCMFSA6A:67
.=
(card I) + (((card J) + 1) + 1)
by A4, x, SCMFSA6A:61
.=
(((card I) + (card J)) + 1) + 1
;
then
((card I) + (card J)) + 1 < card (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by NAT_1:13;
then A21:
((card I) + (card J)) + 1 in dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by SCMFSA6A:15;
dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) = dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))
by AMI_1:105;
then A22:
0 in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by A18, SCMFSA6A:15;
then
0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) }
;
then A23:
0 + (card I) in dom (ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)))
by SCMFSA_5:3;
x:
card (Stop SCM+FSA ) = 1
by SCMNORM:3;
y:
(Stop SCM+FSA ) . 0 = halt SCM+FSA
by AFINSQ_1:38;
card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) =
1 + ((card J) + (card (Stop SCM+FSA )))
by A17, SCMFSA6A:61
.=
(card J) + (1 + (card (Stop SCM+FSA )))
;
then
(card J) + 1 < card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))
by x, XREAL_1:8;
then
(card J) + 1 in dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))
by SCMFSA6A:15;
then A24:
(card J) + 1 in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by AMI_1:105;
A25: ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) . ((card J) + 1) =
(((Goto ((card J) + 1)) ';' J) ';' (Stop SCM+FSA )) . ((card J) + 1)
by SCMFSA6A:67
.=
(ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) . ((card J) + 1)
by A2, A8, FUNCT_4:14
.=
(Relocated (Stop SCM+FSA ),((card J) + 1)) . (0 + ((card J) + 1))
by A3, A8, GRFUNC_1:8
.=
IncAddr (halt SCM+FSA ),((card J) + 1)
by A6, y, SCMFSA_5:7
.=
halt SCM+FSA
by SCMFSA_4:8
;
A26:
ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)) c= Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)
by RELAT_1:88;
dom (ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I))) = { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) }
by SCMFSA_5:3;
then A27:
((card I) + (card J)) + 1 in dom (ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)))
by A24, A5;
Y:
(ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) /. (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) = (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)))
by AMI_1:150;
A28:
IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = 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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))
by A1, A7, A13, Th42;
then A29: CurInstr (ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))),(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) =
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . (card I)
by A1, A7, Th36, Y
.=
(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . (card I)
by AMI_1:54
.=
((I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At 0 ,SCM+FSA )) . (card I)
by A13, A16, A20, FUNCT_4:14
.=
(I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) . (card I)
by A20, SCMFSA6B:7
.=
(ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I))) . (card I)
by A23, FUNCT_4:14
.=
(Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)) . (0 + (card I))
by A23, A12, GRFUNC_1:8
.=
IncAddr (goto ((card J) + 1)),(card I)
by A22, A11, SCMFSA_5:7
.=
goto (((card J) + 1) + (card I))
by SCMFSA_4:14
.=
goto (((card I) + (card J)) + 1)
;
A30:
now let f be
FinSeq-Location ;
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + (1 + 1))) . f = (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . fT:
ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))
by AMI_1:144;
thus (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + (1 + 1))) . f =
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1)) . f
.=
(Following (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 ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) . f
by AMI_1:14
.=
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . f
by A29, SCMFSA_2:95, T
;
verum end;
Y:
(ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2))) /. (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2))) = (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) . (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)))
by AMI_1:150;
T:
ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))
by AMI_1:144;
thus 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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) =
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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1))
.=
IC (Following (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 ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)))
by AMI_1:14
.=
((card I) + (card J)) + 1
by A29, SCMFSA_2:95, T
; ( DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (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)),(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 (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
then A31: CurInstr (ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2))),(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) =
(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . (((card I) + (card J)) + 1)
by AMI_1:54, Y
.=
((I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At 0 ,SCM+FSA )) . (((card I) + (card J)) + 1)
by A13, A21, A15, FUNCT_4:14
.=
(I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) . (((card I) + (card J)) + 1)
by A21, SCMFSA6B:7
.=
(ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I))) . (((card I) + (card J)) + 1)
by A27, FUNCT_4:14
.=
(Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)) . (((card J) + 1) + (card I))
by A27, A26, GRFUNC_1:8
.=
IncAddr (halt SCM+FSA ),(card I)
by A24, A25, SCMFSA_5:7
.=
halt SCM+FSA
by SCMFSA_4:8
;
now let a be
Int-Location ;
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + (1 + 1))) . a = (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . aT:
ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))
by AMI_1:144;
thus (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + (1 + 1))) . a =
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1)) . a
.=
(Following (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 ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))) . a
by AMI_1:14
.=
(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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) . a
by A29, SCMFSA_2:95, T
;
verum end;
then
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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = 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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2))
by A30, SCMFSA6A:38;
hence
DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2))
by A1, A7, A14, Th36; ( ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (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)),(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 (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
hereby ( ( for k being Element of NAT st k <= LifeSpan (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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
let k be
Element of
NAT ;
( k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 implies CurInstr (ProgramPart (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 ))),b1)),(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 ))),b1) <> halt SCM+FSA )assume A33:
k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2
;
CurInstr (ProgramPart (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 ))),b1)),(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 ))),b1) <> halt SCM+FSA per cases
( k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) or LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) < k )
;
suppose A34:
k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))
;
CurInstr (ProgramPart (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 ))),b1)),(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 ))),b1) <> halt SCM+FSA then
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) <> halt SCM+FSA
by A1, A7, Th35;
hence
CurInstr (ProgramPart (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)),
(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
by A1, A7, A13, A34, Th42;
verum end; suppose A35:
LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) < k
;
CurInstr (ProgramPart (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 ))),b1)),(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 ))),b1) <> halt SCM+FSA A36:
InsCode (goto (((card I) + (card J)) + 1)) = 6
by SCMFSA_2:47;
k < ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1
by A33;
then A37:
k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1
by NAT_1:13;
(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1
<= k
by A35, NAT_1:13;
then
(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1
= k
by A37, XXREAL_0:1;
hence
CurInstr (ProgramPart (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)),
(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
by A29, A36, SCMFSA_2:124;
verum end;
end;
hereby ( 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 (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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
let k be
Element of
NAT ;
( k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) implies 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) )assume A38:
k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))
;
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)then
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k)
by A1, A7, Th35, AMI_1:121;
hence
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)
by A1, A7, A13, A38, Th42;
verum
end;
thus
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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I
by A1, A7, A28, Th36; ( 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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
thus A39:
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 ))
by A31, AMI_1:146; LifeSpan (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2
for k being Element of NAT st CurInstr (ProgramPart (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)),(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 holds
(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 <= k
by A32;
hence
LifeSpan (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2
by A31, A39, AMI_1:def 46; verum