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