let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for I being Program of
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
set J3 = (Goto 0) ';' (Stop SCM+FSA);
set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis: for I being Program of
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of ; :: thesis: for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
let s be State of SCM+FSA; :: thesis: for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
let k be Element of NAT ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) implies ( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) ) )
set s1 = Initialize s;
set P1 = P +* (while>0 (a,I));
set sI = Initialize s;
set PI = P +* I;
A2: 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);
A3: rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
assume I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or not k < LifeSpan ((P +* I),(Initialize s)) or not IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 or not DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) or ( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) ) )
then A4: n in dom I by SCMFSA7B:def 6;
then n < card I by AFINSQ_1:66;
then A5: n + 4 < (card I) + 6 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))) = (P +* I) . n by A6
.= I . n by A4, A2, GRFUNC_1:2 ;
assume I is_halting_on s,P ; :: thesis: ( not k < LifeSpan ((P +* I),(Initialize s)) or not IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 or not DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) or ( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) ) )
then A8: P +* I halts_on Initialize s by SCMFSA7B:def 7;
assume k < LifeSpan ((P +* I),(Initialize s)) ; :: thesis: ( not IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 or not DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) or ( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) ) )
then A9: I . n <> halt SCM+FSA by A7, A8, EXTPRO_1:def 15;
A10: (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 A11: n in dom ((I ';' (Goto 0)) ';' (Stop SCM+FSA)) by A4, 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 A12: n + 4 in dom (Shift (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) by VALUED_1:def 12;
then A13: (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 A11, VALUED_1:def 12
.= (Directed I) . n by A4, A10, SCMFSA8A:14
.= I . n by A4, A9, SCMFSA8A:16 ;
card (while>0 (a,I)) = (card I) + 6 by Th5;
then A14: n + 4 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 A3;
A15: 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 A16: 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;
A17: 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 ;
set f = ((card I) + 4) .--> (goto 0);
assume A18: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 ; :: thesis: ( not DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) or ( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) ) )
( dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} & n + 4 <> (card I) + 4 ) by A4, FUNCOP_1:13;
then A19: not n + 4 in dom (((card I) + 4) .--> (goto 0)) by TARSKI:def 1;
A20: 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 A21: n + 4 in dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by A19, A14, XBOOLE_0:def 3;
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 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 A15 ;
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 A21, A16, 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;
(P +* (while>0 (a,I))) . (n + 4) = (while>0 (a,I)) . (n + 4) by A14, 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 A19, A14, A20, A22, FUNCT_4:def 1
.= (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),4)) . (n + 4) by A21, A23, A24, FUNCT_4:def 1
.= IncAddr (j,4) by A12, A13, COMPOS_1:def 19 ;
then A26: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k)))) = IncAddr (j,4) by A18, A25;
assume A27: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) ; :: thesis: ( 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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
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 A26 ;
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),(s +* (Start-At (0,SCM+FSA))),(k + 1))) ) by A18, A27, A17, SCMFSA6A:8; :: thesis: verum