let q be NAT -defined the Instructions of SCMPDS -valued finite non halt-free Function; :: according to AMISTD_5:def 3 :: thesis: for b1 being set holds
( b1 is empty or IC in proj1 b1 )
let p be q -autonomic FinPartState of SCMPDS; :: thesis: ( p is empty or IC in proj1 p )
assume A1: not p is empty ; :: thesis: IC in proj1 p
assume A2: not IC in dom p ; :: thesis: contradiction
not IC in dom p by A2;
then A3: dom p misses {(IC )} by ZFMISC_1:50;
dom p c= {(IC )} \/ (dom (DataPart p)) by MEMSTR_0:32;
then A4: dom p c= dom (DataPart p) by A3, XBOOLE_1:73;
A5: dom (DataPart p) <> {} by A1, A4, XBOOLE_1:3;
DataPart p c= p by MEMSTR_0:12;
then A6: dom (DataPart p) c= dom p by RELAT_1:11;
not p is q -autonomic
proof
set il = the Element of NAT \ (dom q);
set d1 = the Element of dom (DataPart p);
A7: the Element of dom (DataPart p) in dom (DataPart p) by A5;
dom (DataPart p) c= the carrier of SCMPDS by RELAT_1:def 18;
then reconsider d1 = the Element of dom (DataPart p) as Element of SCMPDS by A7;
not NAT c= dom q ;
then A8: 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;
B8: not il in dom q by A8, XBOOLE_0:def 5;
dom (DataPart p) c= SCM-Data-Loc by RELAT_1:58, SCMPDS_2:84;
then reconsider d1 = d1 as Int_position by A7, SCMPDS_2:3;
dom (Start-At (il,SCMPDS)) = {(IC )} by FUNCOP_1:13;
then A11: IC in dom (Start-At (il,SCMPDS)) by TARSKI:def 1;
A13: dom p misses {(IC )} by A2, ZFMISC_1:50;
set p2 = p +* (Start-At (il,SCMPDS));
set p1 = p +* (Start-At (il,SCMPDS));
set q2 = q +* (il .--> (d1 := 1));
set q1 = q +* (il .--> (d1 := 0));
UU: dom (il .--> (d1 := 1)) = {il} by FUNCOP_1:13;
then Y6: dom q misses dom (il .--> (d1 := 1)) by B8, ZFMISC_1:50;
dom (il .--> (d1 := 0)) = {il} by FUNCOP_1:13;
then Y5: dom q misses dom (il .--> (d1 := 0)) by B8, ZFMISC_1:50;
consider s1 being State of SCMPDS such that
A14: p +* (Start-At (il,SCMPDS)) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCMPDS such that
B14: q +* (il .--> (d1 := 0)) c= S1 by PBOOLE:145;
consider s2 being State of SCMPDS such that
A15: p +* (Start-At (il,SCMPDS)) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCMPDS such that
B15: q +* (il .--> (d1 := 1)) c= S2 by PBOOLE:145;
take P1 = S1; :: according to EXTPRO_1:def 10 :: thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 p) ) )
take P2 = S2; :: thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) ) )
dom (Start-At (il,SCMPDS)) = dom (Start-At (il,SCMPDS))
.= {(IC )} by FUNCOP_1:13
.= {(IC )} ;
then (dom p) /\ (dom (Start-At (il,SCMPDS))) = (dom p) /\ {(IC )}
.= {} by A13, XBOOLE_0:def 7
.= {} ;
then dom p misses dom (Start-At (il,SCMPDS)) by XBOOLE_0:def 7;
then p c= p +* (Start-At (il,SCMPDS)) by FUNCT_4:32;
then A16: p c= s1 by A14, XBOOLE_1:1;
q c= q +* (il .--> (d1 := 0)) by Y5, FUNCT_4:32;
hence q c= P1 by B14, XBOOLE_1:1; :: thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) ) )
dom (Start-At (il,SCMPDS)) = dom (Start-At (il,SCMPDS))
.= {(IC )} by FUNCOP_1:13
.= {(IC )} ;
then (dom p) /\ (dom (Start-At (il,SCMPDS))) = (dom p) /\ {(IC )}
.= {} by A13, XBOOLE_0:def 7
.= {} ;
then dom p misses dom (Start-At (il,SCMPDS)) by XBOOLE_0:def 7;
then p c= p +* (Start-At (il,SCMPDS)) by FUNCT_4:32;
then A17: p c= s2 by A15, XBOOLE_1:1;
q c= q +* (il .--> (d1 := 1)) by Y6, FUNCT_4:32;
hence q c= P2 by B15, XBOOLE_1:1; :: thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) )
take s1 ; :: thesis: ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s1,b2)) | (proj1 p) = (Comput (P2,b1,b2)) | (proj1 p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 p) = (Comput (P2,s2,b1)) | (proj1 p) )
p c= s1 by A16;
hence p c= s1 ; :: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 p) = (Comput (P2,s2,b1)) | (proj1 p) )
thus p c= s2 by A17; :: thesis: not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 p) = (Comput (P2,s2,b1)) | (proj1 p)
take 1 ; :: thesis: not (Comput (P1,s1,1)) | (proj1 p) = (Comput (P2,s2,1)) | (proj1 p)
A18: dom (p +* (Start-At (il,SCMPDS))) = (dom p) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1;
B18: dom (q +* (il .--> (d1 := 1))) = (dom q) \/ (dom (il .--> (d1 := 1))) by FUNCT_4:def 1;
A20: IC in dom (Start-At (il,SCMPDS)) by A11;
then IC in dom (p +* (Start-At (il,SCMPDS))) by A18, XBOOLE_0:def 3;
then A21: IC s2 = (p +* (Start-At (il,SCMPDS))) . (IC ) by A15, GRFUNC_1:2
.= (Start-At (il,SCMPDS)) . (IC ) by A20, FUNCT_4:13
.= (Start-At (il,SCMPDS)) . (IC )
.= il by FUNCOP_1:72 ;
il in dom (il .--> (d1 := 1)) by UU, TARSKI:def 1;
then A22: il in dom (il .--> (d1 := 1)) ;
then il in dom (q +* (il .--> (d1 := 1))) by B18, XBOOLE_0:def 3;
then A23: S2 . il = (q +* (il .--> (d1 := 1))) . il by B15, GRFUNC_1:2
.= (il .--> (d1 := 1)) . il by A22, FUNCT_4:13
.= (il .--> (d1 := 1)) . il
.= d1 := 1 by FUNCOP_1:72 ;
A24: S2 /. (IC s2) = S2 . (IC s2) by PBOOLE:143;
A25: (Comput (S2,s2,(0 + 1))) . d1 = (Following (S2,(Comput (S2,s2,0)))) . d1 by EXTPRO_1:3
.= (Following (S2,s2)) . d1 by EXTPRO_1:2
.= 1 by A21, A23, A24, SCMPDS_2:45 ;
A26: dom p c= the carrier of SCMPDS by RELAT_1:def 18;
dom (Comput (S1,s1,1)) = the carrier of SCMPDS by PARTFUN1:def 2;
then A27: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A26, RELAT_1:62;
A29: dom (p +* (Start-At (il,SCMPDS))) = (dom p) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1;
B29: dom (q +* (il .--> (d1 := 0))) = (dom q) \/ (dom (il .--> (d1 := 0))) by FUNCT_4:def 1;
A31: IC in dom (Start-At (il,SCMPDS)) by A11;
then IC in dom (p +* (Start-At (il,SCMPDS))) by A29, XBOOLE_0:def 3;
then A32: IC s1 = (p +* (Start-At (il,SCMPDS))) . (IC ) by A14, GRFUNC_1:2
.= (Start-At (il,SCMPDS)) . (IC ) by A31, FUNCT_4:13
.= (Start-At (il,SCMPDS)) . (IC )
.= il by FUNCOP_1:72 ;
VV: dom (il .--> (d1 := 0)) = {il} by FUNCOP_1:13;
il in dom (il .--> (d1 := 0)) by VV, TARSKI:def 1;
then A33: il in dom (il .--> (d1 := 0)) ;
then il in dom (q +* (il .--> (d1 := 0))) by B29, XBOOLE_0:def 3;
then A34: S1 . il = (q +* (il .--> (d1 := 0))) . il by B14, GRFUNC_1:2
.= (il .--> (d1 := 0)) . il by A33, FUNCT_4:13
.= (il .--> (d1 := 0)) . il
.= d1 := 0 by FUNCOP_1:72 ;
A35: S1 /. (IC s1) = S1 . (IC s1) by PBOOLE:143;
A36: dom (Comput (S2,s2,1)) = the carrier of SCMPDS by PARTFUN1:def 2;
A37: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A26, A36, RELAT_1:62;
(Comput (S1,s1,(0 + 1))) . d1 = (Following (S1,(Comput (S1,s1,0)))) . d1 by EXTPRO_1:3
.= (Following (S1,s1)) . d1 by EXTPRO_1:2
.= 0 by A32, A34, A35, SCMPDS_2:45 ;
then ((Comput (S1,s1,1)) | (dom p)) . d1 = 0 by A7, A27, A6, FUNCT_1:47;
hence not (Comput (P1,s1,1)) | (proj1 p) = (Comput (P2,s2,1)) | (proj1 p) by A25, A7, A37, A6, FUNCT_1:47; :: thesis: verum
end;
hence contradiction ; :: thesis: verum