set D = Data-Locations SCM+FSA;
set JAt = Initialized J;
let s be State of SCM+FSA; EXTPRO_1:def 10,SCM_HALT:def 2 ( not Initialized (I ';' J) c= s or for b1 being set holds
( not ProgramPart (Initialized (I ';' J)) c= b1 or b1 halts_on s ) )
assume A1:
Initialized (I ';' J) c= s
; for b1 being set holds
( not ProgramPart (Initialized (I ';' J)) c= b1 or b1 halts_on s )
then A2:
s = s +* (Initialized (I ';' J))
by FUNCT_4:79;
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; ( not ProgramPart (Initialized (I ';' J)) c= p or p halts_on s )
assume A3:
ProgramPart (Initialized (I ';' J)) c= p
; p halts_on s
ProgramPart (Initialized (I ';' J)) = I ';' J
by SCMFSA6A:33;
then A4:
p = p +* (I ';' J)
by A3, FUNCT_4:79;
A5:
ProgramPart (Initialized (I ';' J)) = I ';' J
by SCMFSA6A:33;
A6:
Initialized (I ';' J) = (I ';' J) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:15;
set s1 = s +* I;
set p1 = p +* I;
set s3 = (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J);
set p3 = (p +* I) +* J;
A7:
J c= (p +* I) +* J
by FUNCT_4:26;
set m1 = LifeSpan ((p +* I),(s +* I));
set s4 = Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1));
A8:
I c= p +* I
by FUNCT_4:26;
A9:
Reloc (J,(card I)) c= I ';' J
by FUNCT_4:26;
A10:
dom I misses dom (Initialize ((intloc 0) .--> 1))
by Th2;
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)));
A11:
dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Data-Locations SCM+FSA)
by RELAT_1:90;
reconsider m = ((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))) as Element of NAT ;
A12:
dom (Directed I) = dom I
by FUNCT_4:105;
dom (I ';' J) misses dom (Initialize ((intloc 0) .--> 1))
by Th2;
then A13:
I ';' J c= Initialized (I ';' J)
by A6, FUNCT_4:33;
then
I ';' J c= s
by A1, XBOOLE_1:1;
then
Reloc (J,(card I)) c= s
by A9, XBOOLE_1:1;
then A14:
( Initialized J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) & Reloc (J,(card I)) c= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) )
by AMI_1:81, FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= (I ';' J) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
then A15:
Initialize ((intloc 0) .--> 1) c= s
by A1, A6, XBOOLE_1:1;
then
s +* (Initialize ((intloc 0) .--> 1)) = s
by FUNCT_4:79;
then A16: s +* I =
s +* ((Initialize ((intloc 0) .--> 1)) +* I)
by FUNCT_4:15
.=
s +* (I +* (Initialize ((intloc 0) .--> 1)))
by A10, FUNCT_4:36
.=
s +* (Initialized I)
by FUNCT_4:15
;
A17:
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
I c= p +* I
by FUNCT_4:26;
then A18:
p +* I halts_on s +* I
by Th5, A17, A16;
A19:
now let x be
set ;
( x in dom (DataPart (Initialized J)) implies (DataPart (Initialized J)) . b1 = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . b1 )assume
x in dom (DataPart (Initialized J))
;
(DataPart (Initialized J)) . b1 = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . b1then A20:
x in (dom (Initialized J)) /\ (Data-Locations SCM+FSA)
by RELAT_1:90;
then A21:
x in dom (Initialized J)
by XBOOLE_0:def 4;
A22:
x in Data-Locations SCM+FSA
by A20, XBOOLE_0:def 4;
per cases
( x in dom J or x = intloc 0 or x = IC )
by A21, SCMFSA6A:44;
suppose A24:
x = intloc 0
;
(DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . b1 = (DataPart (Initialized J)) . b1then
x in Int-Locations
by SCMFSA_2:9;
then A25:
x in Data-Locations SCM+FSA
by XBOOLE_0:def 3, SCMFSA_2:127;
hence (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) . x =
(Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) . x
by FUNCT_1:72
.=
1
by A16, A24, Def3, A17, A8
.=
(Initialized J) . x
by A24, SCMFSA6A:46
.=
(DataPart (Initialized J)) . x
by A25, FUNCT_1:72
;
verum end; end;
take
m
; EXTPRO_1:def 7 ( IC (Comput (p,s,m)) in proj1 p & CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA )
IC (Comput (p,s,m)) in NAT
;
hence
IC (Comput (p,s,m)) in dom p
by PARTFUN1:def 4; CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA
A26:
Directed I c= I ';' J
by SCMFSA6A:55;
then A27:
Directed I c= p
by A3, A5, XBOOLE_1:1;
A28: (s +* I) +* (Directed I) =
s +* (I +* (Directed I))
by FUNCT_4:15
.=
s +* (Directed I)
by A12, FUNCT_4:20
.=
(s +* (Initialized (I ';' J))) +* (Directed I)
by A1, LATTICE2:8
.=
s +* ((Initialized (I ';' J)) +* (Directed I))
by FUNCT_4:15
.=
s +* (Initialized (I ';' J))
by A26, A13, LATTICE2:8, XBOOLE_1:1
.=
s
by A1, LATTICE2:8
;
A29:
Initialized J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)
by FUNCT_4:26;
then
dom (Initialized J) c= dom ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))
by GRFUNC_1:8;
then
dom (Initialized J) c= the carrier of SCM+FSA
by PARTFUN1:def 4;
then
dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Data-Locations SCM+FSA)
by A11, XBOOLE_1:26;
then
dom (DataPart (Initialized J)) c= (dom (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) /\ (Data-Locations SCM+FSA)
by PARTFUN1:def 4;
then
dom (DataPart (Initialized J)) c= dom (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))))
by RELAT_1:90;
then
( DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) = (DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) )
by A19, FUNCT_4:75, GRFUNC_1:8;
then A30:
DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))
by LATTICE2:8;
Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* I)))), Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((p +* I),(s +* I)))) equal_outside NAT
by A16, A18, Th24;
then
Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))), Comput (p,s,(LifeSpan ((p +* I),(s +* I)))) equal_outside NAT
by A2, A16, A4;
then A31:
DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* I))))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))
by COMPOS_1:138, A30;
A32:
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
I c= p +* I
by FUNCT_4:26;
then
p +* I halts_on s +* I
by A16, Th5, A32;
then A33:
DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))
by A15, A28, Th22, A31, FUNCT_4:26, A27;
A34:
ProgramPart (Initialized J) = J
by SCMFSA6A:33;
A35:
Comput (p,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))
by EXTPRO_1:5;
A36:
Reloc (J,(card I)) c= p
by A9, A3, A5, XBOOLE_1:1;
IC (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) = card I
by A15, A18, A28, Th21, FUNCT_4:26, A27;
then A37:
IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J))))))))
by A35, A33, A14, Th12, A7, A36;
(p +* I) +* J halts_on (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)
by A29, EXTPRO_1:def 10, A34, A7;
then CurInstr (p,(Comput (p,s,m))) =
IncAddr ((halt SCM+FSA),(card I))
by A37, EXTPRO_1:def 14
.=
halt SCM+FSA
by COMPOS_1:93
;
hence
CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA
; verum