set J3 = (Goto 0) ';' (Stop SCM+FSA);
set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis:
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let k be Element of NAT ; :: thesis:
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 ; :: thesis:
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, COMPOS_1:145 ;
assume I is_halting_on s ; :: thesis:
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))))) ; :: thesis:
then A7: I . n <> halt SCM+FSA by A5, A6, TX, EXTPRO_1:def 14;
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, COMPOS_1:150
.= 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 EXTPRO_1:4
.= 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 ; :: thesis:
( 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, COMPOS_1:145
.= ((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 COMPOS_1:116
.= (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)) ; :: thesis:
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 EXTPRO_1:4
.= 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; :: thesis: