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;
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 = (s +* (Start-At 0 ,SCM+FSA )) +* I by A4, FUNCT_4:79
.= (s +* I) +* (Start-At 0 ,SCM+FSA ) by Th14
.= 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 AMI_1:51;
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, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
hence A30: ProgramPart s halts_on s by AMI_1:146; :: 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 AMI_1:51;
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, AMI_1:def 46; :: 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, AMI_1:def 46;
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 AMI_1:122;
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, AMI_1:122
.= (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 AMI_1:51
.= (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;