let P be Instruction-Sequence of SCM+FSA; :: thesis:
set J = Stop SCM+FSA;
let a be Int-Location; :: thesis:
set D = Int-Locations \/ FinSeq-Locations;
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis:
let s be State of SCM+FSA; :: thesis:
let k be 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 3;
reconsider n = IC (Comput ((P +* I),(Initialize s),k)) as Element of NAT ;
set Mi = (a >0_goto 3) ";" (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;
A3: I c= P +* I by FUNCT_4:25;
IC (Initialize s) = 0 by MEMSTR_0:def 11;
then IC (Initialize s) in dom I by AFINSQ_1:65;
then A4: n in dom I by AMISTD_1:21, A3;
then n < card I by AFINSQ_1:66;
then A5: n + 3 < (card I) + 5 by XREAL_1:8;
A6: (P +* I) /. (IC (Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by PBOOLE:143;
A7: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = I . n by A4, A1, GRFUNC_1:2, A6;
assume I is_halting_on s,P ; :: thesis:
then A8: P +* I halts_on Initialize s by SCMFSA7B:def 7;
assume k < LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
then I . n <> halt SCM+FSA by A7, A8, EXTPRO_1:def 15;
then A9: n <> LastLoc I by COMPOS_1:def 14;
n <= LastLoc I by A4, VALUED_1:32;
then A10: n < LastLoc I by A9, XXREAL_0:1;
then A11: n in dom (CutLastLoc I) by COMPOS_2:26;
dom I c= dom (I ';' (goto 0)) by COMPOS_1:21;
then A12: n in dom (I ';' (goto 0)) by A4;
dom (I ';' (goto 0)) = (dom (CutLastLoc I)) \/ (dom (Reloc ((Macro (goto 0)),((card I) -' 1)))) by FUNCT_4:def 1;
then A13: dom (CutLastLoc I) c= dom (I ';' (goto 0)) by XBOOLE_1:7;
A14: dom (CutLastLoc I) misses dom (Reloc ((Macro (goto 0)),((card I) -' 1))) by COMPOS_1:18;
A15: n in dom (I ';' (goto 0)) by A11, A13;
dom I c= dom (I ';' (goto 0)) by COMPOS_1:21;
then LastLoc I <= LastLoc (I ';' (goto 0)) by VALUED_1:68;
then n < LastLoc (I ';' (goto 0)) by A10, XXREAL_0:2;
then A16: (I ';' (goto 0)) . n <> halt SCM+FSA by A15, COMPOS_1:def 15;
dom (I ';' (goto 0)) c= dom ((I ';' (goto 0)) ";" (Stop SCM+FSA)) by SCMFSA6A:17;
then A17: n in dom ((I ';' (goto 0)) ";" (Stop SCM+FSA)) by A12;
then n + 3 in { (il + 3) where il is Nat : il in dom ((I ';' (goto 0)) ";" (Stop SCM+FSA)) } ;
then A18: n + 3 in dom (Shift (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3)) by VALUED_1:def 12;
then A19: (Shift (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3)) /. (n + 3) = (Shift (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3)) . (n + 3) by PARTFUN1:def 6
.= ((I ';' (goto 0)) ";" (Stop SCM+FSA)) . n by A17, VALUED_1:def 12
.= (I ';' (goto 0)) . n by A16, A15, SCMFSA6A:15
.= (CutLastLoc I) . n by A11, FUNCT_4:16, A14
.= I . n by A10, COMPOS_2:27 ;
card (while>0 (a,I)) = (card I) + 5 by SCMFSA_X:4;
then A20: n + 3 in dom (while>0 (a,I)) by A5, AFINSQ_1:66;
I . n in rng I by A4, FUNCT_1:def 3;
then reconsider j = I . n as Instruction of SCM+FSA by A2;
A21: card ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) = (card (Macro (a >0_goto 3))) + (card (Goto ((card (I ';' (goto 0))) + 1))) by SCMFSA6A:21
.= (card (Macro (a >0_goto 3))) + 1 by SCMFSA8A:15
.= 2 + 1 by COMPOS_1:56
.= 3 ;
then n + 3 >= card ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) by NAT_1:11;
then A22: not n + 3 in dom ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) by AFINSQ_1:66;
A23: 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 A7 ;
assume A24: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 ; :: thesis:
n + 3 < (LastLoc I) + 3 by A10, XREAL_1:6;
then A25: n + 3 <> ((card I) - 1) + 3 by AFINSQ_1:91;
dom (while>0 (a,I)) = dom (if>0 (a,(I ';' (goto 0)))) by FUNCT_7:30;
then A26: n + 3 in dom (if>0 (a,(I ';' (goto 0)))) by A20;
A27: if>0 (a,(I ';' (goto 0))) = ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA)) by SCMFSA6A:25;
then dom (if>0 (a,(I ';' (goto 0)))) = (dom ((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1)))) \/ (dom (Reloc (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3))) by SCMFSA6A:39, A21;
then A28: n + 3 in dom (Reloc (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3)) by A26, A22, XBOOLE_0:def 3;
A29: (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;
A30: Reloc (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3) = IncAddr ((Shift (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3)),3) by COMPOS_1:34;
(P +* (while>0 (a,I))) . (n + 3) = (while>0 (a,I)) . (n + 3) by A20, FUNCT_4:13
.= (((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))) . (n + 3) by A27, FUNCT_7:32, A25
.= (Reloc (((I ';' (goto 0)) ";" (Stop SCM+FSA)),3)) . (n + 3) by A28, SCMFSA6A:40, A21
.= IncAddr (j,3) by A18, A19, A30, COMPOS_1:def 21 ;
then A31: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k)))) = IncAddr (j,3) by A24, A29;
assume A32: 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,3)),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k)))) by A31 ;
hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) by A24, A32, A23, SCMFSA6A:8; :: thesis: