let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; AMISTD_5:def 4 for b1 being set
for b2 being set holds
( not b1 c= b2 or for b3 being set holds
( not q c= b3 or for b4 being set holds IC (Comput (b3,b2,b4)) in dom q ) )
let p be non empty q -autonomic FinPartState of SCM+FSA; for b1 being set holds
( not p c= b1 or for b2 being set holds
( not q c= b2 or for b3 being set holds IC (Comput (b2,b1,b3)) in dom q ) )
let s be State of SCM+FSA; ( not p c= s or for b1 being set holds
( not q c= b1 or for b2 being set holds IC (Comput (b1,s,b2)) in dom q ) )
assume A1:
p c= s
; for b1 being set holds
( not q c= b1 or for b2 being set holds IC (Comput (b1,s,b2)) in dom q )
let P be Instruction-Sequence of SCM+FSA; ( not q c= P or for b1 being set holds IC (Comput (P,s,b1)) in dom q )
assume A2:
q c= P
; for b1 being set holds IC (Comput (P,s,b1)) in dom q
let i be Nat; IC (Comput (P,s,i)) in dom q
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
assume A3:
not IC (Comput (P,s,i)) in dom q
; contradiction
set I = (intloc 0) := (intloc 0);
set q1 = q +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0)));
set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) as Instruction-Sequence of SCM+FSA ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) as Instruction-Sequence of SCM+FSA ;
A5:
IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt SCM+FSA))
by TARSKI:def 1;
A7:
IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0)))
by TARSKI:def 1;
A8:
dom q misses dom ((IC (Comput (P,s,i))) .--> (halt SCM+FSA))
by A3, ZFMISC_1:50;
A9:
dom q misses dom ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0)))
by A3, ZFMISC_1:50;
A10:
q +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) c= P1
by A2, FUNCT_4:123;
A11:
q +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) c= P2
by A2, FUNCT_4:123;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
not p is q -autonomic
proof
((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) . (IC (Comput (P,s,i))) = halt SCM+FSA
by FUNCOP_1:72;
then A12:
P2 . (IC (Comput (P,s,i))) = halt SCM+FSA
by A5, FUNCT_4:13;
A13:
((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) . (IC (Comput (P,s,i))) = (intloc 0) := (intloc 0)
by FUNCOP_1:72;
take
P1
;
EXTPRO_1:def 10 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 set holds (Comput (P1,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take
P2
;
( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0)))
by A9, FUNCT_4:32;
hence A14:
q c= P1
by A10, XBOOLE_1:1;
( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA))
by A8, FUNCT_4:32;
hence A15:
q c= P2
by A11, XBOOLE_1:1;
ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) )
take
s
;
ex b1 being set st
( p c= s & p c= b1 & not for b2 being set holds (Comput (P1,s,b2)) | (dom p) = (Comput (P2,b1,b2)) | (dom p) )
take
s
;
( p c= s & p c= s & not for b1 being set holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
thus
p c= s
by A1;
( p c= s & not for b1 being set holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
A16:
(Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p)
by A14, A2, A1, EXTPRO_1:def 10;
thus
p c= s
by A1;
not for b1 being set holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p)
A17:
(Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p)
by A14, A15, A1, EXTPRO_1:def 10;
take k =
i + 1;
not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p)
set Cs1k =
Comput (
P1,
s,
k);
A18:
IC in dom p
by AMISTD_5:6;
IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p))
by A18, FUNCT_1:49;
then
IC (Comput (P1,s,i)) = IC (Comput (P,s,i))
by A16, A18, FUNCT_1:49;
then A19:
CurInstr (
P1,
(Comput (P1,s,i))) =
P1 . (IC (Comput (P,s,i)))
by PBOOLE:143
.=
(intloc 0) := (intloc 0)
by A13, A7, FUNCT_4:13
;
A20:
Comput (
P1,
s,
k) =
Following (
P1,
(Comput (P1,s,i)))
by EXTPRO_1:3
.=
Exec (
((intloc 0) := (intloc 0)),
(Comput (P1,s,i)))
by A19
;
A21:
IC (Exec (((intloc 0) := (intloc 0)),(Comput (P1,s,i)))) = (IC (Comput (P1,s,i))) + 1
by SCMFSA_2:63;
A22:
IC in dom p
by AMISTD_5:6;
A23:
IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p))
by A22, FUNCT_1:49;
then A24:
IC (Comput (P1,s,k)) =
(IC (Comput (P,s,i))) + 1
by A20, A21, A16, A22, FUNCT_1:49
.=
(IC (Comput (P,s,i))) + 1
;
set Cs2k =
Comput (
P2,
s,
k);
A25:
Comput (
P2,
s,
k) =
Following (
P2,
(Comput (P2,s,i)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P2,(Comput (P2,s,i)))),
(Comput (P2,s,i)))
;
A26:
P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i)))
by PBOOLE:143;
IC (Comput (P2,s,i)) = IC (Comput (P,s,i))
by A16, A23, A17, A22, FUNCT_1:49;
then A27:
IC (Comput (P2,s,k)) = IC (Comput (P,s,i))
by A25, A12, A26, EXTPRO_1:def 3;
(
IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) &
IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) )
by A22, FUNCT_1:49;
hence
not
(Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p)
by A24, A27;
verum
end;
hence
contradiction
; verum