for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of SCM st DataPart p <> {} holds
IC in dom p
proof
let q be
NAT -defined the
InstructionsF of
SCM -valued finite non
halt-free Function;
for p being q -autonomic FinPartState of SCM st DataPart p <> {} holds
IC in dom plet p be
q -autonomic FinPartState of
SCM;
( DataPart p <> {} implies IC in dom p )
assume
DataPart p <> {}
;
IC in dom p
then A1:
dom (DataPart p) <> {}
;
assume A2:
not
IC in dom p
;
contradiction
then
dom p misses {(IC )}
by ZFMISC_1:50;
then A3:
(dom p) /\ {(IC )} = {}
by XBOOLE_0:def 7;
not
p is
q -autonomic
proof
set il = the
Element of
NAT \ (dom q);
set d2 = the
Element of
(Data-Locations ) \ (dom p);
set d1 = the
Element of
dom (DataPart p);
A4:
the
Element of
dom (DataPart p) in dom (DataPart p)
by A1;
DataPart p c= p
by MEMSTR_0:12;
then A5:
dom (DataPart p) c= dom p
by RELAT_1:11;
dom (DataPart p) c= the
carrier of
SCM
by RELAT_1:def 18;
then reconsider d1 = the
Element of
dom (DataPart p) as
Element of
SCM by A4;
not
Data-Locations c= dom p
;
then A6:
(Data-Locations ) \ (dom p) <> {}
by XBOOLE_1:37;
then
the
Element of
(Data-Locations ) \ (dom p) in Data-Locations
by XBOOLE_0:def 5;
then reconsider d2 = the
Element of
(Data-Locations ) \ (dom p) as
Data-Location by AMI_2:def 16, AMI_3:27;
A7:
not
d2 in dom p
by A6, XBOOLE_0:def 5;
then A8:
dom p misses {d2}
by ZFMISC_1:50;
not
NAT c= dom q
;
then A9:
NAT \ (dom q) <> {}
by XBOOLE_1:37;
then reconsider il = the
Element of
NAT \ (dom q) as
Element of
NAT by XBOOLE_0:def 5;
A10:
not
il in dom q
by A9, XBOOLE_0:def 5;
dom (DataPart p) c= Data-Locations
by RELAT_1:58;
then reconsider d1 =
d1 as
Data-Location by A4, AMI_2:def 16, AMI_3:27;
set p2 =
p +* ((d2 .--> 1) +* (Start-At (il,SCM)));
set p1 =
p +* ((d2 .--> 0) +* (Start-At (il,SCM)));
set q2 =
q +* (il .--> (d1 := d2));
set q1 =
q +* (il .--> (d1 := d2));
consider s1 being
State of
SCM such that A11:
p +* ((d2 .--> 0) +* (Start-At (il,SCM))) c= s1
by PBOOLE:141;
consider S1 being
Instruction-Sequence of
SCM such that A12:
q +* (il .--> (d1 := d2)) c= S1
by PBOOLE:145;
A13:
dom p misses {d2}
by A7, ZFMISC_1:50;
A14:
dom ((d2 .--> 1) +* (Start-At (il,SCM))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1;
consider s2 being
State of
SCM such that A15:
p +* ((d2 .--> 1) +* (Start-At (il,SCM))) c= s2
by PBOOLE:141;
consider S2 being
Instruction-Sequence of
SCM such that A16:
q +* (il .--> (d1 := d2)) c= S2
by PBOOLE:145;
A17:
dom p c= the
carrier of
SCM
by RELAT_1:def 18;
dom (Comput (S2,s2,1)) = the
carrier of
SCM
by PARTFUN1:def 2;
then A18:
dom ((Comput (S2,s2,1)) | (dom p)) = dom p
by A17, RELAT_1:62;
A19:
dom (Comput (S1,s1,1)) = the
carrier of
SCM
by PARTFUN1:def 2;
A20:
dom ((Comput (S1,s1,1)) | (dom p)) = dom p
by A17, A19, RELAT_1:62;
A21:
dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM))))
by FUNCT_4:def 1;
A22:
dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2)))
by FUNCT_4:def 1;
A24:
IC in dom (Start-At (il,SCM))
by TARSKI:def 1;
then A25:
IC in dom ((d2 .--> 1) +* (Start-At (il,SCM)))
by A14, XBOOLE_0:def 3;
then
IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM))))
by A21, XBOOLE_0:def 3;
then A26:
IC s2 =
(p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) . (IC )
by A15, GRFUNC_1:2
.=
((d2 .--> 1) +* (Start-At (il,SCM))) . (IC )
by A25, FUNCT_4:13
.=
(Start-At (il,SCM)) . (IC )
by A24, FUNCT_4:13
.=
il
by FUNCOP_1:72
;
d2 <> IC
by Th2;
then A27:
not
d2 in dom (Start-At (il,SCM))
by TARSKI:def 1;
d2 in dom (d2 .--> 1)
by TARSKI:def 1;
then A28:
d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM)))
by A14, XBOOLE_0:def 3;
then
d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM))))
by A21, XBOOLE_0:def 3;
then A29:
s2 . d2 =
(p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) . d2
by A15, GRFUNC_1:2
.=
((d2 .--> 1) +* (Start-At (il,SCM))) . d2
by A28, FUNCT_4:13
.=
(d2 .--> 1) . d2
by A27, FUNCT_4:11
.=
1
by FUNCOP_1:72
;
A31:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
then
il in dom (q +* (il .--> (d1 := d2)))
by A22, XBOOLE_0:def 3;
then A32:
S2 . il =
(q +* (il .--> (d1 := d2))) . il
by A16, GRFUNC_1:2
.=
(il .--> (d1 := d2)) . il
by A31, FUNCT_4:13
.=
d1 := d2
by FUNCOP_1:72
;
A33:
S2 /. (IC s2) = S2 . (IC s2)
by PBOOLE:143;
A34:
(Comput (S2,s2,(0 + 1))) . d1 =
(Following (S2,(Comput (S2,s2,0)))) . d1
by EXTPRO_1:3
.=
(Following (S2,s2)) . d1
.=
1
by A26, A32, A29, A33, AMI_3:2
;
dom p misses {(IC )}
by A2, ZFMISC_1:50;
then A35:
(dom p) /\ {(IC )} = {}
by XBOOLE_0:def 7;
take P =
S1;
EXTPRO_1:def 10 ex b1 being set st
( q c= P & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being set holds (Comput (P,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 p) ) )
take Q =
S2;
( q c= P & q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
dom ((d2 .--> 0) +* (Start-At (il,SCM))) =
(dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1
.=
(dom (d2 .--> 0)) \/ {(IC )}
.=
{d2} \/ {(IC )}
;
then (dom p) /\ (dom ((d2 .--> 0) +* (Start-At (il,SCM)))) =
((dom p) /\ {d2}) \/ {}
by A35, XBOOLE_1:23
.=
{}
by A8, XBOOLE_0:def 7
;
then
dom p misses dom ((d2 .--> 0) +* (Start-At (il,SCM)))
by XBOOLE_0:def 7;
then
p c= p +* ((d2 .--> 0) +* (Start-At (il,SCM)))
by FUNCT_4:32;
then A36:
p c= s1
by A11, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2))
by A10, ZFMISC_1:50;
then
q c= q +* (il .--> (d1 := d2))
by FUNCT_4:32;
hence
q c= P
by A12, XBOOLE_1:1;
( q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
A37:
dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM))))
by FUNCT_4:def 1;
dom ((d2 .--> 1) +* (Start-At (il,SCM))) =
(dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1
.=
(dom (d2 .--> 1)) \/ {(IC )}
.=
{d2} \/ {(IC )}
;
then (dom p) /\ (dom ((d2 .--> 1) +* (Start-At (il,SCM)))) =
((dom p) /\ {d2}) \/ {}
by A3, XBOOLE_1:23
.=
{}
by A13, XBOOLE_0:def 7
;
then
dom p misses dom ((d2 .--> 1) +* (Start-At (il,SCM)))
by XBOOLE_0:def 7;
then
p c= p +* ((d2 .--> 1) +* (Start-At (il,SCM)))
by FUNCT_4:32;
then A38:
p c= s2
by A15, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2))
by A10, ZFMISC_1:50;
then
q c= q +* (il .--> (d1 := d2))
by FUNCT_4:32;
hence
q c= Q
by A16, XBOOLE_1:1;
ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) )
take
s1
;
ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being set holds (Comput (P,s1,b2)) | (proj1 p) = (Comput (Q,b1,b2)) | (proj1 p) )
take
s2
;
( p c= s1 & p c= s2 & not for b1 being set holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus
p c= s1
by A36;
( p c= s2 & not for b1 being set holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus
p c= s2
by A38;
not for b1 being set holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p)
take
1
;
not (Comput (P,s1,1)) | (proj1 p) = (Comput (Q,s2,1)) | (proj1 p)
A39:
dom ((d2 .--> 0) +* (Start-At (il,SCM))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1;
A41:
IC in dom (Start-At (il,SCM))
by TARSKI:def 1;
then A42:
IC in dom ((d2 .--> 0) +* (Start-At (il,SCM)))
by A39, XBOOLE_0:def 3;
then
IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM))))
by A37, XBOOLE_0:def 3;
then A43:
IC s1 =
(p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) . (IC )
by A11, GRFUNC_1:2
.=
((d2 .--> 0) +* (Start-At (il,SCM))) . (IC )
by A42, FUNCT_4:13
.=
(Start-At (il,SCM)) . (IC )
by A41, FUNCT_4:13
.=
il
by FUNCOP_1:72
;
d2 <> IC
by Th2;
then A44:
not
d2 in dom (Start-At (il,SCM))
by TARSKI:def 1;
d2 in dom (d2 .--> 0)
by TARSKI:def 1;
then A45:
d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM)))
by A39, XBOOLE_0:def 3;
then
d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM))))
by A37, XBOOLE_0:def 3;
then A46:
s1 . d2 =
(p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) . d2
by A11, GRFUNC_1:2
.=
((d2 .--> 0) +* (Start-At (il,SCM))) . d2
by A45, FUNCT_4:13
.=
(d2 .--> 0) . d2
by A44, FUNCT_4:11
.=
0
by FUNCOP_1:72
;
A47:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2)))
by FUNCT_4:def 1;
then
il in dom (q +* (il .--> (d1 := d2)))
by A47, XBOOLE_0:def 3;
then A48:
S1 . il =
(q +* (il .--> (d1 := d2))) . il
by A12, GRFUNC_1:2
.=
(il .--> (d1 := d2)) . il
by A47, FUNCT_4:13
.=
d1 := d2
by FUNCOP_1:72
;
A49:
S1 /. (IC s1) = S1 . (IC s1)
by PBOOLE:143;
(Comput (S1,s1,(0 + 1))) . d1 =
(Following (S1,(Comput (S1,s1,0)))) . d1
by EXTPRO_1:3
.=
0
by A43, A48, A46, A49, AMI_3:2
;
then
((Comput (P,s1,1)) | (dom p)) . d1 = 0
by A4, A5, A20, FUNCT_1:47;
hence
(Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p)
by A18, A34, A4, A5, FUNCT_1:47;
verum
end;
hence
contradiction
;
verum
end;
hence
SCM is IC-recognized
by AMISTD_5:3; verum