set J3 = (Goto 0 ) ';' (Stop SCM+FSA );
set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
let s be State of SCM+FSA ; :: thesis:
set s1 = s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ));
set sI = s +* (I +* (Start-At 0 ,SCM+FSA ));
set life = LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(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 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))));
set sK2 = Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))));
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 ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) 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 );
while>0 a,I c= (while>0 a,I) +* (Start-At 0 ,SCM+FSA ) by SCMFSA8A:9;
then A1: dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
I c= I +* (Start-At 0 ,SCM+FSA ) by SCMFSA8A:9;
then A2: dom I c= dom (I +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
assume I is_closed_on s ; :: thesis:
then A3: n in dom I by SCMFSA7B:def 7;
then n < card I by AFINSQ_1:70;
then A4: 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 ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) /. (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) = (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) . (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) by COMPOS_1:38;
TX: ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) by AMI_1:123;
assume I is_halting_on s ; :: thesis:
then A5: ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
CurInstr (ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) = (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))) . n by Y
.= (s +* (I +* (Start-At 0 ,SCM+FSA ))) . n by AMI_1:54
.= (I +* (Start-At 0 ,SCM+FSA )) . n by A3, A2, FUNCT_4:14
.= I . n by A3, SCMFSA6B:7 ;
then A6: I . n = halt SCM+FSA by A5, TX, AMI_1:def 46;
A7: (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 A8: n in dom ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) by A3, 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 A9: n + 4 in dom (Shift ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4) by VALUED_1:def 12;
then A10: (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 A8, VALUED_1:def 12
.= (Directed I) . n by A3, A7, SCMFSA8A:28
.= goto (card I) by A3, A6, SCMFSA8A:30 ;
set f = ((card I) + 4) .--> (goto 0 );
assume A11: IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) + 4 ; :: thesis:
( dom (((card I) + 4) .--> (goto 0 )) = {((card I) + 4)} & n + 4 <> (card I) + 4 ) by A3, FUNCOP_1:19;
then A12: not n + 4 in dom (((card I) + 4) .--> (goto 0 )) by TARSKI:def 1;
A13: 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 A14: 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;
card (while>0 a,I) = (card I) + 6 by Th5;
then A15: n + 4 in dom (while>0 a,I) by A4, AFINSQ_1:70;
A16: 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 A17: n + 4 in dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) by A12, A15, XBOOLE_0:def 3;
A18: 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 A13 ;
then A19: 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 A20: n + 4 in dom (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4)) by A17, A14, 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 + (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 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (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 + (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 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))))))) 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 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) . (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 A15, A1, FUNCT_4:14
.= ((if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ))) . (n + 4) by A15, 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 A12, A15, A16, A18, FUNCT_4:def 1
.= (ProgramPart (Relocated ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )),4)) . (n + 4) by A17, A19, A20, 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 (goto (card I)),4 by A9, A10, SCMFSA_4:24
.= goto ((card I) + 4) by SCMFSA_4:14 ;
hence 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 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (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 + (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))) = goto ((card I) + 4) by A11, Z; :: thesis: