set J3 = (Goto 0 ) ';' (Stop SCM+FSA );
set J = Stop SCM+FSA ;
let a be Int-Location ; for I being Program of SCM+FSA
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) & IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) holds
( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )
set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of SCM+FSA ; for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) & IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) holds
( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )
let s be State of SCM+FSA ; for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) & IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) holds
( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )
let k be Element of NAT ; ( I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) & IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) implies ( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) ) )
set s1 = s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ));
set sI = s +* (I +* (Start-At 0 ,SCM+FSA ));
set sK1 = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k);
set sK2 = Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k;
set l3 = IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k);
set I1 = I ';' (Goto 0 );
set i = a >0_goto ((card (Stop SCM+FSA )) + 3);
reconsider n = IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) as Element of NAT ;
set Mi = ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1));
set J2 = (I ';' (Goto 0 )) ';' (Stop SCM+FSA );
A1:
rng I c= the Instructions of SCM+FSA
by RELAT_1:def 19;
assume
I is_closed_on s
; ( not I is_halting_on s or not k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) or not IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 or not DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) or ( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) ) )
then A2:
n in dom I
by SCMFSA7B:def 7;
then
n < card I
by AFINSQ_1:70;
then A3:
n + 4 < (card I) + 6
by XREAL_1:10;
Y:
(ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) /. (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) = (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (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 COMPOS_1:38;
I c= I +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A4:
dom I c= dom (I +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
TX:
ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) = ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))
by AMI_1:123;
A5: CurInstr (ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) =
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) . n
by Y
.=
(s +* (I +* (Start-At 0 ,SCM+FSA ))) . n
by AMI_1:54
.=
(I +* (Start-At 0 ,SCM+FSA )) . n
by A2, A4, FUNCT_4:14
.=
I . n
by A2, SCMFSA6B:7
;
assume
I is_halting_on s
; ( not k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) or not IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 or not DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) or ( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) ) )
then A6:
ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA ))
by SCMFSA7B:def 8;
assume
k < LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))
; ( not IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 or not DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) or ( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) ) )
then A7:
I . n <> halt SCM+FSA
by A5, A6, TX, AMI_1:def 46;
A8:
(I ';' (Goto 0 )) ';' (Stop SCM+FSA ) = I ';' ((Goto 0 ) ';' (Stop SCM+FSA ))
by SCMFSA6A:67;
then dom ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) =
(dom (Directed I)) \/ (dom (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),(card I))))
by FUNCT_4:def 1
.=
(dom I) \/ (dom (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),(card I))))
by FUNCT_4:105
;
then A9:
n in dom ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))
by A2, XBOOLE_0:def 3;
then
n + 4 in { (il + 4) where il is Element of NAT : il in dom ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) }
;
then A10:
n + 4 in dom (Shift ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4)
by VALUED_1:def 12;
then A11: (Shift ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4) /. (n + 4) =
(Shift ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4) . (n + 4)
by PARTFUN1:def 8
.=
((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) . n
by A9, VALUED_1:def 12
.=
(Directed I) . n
by A2, A8, SCMFSA8A:28
.=
I . n
by A2, A7, SCMFSA8A:30
;
card (while>0 a,I) = (card I) + 6
by Th5;
then A12:
n + 4 in dom (while>0 a,I)
by A3, AFINSQ_1:70;
I . n in rng I
by A2, FUNCT_1:def 5;
then reconsider j = I . n as Instruction of SCM+FSA by A1;
while>0 a,I c= (while>0 a,I) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A13:
dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
A14: card (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) =
(card ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA ))) + (card (Goto ((card (I ';' (Goto 0 ))) + 1)))
by SCMFSA6A:61
.=
(card ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA ))) + 1
by SCMFSA8A:29
.=
((card (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) + (card (Stop SCM+FSA ))) + 1
by SCMFSA6A:61
.=
(2 + 1) + 1
by LL, SCMFSA7B:6
.=
3 + 1
;
then
n + 4 >= card (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1)))
by NAT_1:11;
then A15:
not n + 4 in dom (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1)))
by AFINSQ_1:70;
T:
ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)
by AMI_1:123;
A16: Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1) =
Following (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)
by AMI_1:14
.=
Exec j,(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)
by A5, T
;
set f = ((card I) + 4) .--> (goto 0 );
assume A17:
IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4
; ( not DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) or ( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) ) )
( dom (((card I) + 4) .--> (goto 0 )) = {((card I) + 4)} & n + 4 <> (card I) + 4 )
by A2, FUNCOP_1:19;
then A18:
not n + 4 in dom (((card I) + 4) .--> (goto 0 ))
by TARSKI:def 1;
A19:
dom (while>0 a,I) = (dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ))) \/ (dom (((card I) + 4) .--> (goto 0 )))
by FUNCT_4:def 1;
then A20:
n + 4 in dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ))
by A18, A12, XBOOLE_0:def 3;
A21: if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ) =
((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' (I ';' (Goto 0 ))) ';' (Stop SCM+FSA )
by SCMFSA8B:def 2
.=
(((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))
by SCMFSA6A:67
.=
(Directed (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1)))) +* (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4))
by A14
;
then A22:
dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (dom (Directed (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))))) \/ (dom (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4)))
by FUNCT_4:def 1;
then
dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (dom (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1)))) \/ (dom (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4)))
by FUNCT_4:105;
then A23:
n + 4 in dom (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4))
by A20, A15, XBOOLE_0:def 3;
Z:
(ProgramPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k))) /. (IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k))) = (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) . (IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)))
by COMPOS_1:38;
(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) . (n + 4) =
(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . (n + 4)
by AMI_1:54
.=
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . (n + 4)
by A12, A13, FUNCT_4:14
.=
((if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ))) . (n + 4)
by A12, SCMFSA6B:7
.=
((Directed (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1)))) +* (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4))) . (n + 4)
by A18, A12, A19, A21, FUNCT_4:def 1
.=
(ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4)) . (n + 4)
by A20, A22, A23, FUNCT_4:def 1
.=
(Reloc (ProgramPart ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))),4) . (n + 4)
by AMISTD_2:69
.=
(Reloc ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4) . (n + 4)
by RELAT_1:209
.=
IncAddr j,4
by A10, A11, SCMFSA_4:24
;
then A24:
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k))),(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = IncAddr j,4
by A17, Z;
assume A25:
DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)
; ( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )
T:
ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k))
by AMI_1:123;
Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1) =
Following (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k))
by AMI_1:14
.=
Exec (IncAddr j,4),(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k))
by A24, T
;
hence
( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )
by A17, A25, A16, SCMFSA6A:41; verum