for q being NAT -defined the InstructionsF 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
InstructionsF of
SCM+FSA -valued finite non
halt-free Function;
for p being q -autonomic FinPartState of SCM+FSA st DataPart p <> {} holds
IC in dom plet p be
q -autonomic FinPartState of
SCM+FSA;
( DataPart p <> {} implies IC in dom p )
assume
DataPart p <> {}
;
IC in dom p
then A1:
dom (DataPart p) <> {}
;
assume
not
IC in dom p
;
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 AMI_2:def 16;
A6:
the
Element of
dom (DataPart p) in dom (DataPart p)
by A1;
DataPart p c= p
by MEMSTR_0:12;
then A7:
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
;
not p is q -autonomic then reconsider d1 =
d1 as
Int-Location by AMI_2:def 16;
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 A9:
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 A12:
q +* (il .--> (d1 := d2)) c= S2
by PBOOLE:145;
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)) | (dom p) = (Comput (b1,b3,b4)) | (dom 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)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) )A14:
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 )}
.=
{d2} \/ {(IC )}
;
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 A15:
p c= s1
by A8, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2))
by A14, ZFMISC_1:50;
then
q c= q +* (il .--> (d1 := d2))
by FUNCT_4:32;
hence
q c= P
by A9, 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)) | (dom p) = (Comput (Q,b2,b3)) | (dom 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 )}
.=
{d2} \/ {(IC )}
;
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 A16:
p c= s2
by A11, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2))
by A14, ZFMISC_1:50;
then
q c= q +* (il .--> (d1 := d2))
by FUNCT_4:32;
hence
q c= Q
by A12, 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)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) )take
s1
;
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
;
( 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 A15;
( 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 A16;
not for b1 being set holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p)take
1
;
not (Comput (P,s1,1)) | (dom p) = (Comput (Q,s2,1)) | (dom p)A17:
dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA)))
by FUNCT_4:def 1;
A18:
dom p c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
A19:
dom (Comput (S2,s2,1)) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A20:
dom ((Comput (S2,s2,1)) | (dom p)) = dom p
by A18, A19, RELAT_1:62;
A21:
dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA)))
by FUNCT_4:def 1;
A22:
dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))))
by FUNCT_4:def 1;
A24:
IC in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
then A25:
IC in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))
by A21, XBOOLE_0:def 3;
then
IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))))
by A22, XBOOLE_0:def 3;
then A26:
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 A25, FUNCT_4:13
.=
(Start-At (il,SCM+FSA)) . (IC )
by A24, 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 TARSKI:def 1;
d2 in dom (d2 .--> 0)
by TARSKI:def 1;
then A28:
d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))
by A21, XBOOLE_0:def 3;
then
d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))))
by A22, XBOOLE_0:def 3;
then A29:
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 A28, FUNCT_4:13
.=
(d2 .--> 0) . d2
by A27, FUNCT_4:11
.=
0
by FUNCOP_1:72
;
A30:
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 A30, XBOOLE_0:def 3;
then A31:
S1 . il =
(q +* (il .--> (d1 := d2))) . il
by A9, GRFUNC_1:2
.=
(il .--> (d1 := d2)) . il
by A30, FUNCT_4:13
.=
d1 := d2
by FUNCOP_1:72
;
A32:
dom p c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
A33:
dom (Comput (S1,s1,1)) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A34:
dom ((Comput (S1,s1,1)) | (dom p)) = dom p
by A32, A33, RELAT_1:62;
A35:
dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))))
by FUNCT_4:def 1;
A36:
dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2)))
by FUNCT_4:def 1;
A38:
IC in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
then A39:
IC in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))
by A17, XBOOLE_0:def 3;
then
IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))))
by A35, XBOOLE_0:def 3;
then A40:
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 A39, FUNCT_4:13
.=
(Start-At (il,SCM+FSA)) . (IC )
by A38, FUNCT_4:13
.=
il
by FUNCOP_1:72
;
d2 <> IC
by SCMFSA_2:56;
then A41:
not
d2 in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
d2 in dom (d2 .--> 1)
by TARSKI:def 1;
then A42:
d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))
by A17, XBOOLE_0:def 3;
then
d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))))
by A35, XBOOLE_0:def 3;
then A43:
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 A42, FUNCT_4:13
.=
(d2 .--> 1) . d2
by A41, FUNCT_4:11
.=
1
by FUNCOP_1:72
;
A44:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
il in dom (q +* (il .--> (d1 := d2)))
by A36, A44, XBOOLE_0:def 3;
then A45:
S2 . il =
(q +* (il .--> (d1 := d2))) . il
by A12, GRFUNC_1:2
.=
(il .--> (d1 := d2)) . il
by A44, FUNCT_4:13
.=
d1 := d2
by FUNCOP_1:72
;
A46:
S2 /. (IC s2) = S2 . (IC s2)
by PBOOLE:143;
A47:
(Comput (S2,s2,(0 + 1))) . d1 =
(Following (S2,(Comput (S2,s2,0)))) . d1
by EXTPRO_1:3
.=
(Following (S2,s2)) . d1
.=
1
by A40, A45, A43, A46, SCMFSA_2:63
;
A48:
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
.=
0
by A26, A31, A29, A48, SCMFSA_2:63
;
then
((Comput (S1,s1,1)) | (dom p)) . d1 = 0
by A7, A34, A6, FUNCT_1:47;
hence
(Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p)
by A47, A6, A7, A20, FUNCT_1:47;
verum end; suppose
d1 in FinSeq-Locations
;
not p is q -autonomic then reconsider d1 =
d1 as
FinSeq-Location by SCMFSA_2:def 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 A49:
p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) c= s1
by PBOOLE:141;
consider S1 being
Instruction-Sequence of
SCM+FSA such that A50:
q +* (il .--> (d1 :=<0,...,0> d2)) c= S1
by PBOOLE:145;
A51:
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
Nat such that A52:
k = |.(s1 . d2).|
and A53:
(Exec ((d1 :=<0,...,0> d2),s1)) . d1 = k |-> 0
by SCMFSA_2:75;
A54:
dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))))
by FUNCT_4:def 1;
A55:
dom (q +* (il .--> (d1 :=<0,...,0> d2))) = (dom q) \/ (dom (il .--> (d1 :=<0,...,0> d2)))
by FUNCT_4:def 1;
A57:
IC in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
then A58:
IC in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))
by A51, XBOOLE_0:def 3;
then
IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))))
by A54, XBOOLE_0:def 3;
then A59:
IC s1 =
(p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . (IC )
by A49, GRFUNC_1:2
.=
((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . (IC )
by A58, FUNCT_4:13
.=
(Start-At (il,SCM+FSA)) . (IC )
by A57, FUNCT_4:13
.=
il
by FUNCOP_1:72
;
consider s2 being
State of
SCM+FSA such that A60:
p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) c= s2
by PBOOLE:141;
consider S2 being
Instruction-Sequence of
SCM+FSA such that A61:
q +* (il .--> (d1 :=<0,...,0> d2)) c= S2
by PBOOLE:145;
d2 <> IC
by SCMFSA_2:56;
then A62:
not
d2 in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
d2 in dom (d2 .--> 0)
by TARSKI:def 1;
then A63:
d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))
by A51, XBOOLE_0:def 3;
then
d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))))
by A54, XBOOLE_0:def 3;
then s1 . d2 =
(p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . d2
by A49, GRFUNC_1:2
.=
((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . d2
by A63, FUNCT_4:13
.=
(d2 .--> 0) . d2
by A62, FUNCT_4:11
.=
0
by FUNCOP_1:72
;
then A64:
k |-> 0 =
0 |-> 0
by A52, ABSVALUE:2
.=
{}
by FINSEQ_2:58
;
not
d2 in dom p
by A5, XBOOLE_0:def 5;
then A65:
dom p misses {d2}
by ZFMISC_1:50;
A67:
il in dom (il .--> (d1 :=<0,...,0> d2))
by ZFMISC_1:31;
then
il in dom (q +* (il .--> (d1 :=<0,...,0> d2)))
by A55, XBOOLE_0:def 3;
then A68:
S1 . il =
(q +* (il .--> (d1 :=<0,...,0> d2))) . il
by A50, GRFUNC_1:2
.=
(il .--> (d1 :=<0,...,0> d2)) . il
by A67, FUNCT_4:13
.=
d1 :=<0,...,0> d2
by FUNCOP_1:72
;
A69:
dom p c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
A70:
dom (Comput (S1,s1,1)) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A71:
dom ((Comput (S1,s1,1)) | (dom p)) = dom p
by A69, A70, RELAT_1:62;
consider k being
Nat such that A72:
k = |.(s2 . d2).|
and A73:
(Exec ((d1 :=<0,...,0> d2),s2)) . d1 = k |-> 0
by SCMFSA_2:75;
A74:
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;
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)) | (dom p) = (Comput (b1,b3,b4)) | (dom 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)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) )A76:
not
il in dom q
by A4, XBOOLE_0:def 5;
A77:
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 )}
.=
{d2} \/ {(IC )}
;
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 A65, 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 A78:
p c= s1
by A49, XBOOLE_1:1;
dom q misses dom (il .--> (d1 :=<0,...,0> d2))
by A76, ZFMISC_1:50;
then
q c= q +* (il .--> (d1 :=<0,...,0> d2))
by FUNCT_4:32;
hence
q c= P
by A50, 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)) | (dom p) = (Comput (Q,b2,b3)) | (dom 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 )}
.=
{d2} \/ {(IC )}
;
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 A65, 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 A79:
p c= s2
by A60, XBOOLE_1:1;
dom q misses dom (il .--> (d1 :=<0,...,0> d2))
by A76, ZFMISC_1:50;
then
q c= q +* (il .--> (d1 :=<0,...,0> d2))
by FUNCT_4:32;
hence
q c= Q
by A61, 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)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) )take
s1
;
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
;
( 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 A78;
( 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 A79;
not for b1 being set holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p)take
1
;
not (Comput (P,s1,1)) | (dom p) = (Comput (Q,s2,1)) | (dom p)A80:
dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA)))
by FUNCT_4:def 1;
A82:
IC in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
then A83:
IC in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))
by A80, XBOOLE_0:def 3;
then
IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))))
by A74, XBOOLE_0:def 3;
then A84:
IC s2 =
(p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . (IC )
by A60, GRFUNC_1:2
.=
((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . (IC )
by A83, FUNCT_4:13
.=
(Start-At (il,SCM+FSA)) . (IC )
by A82, FUNCT_4:13
.=
il
by FUNCOP_1:72
;
d2 <> IC
by SCMFSA_2:56;
then A85:
not
d2 in dom (Start-At (il,SCM+FSA))
by TARSKI:def 1;
d2 in dom (d2 .--> 1)
by TARSKI:def 1;
then A86:
d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))
by A80, XBOOLE_0:def 3;
then
d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))))
by A74, XBOOLE_0:def 3;
then s2 . d2 =
(p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . d2
by A60, GRFUNC_1:2
.=
((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . d2
by A86, FUNCT_4:13
.=
(d2 .--> 1) . d2
by A85, FUNCT_4:11
.=
1
by FUNCOP_1:72
;
then A87:
k |-> 0 =
1
|-> 0
by A72, ABSVALUE:def 1
.=
<*0*>
by FINSEQ_2:59
;
A88:
il in dom (il .--> (d1 :=<0,...,0> d2))
by TARSKI:def 1;
then
il in dom (q +* (il .--> (d1 :=<0,...,0> d2)))
by A77, XBOOLE_0:def 3;
then A89:
S2 . il =
(q +* (il .--> (d1 :=<0,...,0> d2))) . il
by A61, GRFUNC_1:2
.=
(il .--> (d1 :=<0,...,0> d2)) . il
by A88, FUNCT_4:13
.=
d1 :=<0,...,0> d2
by FUNCOP_1:72
;
A90:
(Comput (S2,s2,(0 + 1))) . d1 =
(Following (S2,(Comput (S2,s2,0)))) . d1
by EXTPRO_1:3
.=
(Following (S2,s2)) . d1
.=
<*0*>
by A84, A89, A73, A87, PBOOLE:143
;
A91:
dom p c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
A92:
dom (Comput (S2,s2,1)) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A93:
dom ((Comput (S2,s2,1)) | (dom p)) = dom p
by A91, A92, 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 A59, A68, A53, A64, PBOOLE:143
;
then
((Comput (S1,s1,1)) | (dom p)) . d1 = {}
by A6, A7, A71, FUNCT_1:47;
hence
(Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p)
by A90, A6, A7, A93, FUNCT_1:47;
verum end; end;
end;
hence
contradiction
;
verum
end;
hence
SCM+FSA is IC-recognized
by AMISTD_5:3; verum