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 COMPOS_1:116
.=
{ (m + ((card J) + 1)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA)) }
by COMPOS_1:117
;
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 COMPOS_1:117;
then A23:
0 + (card I) in dom (ProgramPart (Relocated (((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))),(card I))))
by COMPOS_1:116;
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, COMPOS_1:122
.=
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 COMPOS_1:116
.=
{ (m + (card I)) where m is Element of NAT : m in dom (ProgramPart ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA)))) }
by COMPOS_1:117
;
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, COMPOS_1:122
.=
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 EXTPRO_1:4
.=
(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 EXTPRO_1:4
.=
((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, COMPOS_1:122
.=
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 EXTPRO_1:4
.=
(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+FSATZ:
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+FSAthen
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
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, 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, EXTPRO_1:30; 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, EXTPRO_1:def 14; verum