for q being NAT -defined the Instructions of SCM+FSA -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of SCM+FSA st DataPart p <> {} holds
IC in dom p
proof
let q be NAT -defined the Instructions of SCM+FSA -valued finite non halt-free Function; :: thesis: for p being q -autonomic FinPartState of SCM+FSA st DataPart p <> {} holds
IC in dom p
let p be q -autonomic FinPartState of SCM+FSA; :: thesis: ( DataPart p <> {} implies IC in dom p )
assume DataPart p <> {} ; :: thesis: IC in dom p
then A1: dom (DataPart p) <> {} ;
assume not IC in dom p ; :: thesis: contradiction
then A2: dom p misses {(IC )} by ZFMISC_1:50;
not p is q -autonomic
proof
set il = the Element of NAT \ (dom q);
set d2 = the Element of Int-Locations \ (dom p);
set d1 = the Element of dom (DataPart p);
A3: dom (DataPart p) c= Data-Locations by RELAT_1:58;
not NAT c= dom q ;
then A4: 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;
not Int-Locations c= dom p ;
then A5: Int-Locations \ (dom p) <> {} by XBOOLE_1:37;
then the Element of Int-Locations \ (dom p) in Int-Locations by XBOOLE_0:def 5;
then reconsider d2 = the Element of Int-Locations \ (dom p) as Int-Location by SCMFSA_2:4;
A6: the Element of dom (DataPart p) in dom (DataPart p) by A1;
DataPart p c= p by MEMSTR_0:12;
then B7: dom (DataPart p) c= dom p by RELAT_1:11;
dom (DataPart p) c= the carrier of SCM+FSA by RELAT_1:def 18;
then reconsider d1 = the Element of dom (DataPart p) as Element of SCM+FSA by A6;
per cases ( d1 in Int-Locations or d1 in FinSeq-Locations ) by A6, A3, SCMFSA_2:100, XBOOLE_0:def 3;
suppose d1 in Int-Locations ; :: thesis: not p is q -autonomic
then reconsider d1 = d1 as Int-Location by SCMFSA_2:4;
set p1 = p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)));
set p2 = p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)));
set q1 = q +* (il .--> (d1 := d2));
set q2 = q +* (il .--> (d1 := d2));
consider s1 being State of SCM+FSA such that
A8: p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCM+FSA such that
B8: q +* (il .--> (d1 := d2)) c= S1 by PBOOLE:145;
not d2 in dom p by A5, XBOOLE_0:def 5;
then A10: dom p misses {d2} by ZFMISC_1:50;
consider s2 being State of SCM+FSA such that
A11: p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCM+FSA such that
B11: q +* (il .--> (d1 := d2)) c= S2 by PBOOLE:145;
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 Element of NAT holds (Comput (P,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 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 Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
UU: dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
VV: not il in dom q by A4, XBOOLE_0:def 5;
dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1
.= (dom (d2 .--> 0)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def 7
.= {} by A10, XBOOLE_0:def 7 ;
then dom p misses dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def 7;
then p c= p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A12: p c= s1 by A8, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2)) by UU, VV, ZFMISC_1:50;
then q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32;
hence q c= P by B8, XBOOLE_1:1; :: thesis: ( q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1
.= (dom (d2 .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def 7
.= {} by A10, XBOOLE_0:def 7 ;
then dom p misses dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def 7;
then p c= p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A13: p c= s2 by A11, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2)) by UU, VV, ZFMISC_1:50;
then q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32;
hence q c= Q by B11, 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 (P,b1,b3)) | (proj1 p) = (Comput (Q,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 (P,s1,b2)) | (proj1 p) = (Comput (Q,b1,b2)) | (proj1 p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus p c= s1 by A12; :: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus p c= s2 by A13; :: thesis: not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p)
take 1 ; :: thesis: not (Comput (P,s1,1)) | (proj1 p) = (Comput (Q,s2,1)) | (proj1 p)
A14: dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1;
A15: dom p c= the carrier of SCM+FSA by RELAT_1:def 18;
A16: dom (Comput (S2,s2,1)) = the carrier of SCM+FSA by PARTFUN1:def 2;
A17: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A15, A16, RELAT_1:62;
A19: dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1;
A20: dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def 1;
A21: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A22: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def 1;
then A23: IC in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A19, XBOOLE_0:def 3;
then IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A20, XBOOLE_0:def 3;
then A24: IC s1 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . (IC ) by A8, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . (IC ) by A23, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A22, FUNCT_4:13
.= il by FUNCOP_1:72 ;
d2 <> IC by SCMFSA_2:56;
then A27: not d2 in dom (Start-At (il,SCM+FSA)) by A21, TARSKI:def 1;
dom (d2 .--> 0) = {d2} by FUNCOP_1:13;
then d2 in dom (d2 .--> 0) by TARSKI:def 1;
then A30: d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A19, XBOOLE_0:def 3;
then d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A20, XBOOLE_0:def 3;
then A31: s1 . d2 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . d2 by A8, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . d2 by A30, FUNCT_4:13
.= (d2 .--> 0) . d2 by A27, FUNCT_4:11
.= 0 by FUNCOP_1:72 ;
dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
then A33: 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 A33, XBOOLE_0:def 3;
then A34: S1 . il = (q +* (il .--> (d1 := d2))) . il by B8, GRFUNC_1:2
.= (il .--> (d1 := d2)) . il by A33, FUNCT_4:13
.= d1 := d2 by FUNCOP_1:72 ;
A35: dom p c= the carrier of SCM+FSA by RELAT_1:def 18;
A36: dom (Comput (S1,s1,1)) = the carrier of SCM+FSA by PARTFUN1:def 2;
A37: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A35, A36, RELAT_1:62;
A38: dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def 1;
B38: dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def 1;
A39: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A40: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def 1;
then A41: IC in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A14, XBOOLE_0:def 3;
then IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A38, XBOOLE_0:def 3;
then A42: IC s2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . (IC ) by A11, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . (IC ) by A41, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A40, FUNCT_4:13
.= il by FUNCOP_1:72 ;
d2 <> IC by SCMFSA_2:56;
then A43: not d2 in dom (Start-At (il,SCM+FSA)) by A39, TARSKI:def 1;
dom (d2 .--> 1) = {d2} by FUNCOP_1:13;
then d2 in dom (d2 .--> 1) by TARSKI:def 1;
then A46: d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A14, XBOOLE_0:def 3;
then d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A38, XBOOLE_0:def 3;
then A47: s2 . d2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . d2 by A11, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . d2 by A46, FUNCT_4:13
.= (d2 .--> 1) . d2 by A43, FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
then A50: il in dom (il .--> (d1 := d2)) by TARSKI:def 1;
il in dom (q +* (il .--> (d1 := d2))) by B38, A50, XBOOLE_0:def 3;
then A51: S2 . il = (q +* (il .--> (d1 := d2))) . il by B11, GRFUNC_1:2
.= (il .--> (d1 := d2)) . il by A50, FUNCT_4:13
.= d1 := d2 by FUNCOP_1:72 ;
A52: S2 /. (IC s2) = S2 . (IC s2) by PBOOLE:143;
A53: (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 A42, A51, A47, A52, SCMFSA_2:63 ;
A54: 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
.= (Following (S1,s1)) . d1 by EXTPRO_1:2
.= 0 by A24, A34, A31, A54, SCMFSA_2:63 ;
then ((Comput (S1,s1,1)) | (dom p)) . d1 = 0 by B7, A37, A6, FUNCT_1:47;
hence (Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p) by A53, A6, B7, A17, FUNCT_1:47; :: thesis: verum
end;
suppose d1 in FinSeq-Locations ; :: thesis: not p is q -autonomic
then reconsider d1 = d1 as FinSeq-Location by SCMFSA_2:5;
set p1 = p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)));
set p2 = p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)));
set q1 = q +* (il .--> (d1 :=<0,...,0> d2));
set q2 = q +* (il .--> (d1 :=<0,...,0> d2));
consider s1 being State of SCM+FSA such that
A55: p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCM+FSA such that
B55: q +* (il .--> (d1 :=<0,...,0> d2)) c= S1 by PBOOLE:145;
A57: dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1;
consider k being Element of NAT such that
A58: k = abs (s1 . d2) and
A59: (Exec ((d1 :=<0,...,0> d2),s1)) . d1 = k |-> 0 by SCMFSA_2:75;
A61: dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def 1;
B61: dom (q +* (il .--> (d1 :=<0,...,0> d2))) = (dom q) \/ (dom (il .--> (d1 :=<0,...,0> d2))) by FUNCT_4:def 1;
A62: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A63: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def 1;
then A64: IC in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A57, XBOOLE_0:def 3;
then IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A61, XBOOLE_0:def 3;
then A65: IC s1 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . (IC ) by A55, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . (IC ) by A64, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A63, FUNCT_4:13
.= il by FUNCOP_1:72 ;
consider s2 being State of SCM+FSA such that
A67: p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCM+FSA such that
B67: q +* (il .--> (d1 :=<0,...,0> d2)) c= S2 by PBOOLE:145;
d2 <> IC by SCMFSA_2:56;
then A68: not d2 in dom (Start-At (il,SCM+FSA)) by A62, TARSKI:def 1;
dom (d2 .--> 0) = {d2} by FUNCOP_1:13;
then d2 in dom (d2 .--> 0) by TARSKI:def 1;
then A71: d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A57, XBOOLE_0:def 3;
then d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A61, XBOOLE_0:def 3;
then s1 . d2 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . d2 by A55, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . d2 by A71, FUNCT_4:13
.= (d2 .--> 0) . d2 by A68, FUNCT_4:11
.= 0 by FUNCOP_1:72 ;
then A72: k |-> 0 = 0 |-> 0 by A58, ABSVALUE:2
.= {} by FINSEQ_2:58 ;
not d2 in dom p by A5, XBOOLE_0:def 5;
then A73: dom p misses {d2} by ZFMISC_1:50;
B74: dom (il .--> (d1 :=<0,...,0> d2)) = {il} by FUNCOP_1:13;
A75: il in dom (il .--> (d1 :=<0,...,0> d2)) by B74, ZFMISC_1:31;
then il in dom (q +* (il .--> (d1 :=<0,...,0> d2))) by B61, XBOOLE_0:def 3;
then A76: S1 . il = (q +* (il .--> (d1 :=<0,...,0> d2))) . il by B55, GRFUNC_1:2
.= (il .--> (d1 :=<0,...,0> d2)) . il by A75, FUNCT_4:13
.= d1 :=<0,...,0> d2 by FUNCOP_1:72 ;
A77: dom p c= the carrier of SCM+FSA by RELAT_1:def 18;
A78: dom (Comput (S1,s1,1)) = the carrier of SCM+FSA by PARTFUN1:def 2;
A79: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A77, A78, RELAT_1:62;
consider k being Element of NAT such that
A81: k = abs (s2 . d2) and
A82: (Exec ((d1 :=<0,...,0> d2),s2)) . d1 = k |-> 0 by SCMFSA_2:75;
A83: dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def 1;
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 Element of NAT holds (Comput (P,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 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 Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
UU: dom (il .--> (d1 :=<0,...,0> d2)) = {il} by FUNCOP_1:13;
VV: not il in dom q by A4, XBOOLE_0:def 5;
B83: dom (q +* (il .--> (d1 :=<0,...,0> d2))) = (dom q) \/ (dom (il .--> (d1 :=<0,...,0> d2))) by FUNCT_4:def 1;
dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1
.= (dom (d2 .--> 0)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def 7
.= {} by A73, XBOOLE_0:def 7 ;
then dom p misses dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def 7;
then p c= p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A84: p c= s1 by A55, XBOOLE_1:1;
dom q misses dom (il .--> (d1 :=<0,...,0> d2)) by UU, VV, ZFMISC_1:50;
then q c= q +* (il .--> (d1 :=<0,...,0> d2)) by FUNCT_4:32;
hence q c= P by B55, XBOOLE_1:1; :: thesis: ( q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1
.= (dom (d2 .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def 7
.= {} by A73, XBOOLE_0:def 7 ;
then dom p misses dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def 7;
then p c= p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A85: p c= s2 by A67, XBOOLE_1:1;
dom q misses dom (il .--> (d1 :=<0,...,0> d2)) by UU, VV, ZFMISC_1:50;
then q c= q +* (il .--> (d1 :=<0,...,0> d2)) by FUNCT_4:32;
hence q c= Q by B67, 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 (P,b1,b3)) | (proj1 p) = (Comput (Q,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 (P,s1,b2)) | (proj1 p) = (Comput (Q,b1,b2)) | (proj1 p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus p c= s1 by A84; :: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus p c= s2 by A85; :: thesis: not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p)
take 1 ; :: thesis: not (Comput (P,s1,1)) | (proj1 p) = (Comput (Q,s2,1)) | (proj1 p)
A86: dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def 1;
A87: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A88: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def 1;
then A89: IC in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A86, XBOOLE_0:def 3;
then IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A83, XBOOLE_0:def 3;
then A90: IC s2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . (IC ) by A67, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . (IC ) by A89, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A88, FUNCT_4:13
.= il by FUNCOP_1:72 ;
d2 <> IC by SCMFSA_2:56;
then A91: not d2 in dom (Start-At (il,SCM+FSA)) by A87, TARSKI:def 1;
dom (d2 .--> 1) = {d2} by FUNCOP_1:13;
then d2 in dom (d2 .--> 1) by TARSKI:def 1;
then A94: d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A86, XBOOLE_0:def 3;
then d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A83, XBOOLE_0:def 3;
then s2 . d2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . d2 by A67, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . d2 by A94, FUNCT_4:13
.= (d2 .--> 1) . d2 by A91, FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
then A95: k |-> 0 = 1 |-> 0 by A81, ABSVALUE:def 1
.= <*0*> by FINSEQ_2:59 ;
dom (il .--> (d1 :=<0,...,0> d2)) = {il} by FUNCOP_1:13;
then A98: il in dom (il .--> (d1 :=<0,...,0> d2)) by TARSKI:def 1;
then il in dom (q +* (il .--> (d1 :=<0,...,0> d2))) by B83, XBOOLE_0:def 3;
then A99: S2 . il = (q +* (il .--> (d1 :=<0,...,0> d2))) . il by B67, GRFUNC_1:2
.= (il .--> (d1 :=<0,...,0> d2)) . il by A98, FUNCT_4:13
.= d1 :=<0,...,0> d2 by FUNCOP_1:72 ;
A101: (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
.= <*0*> by A90, A99, A82, A95, PBOOLE:143 ;
A102: dom p c= the carrier of SCM+FSA by RELAT_1:def 18;
A103: dom (Comput (S2,s2,1)) = the carrier of SCM+FSA by PARTFUN1:def 2;
A104: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A102, A103, 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
.= {} by A65, A76, A59, A72, PBOOLE:143 ;
then ((Comput (S1,s1,1)) | (dom p)) . d1 = {} by A6, B7, A79, FUNCT_1:47;
hence (Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p) by A101, A6, B7, A104, FUNCT_1:47; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence SCM+FSA is IC-recognized by AMISTD_5:3; :: thesis: verum