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:
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of ; :: thesis:
let s be State of SCM+FSA; :: thesis:
let k be Element of NAT ; :: thesis:
set s1 = Initialize s;
set P1 = P +* (while=0 (a,I));
set sI = Initialize s;
set PI = P +* I;
A1: I c= P +* I by FUNCT_4:25;
set sK1 = Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k));
set sK2 = Comput ((P +* I),(Initialize s),k);
set l3 = IC (Comput ((P +* I),(Initialize s),k));
set I1 = I ";" (Goto 0);
set i = a =0_goto ((card (Stop SCM+FSA)) + 3);
reconsider n = IC (Comput ((P +* I),(Initialize s),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);
A2: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
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),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by PBOOLE:143;
A6: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . n by A5
.= I . n by A3, A1, GRFUNC_1:2 ;
assume I is_halting_on s,P ; :: thesis:
then A7: P +* I halts_on Initialize s by SCMFSA7B:def 7;
assume k < LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
then A8: I . n <> halt SCM+FSA by A6, 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 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 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 A3, A9, SCMFSA8A:14
.= I . n by A3, A8, SCMFSA8A:16 ;
card (while=0 (a,I)) = (card I) + 6 by Th4;
then A13: n + 4 in dom (while=0 (a,I)) by A4, AFINSQ_1:66;
I . n in rng I by A3, FUNCT_1:def 3;
then reconsider j = I . n as Instruction of SCM+FSA by A2;
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;
A16: Comput ((P +* I),(Initialize s),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),k))) by EXTPRO_1:3
.= Exec (j,(Comput ((P +* I),(Initialize s),k))) by A6 ;
set f = ((card I) + 4) .--> (goto 0);
assume A17: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 ; :: thesis:
( dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} & n + 4 <> (card I) + 4 ) by A3, FUNCOP_1:13;
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, A13, XBOOLE_0:def 3;
A21: 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)) ;
A22: 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 1
.= (((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, A21 ;
then A23: 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 A24: n + 4 in dom (Reloc (((I ";" (Goto 0)) ";" (Stop SCM+FSA)),4)) by A20, A15, XBOOLE_0:def 3;
A25: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k)))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k)))) by PBOOLE:143;
A26: 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) = (while=0 (a,I)) . (n + 4) by A13, FUNCT_4:13
.= ((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 A18, A13, A19, A22, FUNCT_4:def 1
.= (Reloc (((I ";" (Goto 0)) ";" (Stop SCM+FSA)),4)) . (n + 4) by A20, A23, A24, FUNCT_4:def 1
.= IncAddr (j,4) by A11, A12, A26, COMPOS_1:def 21 ;
then A27: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k)))) = IncAddr (j,4) by A17, A25;
assume A28: DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) ; :: thesis:
Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k)))) by EXTPRO_1:3
.= Exec ((IncAddr (j,4)),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k)))) by A27 ;
hence ( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 4 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) by A17, A28, A16, SCMFSA6A:8; :: thesis: