let P be Instruction-Sequence of SCM+FSA; :: thesis:
set J3 = (Goto 0) ';' (Stop SCM+FSA);
set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis:
let I be Program of ; :: thesis:
let s be State of SCM+FSA; :: thesis:
set s1 = Initialize s;
set P1 = P +* (while>0 (a,I));
A1: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:25;
set sI = Initialize s;
set PI = P +* I;
A2: I c= P +* I by FUNCT_4:25;
set life = LifeSpan ((P +* I),(Initialize s));
set sK1 = Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))));
set sK2 = Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))));
set I1 = I ';' (Goto 0);
set i = a >0_goto ((card (Stop SCM+FSA)) + 3);
reconsider n = IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) 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);
assume I is_closed_on s,P ; :: thesis:
then A4: n in dom I by SCMFSA7B:def 6;
then n < card I by AFINSQ_1:66;
then A5: n + 4 < (card I) + 6 by XREAL_1:8;
A6: (P +* I) /. (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by PBOOLE:143;
assume I is_halting_on s,P ; :: thesis:
then A7: P +* I halts_on Initialize s by SCMFSA7B:def 7;
CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = I . n by A4, A2, A6, GRFUNC_1:2;
then A8: I . n = halt SCM+FSA by A7, EXTPRO_1:def 15;
A9: (I ';' (Goto 0)) ';' (Stop SCM+FSA) = I ';' ((Goto 0) ';' (Stop SCM+FSA)) by SCMFSA6A:25;
then dom ((I ';' (Goto 0)) ';' (Stop SCM+FSA)) = (dom (Directed I)) \/ (dom (Reloc (((Goto 0) ';' (Stop SCM+FSA)),(card I)))) by FUNCT_4:def 1
.= (dom I) \/ (dom (Reloc (((Goto 0) ';' (Stop SCM+FSA)),(card I)))) by FUNCT_4:99 ;
then A10: n in dom ((I ';' (Goto 0)) ';' (Stop SCM+FSA)) by A4, 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 A11: n + 4 in dom (Shift (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) by VALUED_1:def 12;
then A12: (Shift (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) /. (n + 4) = (Shift (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) . (n + 4) by PARTFUN1:def 6
.= ((I ';' (Goto 0)) ';' (Stop SCM+FSA)) . n by A10, VALUED_1:def 12
.= (Directed I) . n by A4, A9, SCMFSA8A:14
.= goto (card I) by A4, A8, SCMFSA8A:16 ;
set f = ((card I) + 4) .--> (goto 0);
assume A13: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 4 ; :: thesis:
( dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} & n + 4 <> (card I) + 4 ) by A4, FUNCOP_1:13;
then A14: not n + 4 in dom (((card I) + 4) .--> (goto 0)) by TARSKI:def 1;
A15: 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:21
.= (card ((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA))) + 1 by SCMFSA8A:15
.= ((card (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3)))) + (card (Stop SCM+FSA))) + 1 by SCMFSA6A:21
.= (2 + 1) + 1 by Lm1, COMPOS_1:56
.= 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 A16: 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:66;
card (while>0 (a,I)) = (card I) + 6 by Th5;
then A17: n + 4 in dom (while>0 (a,I)) by A5, AFINSQ_1:66;
A18: 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 A19: n + 4 in dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by A14, A17, XBOOLE_0:def 3;
A20: 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:25
.= (Directed (((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1)))) +* (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) by A15 ;
then A21: 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 (Reloc (((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 (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4))) by FUNCT_4:99;
then A22: n + 4 in dom (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) by A19, A16, XBOOLE_0:def 3;
A23: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) by PBOOLE:143;
(P +* (while>0 (a,I))) . (n + 4) = ((if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) . (n + 4) by A17, A1, GRFUNC_1:2
.= ((Directed (((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1)))) +* (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4))) . (n + 4) by A14, A17, A18, A20, FUNCT_4:def 1
.= (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) . (n + 4) by A19, A21, A22, FUNCT_4:def 1
.= IncAddr ((goto (card I)),4) by A11, A12, COMPOS_1:def 19
.= goto ((card I) + 4) by SCMFSA_4:1 ;
hence CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto ((card I) + 4) by A13, A23; :: thesis: