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 A3: n in dom I by SCMFSA7B:def 6;
then n < card I by AFINSQ_1:66;
then A4: n + 4 < (card I) + 6 by XREAL_1:8;
A5: (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 A6: 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 A3, A2, A5, GRFUNC_1:2;
then A7: I . n = halt SCM+FSA by A6, EXTPRO_1:def 15;
A8: (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 A9: 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 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 6
.= ((I ";" (Goto 0)) ";" (Stop SCM+FSA)) . n by A9, VALUED_1:def 12
.= (Directed I) . n by A3, A8, SCMFSA8A:14
.= goto (card I) by A3, A7, SCMFSA8A:16 ;
set f = ((card I) + 4) .--> (goto 0);
assume A12: 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 A3, FUNCOP_1:13;
then A13: not n + 4 in dom (((card I) + 4) .--> (goto 0)) by TARSKI:def 1;
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: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 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:66;
card (while>0 (a,I)) = (card I) + 6 by Th5;
then A16: n + 4 in dom (while>0 (a,I)) by A4, AFINSQ_1:66;
A17: 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 A18: n + 4 in dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) by A13, A16, XBOOLE_0:def 3;
A19: CutLastLoc (stop (((a >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (I ";" (Goto 0))) + 1)))) = ((a >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (I ";" (Goto 0))) + 1)) ;
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 A14, A19 ;
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 A18, A15, 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;
A24: Reloc (((I ";" (Goto 0)) ";" (Stop SCM+FSA)),4) = IncAddr ((Shift (((I ";" (Goto 0)) ";" (Stop SCM+FSA)),4)),4) by COMPOS_1:34;
(P +* (while>0 (a,I))) . (n + 4) = ((if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) . (n + 4) by A16, 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 A13, A16, A17, A20, FUNCT_4:def 1
.= (Reloc (((I ";" (Goto 0)) ";" (Stop SCM+FSA)),4)) . (n + 4) by A18, A21, A22, FUNCT_4:def 1
.= IncAddr ((goto (card I)),4) by A10, A11, A24, COMPOS_1:def 21
.= 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 A12, A23; :: thesis: