set D = Int-Locations \/ FinSeq-Locations;
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA
for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
set SA0 = Start-At (0,SCM+FSA);
let J be parahalting Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
let s be State of SCM+FSA; :: thesis: ( Initialized (I ';' J) c= s implies ( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) ) )
set s1 = s +* I;
set s3 = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J);
set m1 = LifeSpan ((ProgramPart (s +* I)),(s +* I));
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)));
A1: dom (Directed I) = dom I by FUNCT_4:105;
A2: ( Directed I c= I ';' J & I ';' J c= Initialized (I ';' J) ) by SCMFSA6A:26, SCMFSA6A:55;
assume A3: Initialized (I ';' J) c= s ; :: thesis: ( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
then ( Start-At (0,SCM+FSA) c= (I ';' J) +* (Start-At (0,SCM+FSA)) & (I ';' J) +* (Start-At (0,SCM+FSA)) c= s ) by Th8, FUNCT_4:26;
then A4: Start-At (0,SCM+FSA) c= s by XBOOLE_1:1;
A5: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A1, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A3, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A2, LATTICE2:8, XBOOLE_1:1
.= s by A3, LATTICE2:8 ;
then A6: Directed I c= s by FUNCT_4:26;
(I ';' J) +* (Start-At (0,SCM+FSA)) c= s by A3, Th8;
then A7: s = s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
A8: Initialized I c= s +* I by A3, SCMFSA6A:52;
then A9: I +* (Start-At (0,SCM+FSA)) c= s +* I by Th8;
then A10: ProgramPart (s +* I) halts_on s +* I by Th18;
hence A11: IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I by A4, A5, Th37, FUNCT_4:26; :: thesis: ( DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
A12: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
A13: now
let x be set ; :: thesis: ( x in dom (DataPart (Initialized J)) implies (DataPart (Initialized J)) . b1 = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b1 )
assume x in dom (DataPart (Initialized J)) ; :: thesis: (DataPart (Initialized J)) . b1 = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b1
then A14: x in (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then A15: x in dom (Initialized J) by XBOOLE_0:def 4;
A16: x in Int-Locations \/ FinSeq-Locations by A14, XBOOLE_0:def 4;
per cases ( x in dom J or x = intloc 0 or x = IC SCM+FSA ) by A15, SCMFSA6A:44;
suppose A17: x in dom J ; :: thesis: (DataPart (Initialized J)) . b1 = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b1
dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A17;
(DataPart (Initialized J)) . l = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . l by A16, SCMFSA6A:37;
hence (DataPart (Initialized J)) . x = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . x ; :: thesis: verum
end;
suppose A18: x = intloc 0 ; :: thesis: (DataPart (Initialized J)) . b1 = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b1
thus (DataPart (Initialized J)) . x = (Initialized J) . x by A16, FUNCT_1:72, SCMFSA_2:127
.= 1 by A18, SCMFSA6A:46
.= (Initialized I) . x by A18, SCMFSA6A:46
.= (s +* I) . x by A8, A12, A18, GRFUNC_1:8
.= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) . x by A9, A18, Def4
.= (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . x by A16, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum
end;
suppose x = IC SCM+FSA ; :: thesis: (DataPart (Initialized J)) . b1 = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b1
hence (DataPart (Initialized J)) . x = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . x by A14, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
set s4 = Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1));
reconsider m = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))) as Element of NAT ;
A19: ProgramPart (Relocated (J,(card I))) c= I ';' J by FUNCT_4:26;
A20: Initialized J c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
Initialized J c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by GRFUNC_1:8;
then A21: dom (Initialized J) c= the carrier of SCM+FSA by PARTFUN1:def 4;
A22: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by Th19, FUNCT_4:26;
dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations) by A21, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) /\ (Int-Locations \/ FinSeq-Locations) by PARTFUN1:def 4;
then dom (DataPart (Initialized J)) c= dom (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) by RELAT_1:90, SCMFSA_2:127;
then ( DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) ) by A13, FUNCT_4:75, GRFUNC_1:8;
then A23: DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by LATTICE2:8;
s +* I = (Initialize s) +* I by A4, FUNCT_4:79
.= Initialize (s +* I) by COMPOS_1:83
.= s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:15 ;
then DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A7, A10, A23, Th40, SCMFSA6A:39;
hence A24: DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A4, A6, A10, Th38; :: thesis: ( ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then I ';' J c= s by A3, XBOOLE_1:1;
then ProgramPart (Relocated (J,(card I))) c= s by A19, XBOOLE_1:1;
then A25: ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) by AMI_1:81;
hence ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) ; :: thesis: ( (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
A26: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A27: intloc 0 in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = (DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))) . (intloc 0) by A24, FUNCT_1:72, SCMFSA_2:127
.= ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) . (intloc 0) by A27, FUNCT_1:72, SCMFSA_2:127
.= (Initialized J) . (intloc 0) by A26, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: ( ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
u: Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))) by EXTPRO_1:5;
TX: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) by AMI_1:123;
TY: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,m)) by AMI_1:123;
A28: J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by Th8, FUNCT_4:26;
then IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))))),(Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))))) by A11, A24, A25, Th27;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))) by u, T, TX, TY;
then A29: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A22, EXTPRO_1:def 14
.= halt SCM+FSA by SCMFSA_4:8 ;
hence A30: ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: ( LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
A31: now
let k be Element of NAT ; :: thesis: ( ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k < m implies not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)))) = halt SCM+FSA )
assume ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k < m ; :: thesis: not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)))) = halt SCM+FSA
then A32: k < LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))) by XREAL_1:8;
assume A33: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)))) = halt SCM+FSA ; :: thesis: contradiction
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
u: Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),k) by EXTPRO_1:5;
TX: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k)) by AMI_1:123;
TU: ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),k)) by AMI_1:123;
IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k)))),(card I)) = CurInstr ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),k))) by A11, A24, A28, A25, Th27, TU, TX
.= halt SCM+FSA by A33, u, T ;
then InsCode (CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k)))) = 0 by SCMFSA_2:124, SCMFSA_4:22;
then CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k))) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A22, A32, EXTPRO_1:def 14; :: thesis: verum
end;
now
let k be Element of NAT ; :: thesis: ( k < m implies CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b1))) <> halt SCM+FSA )
assume A34: k < m ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b1))) <> halt SCM+FSA
per cases ( k <= LifeSpan ((ProgramPart (s +* I)),(s +* I)) or LifeSpan ((ProgramPart (s +* I)),(s +* I)) < k ) ;
suppose LifeSpan ((ProgramPart (s +* I)),(s +* I)) < k ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b1))) <> halt SCM+FSA
then (LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A35: ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + kk = k by NAT_1:10;
kk in NAT by ORDINAL1:def 13;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCM+FSA by A31, A34, A35; :: thesis: verum
end;
end;
end;
then for k being Element of NAT st CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA holds
m <= k ;
then A36: LifeSpan ((ProgramPart s),s) = m by A29, A30, EXTPRO_1:def 14;
s +* I = s +* (Initialized I) by A3, SCMFSA6A:51;
then Initialized I c= s +* I by FUNCT_4:26;
then ProgramPart (s +* I) halts_on s +* I by Th19;
then Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))) = Result ((ProgramPart (s +* I)),(s +* I)) by EXTPRO_1:23;
hence LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) by A36; :: thesis: ( J is keeping_0 implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 )
A37: J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by Th8, FUNCT_4:26;
hereby :: thesis: verum
A38: DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) = DataPart (Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) by A11, A24, A28, A25, Th27;
assume A39: J is keeping_0 ; :: thesis: (Result ((ProgramPart s),s)) . (intloc 0) = 1
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
thus (Result ((ProgramPart s),s)) . (intloc 0) = (Comput ((ProgramPart s),s,m)) . (intloc 0) by A30, A36, EXTPRO_1:23
.= (Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by EXTPRO_1:5
.= (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by A38, T, SCMFSA6A:38
.= ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) . (intloc 0) by A37, A39, Def4
.= (Initialized J) . (intloc 0) by A26, A20, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis: verum
end;