let I, J be 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 )
let s be State of SCM+FSA ; ( I is_closed_on Initialized s & I is_halting_on Initialized s implies ( 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 ) )
assume A1:
I is_closed_on Initialized s
; ( not I is_halting_on Initialized s or ( 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 ) )
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 COMPOS_1:45;
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, RELAT_1:209;
set J2 = (Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ));
set s2 = s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )));
set s1 = s +* (Initialized I);
assume A7:
I is_halting_on Initialized s
; ( 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 )
dom (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) =
dom (Reloc (ProgramPart (Stop SCM+FSA )),((card J) + 1))
by AMISTD_2:69
.=
{ (m + ((card J) + 1)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA )) }
by AMISTD_2:70
;
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 +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1)) = 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))) + 1))
by A1, A7, Th43;
I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) c= Initialized (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by SCMFSA6A:26;
then A15:
dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) c= dom (Initialized (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))))
by GRFUNC_1:8;
I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))) c= Initialized (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by SCMFSA6A:26;
then A16:
dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) c= dom (Initialized (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop 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 AFINSQ_1:70;
x:
card (Stop SCM+FSA ) = 1
by COMPOS_1:46;
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 AFINSQ_1:70;
dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) = dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))
by RELAT_1:209;
then A22:
0 in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by A18, AFINSQ_1:70;
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
0 + (card I) in dom (Reloc (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))),(card I))
by AMISTD_2:70;
then A23:
0 + (card I) in dom (ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)))
by AMISTD_2:69;
x:
card (Stop SCM+FSA ) = 1
by COMPOS_1:46;
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 AFINSQ_1:70;
then A24:
(card J) + 1 in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))
by RELAT_1:209;
Y:
(ProgramPart (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))) /. (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))) = (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)) . (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)))
by COMPOS_1:38;
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, AMISTD_2:76
.=
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))) =
dom (Reloc (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))),(card I))
by AMISTD_2:69
.=
{ (m + (card I)) where m is Element of NAT : m in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) }
by AMISTD_2:70
;
then A27:
((card I) + (card J)) + 1 in dom (ProgramPart (Relocated ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))),(card I)))
by A24, A5;
A28:
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 ';' (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))
by A1, A7, A13, Th43;
then A29: CurInstr (ProgramPart (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))),(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)) =
(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)
by A1, A7, Th45, Y
.=
(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) . (card I)
by AMI_1:54
.=
(Initialized (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA ))))) . (card I)
by A13, A16, A20, FUNCT_4:14
.=
(I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA )))) . (card I)
by A20, SCMFSA6A:50
.=
(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, AMISTD_2:76
.=
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 +* (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 + 1))) . f = (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)) . fT:
ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) = ProgramPart (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))
by AMI_1:123;
thus (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 + 1))) . f =
(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) + 1)) . f
.=
(Following (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 )))),((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1))) . f
by AMI_1:14
.=
(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)) . f
by A29, T, SCMFSA_2:95
;
verum end;
Y:
(ProgramPart (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))) /. (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))) = (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)) . (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)))
by COMPOS_1:38;
T:
ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) = ProgramPart (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))
by AMI_1:123;
TZ:
ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) = ProgramPart (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))
by AMI_1:123;
thus 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)) =
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) + 1))
.=
IC (Following (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 )))),((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1)))
by AMI_1:14
.=
((card I) + (card J)) + 1
by A29, T, SCMFSA_2:95
; ( 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 )
then A31: 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 )))),((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 2)) =
(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) . (((card I) + (card J)) + 1)
by Y, TZ, AMI_1:54
.=
(Initialized (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop 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, SCMFSA6A:50
.=
(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, AMISTD_2:76
.=
halt SCM+FSA
by SCMFSA_4:8
;
now let a be
Int-Location ;
(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 + 1))) . a = (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)) . aT:
ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) = ProgramPart (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))
by AMI_1:123;
thus (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 + 1))) . a =
(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) + 1)) . a
.=
(Following (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 )))),((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1))) . a
by AMI_1:14
.=
(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)) . a
by A29, T, SCMFSA_2:95
;
verum end;
then
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))) + 1)) = 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))
by A30, SCMFSA6A:38;
hence
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))
by A1, A7, A14, Th45; ( ( 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 )
hereby ( ( 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 )
let k be
Element of
NAT ;
( k < (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 2 implies 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 )))),b1) <> halt SCM+FSA )assume A33:
k < (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 2
;
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 )))),b1) <> halt SCM+FSA TZ:
ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) = ProgramPart (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)
by AMI_1:123;
per cases
( k <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) or LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) < k )
;
suppose A34:
k <= LifeSpan (ProgramPart (s +* (Initialized I))),
(s +* (Initialized I))
;
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 )))),b1) <> halt SCM+FSA then
CurInstr (ProgramPart (s +* (Initialized (Directed I)))),
(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) <> halt SCM+FSA
by A1, A7, Th44;
hence
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
by A1, A7, A13, A34, Th43;
verum end; suppose A35:
LifeSpan (ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)) < k
;
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 )))),b1) <> halt SCM+FSA A36:
InsCode (goto (((card I) + (card J)) + 1)) = 6
by SCMFSA_2:47;
k < ((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 1
by A33;
then A37:
k <= (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1
by NAT_1:13;
(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1
<= k
by A35, NAT_1:13;
then
(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1
= k
by A37, XXREAL_0:1;
hence
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
by A29, A36, TZ, SCMFSA_2:124;
verum end;
end;
hereby ( 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 )
let k be
Element of
NAT ;
( k <= LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) implies 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) )assume A38:
k <= LifeSpan (ProgramPart (s +* (Initialized I))),
(s +* (Initialized I))
;
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)then
IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) = IC (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k)
by A1, A7, Th44, COMPOS_1:24;
hence
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)
by A1, A7, A13, A38, Th43;
verum
end;
thus
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
by A1, A7, A28, Th45; ( 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 )
thus A39:
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 )))
by A31, AMI_1:146; 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
for k being Element of NAT st 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 holds
(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 2 <= k
by A32;
hence
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
by A31, A39, AMI_1:def 46; verum