set D = Int-Locations \/ FinSeq-Locations ;
let a be Int-Location ; :: thesis:
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 (insloc 0 )));
set sI = s +* (I +* (Start-At (insloc 0 )));
set sK1 = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k);
set sK2 = Computation (s +* (I +* (Start-At (insloc 0 )))),k;
set l3 = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k);
assume A1: I is_closed_on s ; :: thesis:
assume A2: I is_halting_on s ; :: thesis:
assume A3: k < LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis:
assume A4: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)) + 4 ; :: thesis:
assume A5: DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ; :: thesis:
set I1 = I ';' (Goto (insloc 0 ));
set J = Stop SCM+FSA ;
set f = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set i = a >0_goto (insloc ((card (Stop SCM+FSA )) + 3));
A6: dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} by FUNCOP_1:19;
reconsider n = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) as Element of NAT by ORDINAL1:def 13;
A8: insloc n in dom I by A1, SCMFSA7B:def 7;
then A9: n < card I by SCMFSA6A:15;
n + 4 <> (card I) + 4 by A8, SCMFSA6A:15;
then A10: not insloc (n + 4) in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by A6, TARSKI:def 1;
A11: n + 4 < (card I) + 6 by A9, XREAL_1:10;
card (while>0 a,I) = (card I) + 6 by Th5;
then A12: insloc (n + 4) in dom (while>0 a,I) by A11, SCMFSA6A:15;
A13: dom (while>0 a,I) = (dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) \/ (dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) by FUNCT_4:def 1;
then A14: insloc (n + 4) in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A10, A12, XBOOLE_0:def 3;
set Mi = ((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)));
set J2 = (I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA );
set J3 = (Goto (insloc 0 )) ';' (Stop SCM+FSA );
A15: card (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) = (card ((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA ))) + (card (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) by SCMFSA6A:61
.= (card ((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA ))) + 1 by SCMFSA8A:29
.= ((card (Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))))) + (card (Stop SCM+FSA ))) + 1 by SCMFSA6A:61
.= (2 + 1) + 1 by SCMFSA7B:6, SCMFSA8A:17
.= 3 + 1 ;
then n + 4 >= card (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) by NAT_1:11;
then A16: not insloc (n + 4) in dom (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) by SCMFSA6A:15;
A17: if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) = ((((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2
.= (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= (Directed (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))) +* (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4)) by A15 ;
then A18: dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom (Directed (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))))) \/ (dom (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4))) by FUNCT_4:def 1;
then dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))) \/ (dom (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4))) by FUNCT_4:105;
then A19: insloc (n + 4) in dom (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4)) by A14, A16, XBOOLE_0:def 3;
while>0 a,I c= (while>0 a,I) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A21: dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A22: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A23: CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),k) = (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . (insloc n) by AMI_1:def 17
.= (s +* (I +* (Start-At (insloc 0 )))) . (insloc n) by AMI_1:54
.= (I +* (Start-At (insloc 0 ))) . (insloc n) by A8, A22, FUNCT_4:14
.= I . (insloc n) by A8, SCMFSA6B:7 ;
s +* (I +* (Start-At (insloc 0 ))) is halting by A2, SCMFSA7B:def 8;
then A24: I . (insloc n) <> halt SCM+FSA by A3, A23, AMI_1:def 46;
A25: (I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ) = I ';' ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:67;
then dom ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )) = (dom (Directed I)) \/ (dom (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),(card I)))) by FUNCT_4:def 1
.= (dom I) \/ (dom (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),(card I)))) by FUNCT_4:105 ;
then A26: insloc n in dom ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )) by A8, XBOOLE_0:def 3;
then (insloc n) + 4 in { (il + 4) where il is Element of NAT : il in dom ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )) } ;
then A27: insloc (n + 4) in dom (Shift ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4) by VALUED_1:def 12;
then A28: pi (Shift ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4),(n + 4) = (Shift ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4) . ((insloc n) + 4) by AMI_1:def 47
.= ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )) . (insloc n) by A26, VALUED_1:def 12
.= (Directed I) . (insloc n) by A8, A25, SCMFSA8A:28
.= I . (insloc n) by A8, A24, SCMFSA8A:30 ;
A29: I . (insloc n) in rng I by A8, FUNCT_1:def 5;
rng I c= the Instructions of SCM+FSA by AMI_1:118;
then reconsider j = I . (insloc n) as Instruction of SCM+FSA by A29;
(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) . (insloc (n + 4)) = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc (n + 4)) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc (n + 4)) by A12, A21, FUNCT_4:14
.= ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) . (insloc (n + 4)) by A12, SCMFSA6B:7
.= ((Directed (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))) +* (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4))) . (insloc (n + 4)) by A10, A12, A13, A17, FUNCT_4:def 1
.= (ProgramPart (Relocated ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4)) . (insloc (n + 4)) by A14, A18, A19, FUNCT_4:def 1
.= (IncAddr [(Shift (ProgramPart ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ))),4)],4) . (insloc (n + 4)) by SCMFSA_5:2
.= (IncAddr (Shift ((I ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA )),4),4) . (insloc (n + 4)) by AMI_1:105
.= IncAddr j,4 by A27, A28, SCMFSA_4:24 ;
then A30: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) = IncAddr j,4 by A4, AMI_1:def 17;
A31: Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1) = Following (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) by AMI_1:14
.= Exec (IncAddr j,4),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + k)) by A30, AMI_1:def 18 ;
Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec j,(Computation (s +* (I +* (Start-At (insloc 0 )))),k) by A23, AMI_1:def 18 ;
hence ( IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1))) + 4 & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(k + 1)) ) by A4, A5, A31, SCMFSA6A:41; :: thesis: