:: Computation in { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 7, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SCMFSA_2, AMI_1, RELAT_1, AMI_3, FSM_1,
STRUCT_0, FUNCT_4, FUNCOP_1, XBOOLE_0, TARSKI, FUNCT_1, XXREAL_0,
ARYTM_3, GRAPHSP, EXTPRO_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2,
CARD_1, INT_1, CIRCUIT2, ARYTM_1, AMISTD_5, FINSET_1, COMPOS_1, GOBRD13,
NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
INT_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1, NAT_1, STRUCT_0,
FUNCOP_1, FINSEQ_1, FINSEQ_2, MEMSTR_0, COMPOS_1, EXTPRO_1, FUNCT_7,
SCMFSA_2, XXREAL_0, AMISTD_5;
constructors DOMAIN_1, INT_2, AMI_3, SCMFSA_2, RELSET_1, PRE_POLY, SCMFSA_1,
AMISTD_5, FUNCT_7;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0,
SCMFSA_2, FINSET_1, ORDINAL1, COMPOS_1, EXTPRO_1, CARD_1, MEMSTR_0,
FUNCT_4, FUNCOP_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1, AMISTD_5;
equalities EXTPRO_1, FUNCOP_1, SCMFSA_2, MEMSTR_0, SCM_INST;
theorems GRFUNC_1, FUNCOP_1, TARSKI, FUNCT_4, FUNCT_1, ZFMISC_1, INT_1,
RELAT_1, SCMFSA_2, ABSVALUE, FINSEQ_2, XBOOLE_0, XBOOLE_1, PBOOLE,
PARTFUN1, EXTPRO_1, AMISTD_5, MEMSTR_0, AMI_2;
begin :: Finite partial states of SCM+FSA
::$CT 2
reserve k for Nat,
da,db for Int-Location,
fa for FinSeq-Location;
theorem
for s being State of SCM+FSA, iloc being Nat
, a being Int-Location holds s.a = (s +* Start-At(iloc,SCM+FSA)).a
proof
let s be State of SCM+FSA, iloc be Nat, a be
Int-Location;
a in the carrier of SCM+FSA;
then a in dom s by PARTFUN1:def 2;
then
A1: dom (Start-At(iloc,SCM+FSA)) = {IC SCM+FSA} &
a in dom s \/ dom (Start-At(iloc,SCM+FSA))
by XBOOLE_0:def 3;
a <> IC SCM+FSA by SCMFSA_2:56;
then not a in {IC SCM+FSA} by TARSKI:def 1;
hence thesis by A1,FUNCT_4:def 1;
end;
theorem
for s being State of SCM+FSA, iloc being Nat
, a being FinSeq-Location holds s.a = (s +* Start-At(iloc,SCM+FSA)).a
proof
let s be State of SCM+FSA, iloc be Nat, a be
FinSeq-Location;
a in the carrier of SCM+FSA;
then a in dom s by PARTFUN1:def 2;
then
A1: dom (Start-At(iloc,SCM+FSA)) = {IC SCM+FSA} &
a in dom s \/ dom (Start-At(iloc,SCM+FSA))
by XBOOLE_0:def 3;
a <> IC SCM+FSA by SCMFSA_2:57;
then not a in {IC SCM+FSA} by TARSKI:def 1;
hence thesis by A1,FUNCT_4:def 1;
end;
begin :: Autonomic finite partial states of SCM+FSA
definition
let la be Int-Location;
let a be Integer;
redefine func la .--> a -> FinPartState of SCM+FSA; :: redefines .--> (FUNCOP_1, definition)
coherence
proof
a is Element of INT & Values la = INT by INT_1:def 2,SCMFSA_2:11;
hence thesis;
end;
end;
registration
cluster SCM+FSA -> IC-recognized;
coherence
proof
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic FinPartState of SCM+FSA
st DataPart p <> {} holds IC SCM+FSA in dom p
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic FinPartState of SCM+FSA;
assume DataPart p <> {};
then
A1: dom DataPart p <> {};
assume not IC SCM+FSA in dom p;
then
A2: dom p misses {IC SCM+FSA} by ZFMISC_1:50;
p is not 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 SCM+FSA by RELAT_1:58;
not NAT c= dom q;
then
A4: (NAT) \ dom q <> {} by XBOOLE_1:37;
then reconsider il 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 d2 in Int-Locations by XBOOLE_0:def 5;
then reconsider d2 as Int-Location by AMI_2:def 16;
A6: d1 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 as Element of SCM+FSA by A6;
per cases by A6,A3,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
d1 in Int-Locations;
then reconsider 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: p1 c= s1 by PBOOLE:141;
consider S1 being
Instruction-Sequence of SCM+FSA
such that
A9: q1 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: p2 c= s2 by PBOOLE:141;
consider S2 being
Instruction-Sequence of SCM+FSA
such that
A12: q2 c= S2 by PBOOLE:145;
take P = S1, Q = S2;
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 SCM+FSA}
.= {d2} \/ {IC SCM+FSA};
then dom p /\ dom (( d2.--> 0) +* Start-At(il,SCM+FSA)) =
dom p /\ ({d2}) \/ dom p /\ {IC SCM+FSA} 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= p1 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= q1 by FUNCT_4:32;
hence q c= P by A9,XBOOLE_1:1;
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 SCM+FSA}
.= {d2} \/ {IC SCM+FSA};
then dom p /\ dom (( d2.--> 1) +* Start-At(il,SCM+FSA)) =
dom p /\ ({d2}) \/ dom p /\ {IC SCM+FSA} 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= p2 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= q1 by FUNCT_4:32;
hence q c= Q by A12,XBOOLE_1:1;
take s1,s2;
thus p c= s1 by A15;
thus p c= s2 by A16;
take 1;
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 p1 = dom p \/ dom (( d2.--> 0) +*
Start-At(il,SCM+FSA)) by FUNCT_4:def 1;
A24: IC SCM+FSA in dom (Start-At(il,SCM+FSA)) by TARSKI:def 1;
then
A25: IC SCM+FSA in dom (( d2.--> 0) +* Start-At(il,SCM+FSA))
by A21,XBOOLE_0:def 3;
then IC SCM+FSA in dom p1 by A22,XBOOLE_0:def 3;
then
A26: IC s1 = p1.IC SCM+FSA by A8,GRFUNC_1:2
.= (( d2.--> 0) +*
Start-At(il,SCM+FSA)).IC SCM+FSA by A25,FUNCT_4:13
.= (Start-At(il,SCM+FSA)).IC SCM+FSA by A24,FUNCT_4:13
.= il by FUNCOP_1:72;
d2 <> IC SCM+FSA 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 p1 by A22,XBOOLE_0:def 3;
then
A29: s1.d2 = p1.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 q1 = dom q \/ dom(il .--> (d1:=d2)) by FUNCT_4:def 1;
then il in dom q1 by A30,XBOOLE_0:def 3;
then
A31: S1.il = q1.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 p2 = dom p \/ dom (( d2.--> 1) +*
Start-At(il,SCM+FSA)) by FUNCT_4:def 1;
A36: dom q2 = dom q \/ dom(il .--> (d1:=d2)) by FUNCT_4:def 1;
A38: IC SCM+FSA in dom (Start-At(il,SCM+FSA)) by TARSKI:def 1;
then
A39: IC SCM+FSA in dom (( d2.--> 1) +* Start-At(il,SCM+FSA)
) by A17,XBOOLE_0:def 3;
then IC SCM+FSA in dom p2 by A35,XBOOLE_0:def 3;
then
A40: IC s2 = p2.IC SCM+FSA by A11,GRFUNC_1:2
.= (( d2.--> 1) +*
Start-At(il,SCM+FSA)).IC SCM+FSA by A39,FUNCT_4:13
.= (Start-At(il,SCM+FSA)).IC SCM+FSA by A38,FUNCT_4:13
.= il by FUNCOP_1:72;
d2 <> IC SCM+FSA 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 p2 by A35,XBOOLE_0:def 3;
then
A43: s2.d2 = p2.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 q2 by A36,A44,XBOOLE_0:def 3;
then
A45: S2.il = q2.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;
end;
suppose
d1 in FinSeq-Locations;
then reconsider 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: p1 c= s1 by PBOOLE:141;
consider S1 being
Instruction-Sequence of SCM+FSA
such that
A50: q1 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 such that
A52: k = |.s1.d2.| and
A53: Exec(d1:=<0,...,0>d2, s1).d1 = k |-> 0 by SCMFSA_2:75;
A54: dom p1 = dom p \/ dom (( d2.--> 0)
+* Start-At(il,SCM+FSA)) by FUNCT_4:def 1;
A55: dom q1 = dom q \/ dom(il .--> (d1:=<0,...,0>d2)) by FUNCT_4:def 1;
A57: IC SCM+FSA in dom (Start-At(il,SCM+FSA)) by TARSKI:def 1;
then
A58: IC SCM+FSA in dom (( d2.--> 0) +*
Start-At(il,SCM+FSA)) by A51,XBOOLE_0:def 3;
then IC SCM+FSA in dom p1 by A54,XBOOLE_0:def 3;
then
A59: IC s1 = p1.IC SCM+FSA by A49,GRFUNC_1:2
.= (( d2.--> 0) +* Start-At(il,SCM+FSA)).IC SCM+FSA by A58,FUNCT_4:13
.= (Start-At(il,SCM+FSA)).IC SCM+FSA by A57,FUNCT_4:13
.= il by FUNCOP_1:72;
consider s2 being State of SCM+FSA such that
A60: p2 c= s2 by PBOOLE:141;
consider S2 being
Instruction-Sequence of SCM+FSA
such that
A61: q2 c= S2 by PBOOLE:145;
d2 <> IC SCM+FSA 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 p1 by A54,XBOOLE_0:def 3;
then s1.d2 = p1.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 q1 by A55,XBOOLE_0:def 3;
then
A68: S1.il = q1.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 such that
A72: k = |.s2.d2.| and
A73: Exec(d1:=<0,...,0>d2, s2).d1 = k |-> 0 by SCMFSA_2:75;
A74: dom p2 = dom p \/ dom (( d2.--> 1)
+* Start-At(il,SCM+FSA)) by FUNCT_4:def 1;
take P = S1, Q = S2;
A76: not il in dom q by A4,XBOOLE_0:def 5;
A77: dom q2 = 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 SCM+FSA}
.= {d2} \/ {IC SCM+FSA};
then dom p /\ dom (( d2.--> 0) +*
Start-At(il,SCM+FSA)) = dom p /\ ({d2}) \/ dom p /\ {IC SCM+FSA}
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= p1 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= q1 by FUNCT_4:32;
hence q c= P by A50,XBOOLE_1:1;
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 SCM+FSA}
.= {d2} \/ {IC SCM+FSA};
then dom p /\ dom (( d2.--> 1) +*
Start-At(il,SCM+FSA)) = dom p /\ ({d2}) \/ dom p /\ {IC SCM+FSA}
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= p2 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= q2 by FUNCT_4:32;
hence q c= Q by A61,XBOOLE_1:1;
take s1,s2;
thus p c= s1 by A78;
thus p c= s2 by A79;
take 1;
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 SCM+FSA in dom (Start-At(il,SCM+FSA)) by TARSKI:def 1;
then
A83: IC SCM+FSA in dom (( d2.--> 1) +*
Start-At(il,SCM+FSA)) by A80,XBOOLE_0:def 3;
then IC SCM+FSA in dom p2 by A74,XBOOLE_0:def 3;
then
A84: IC s2 = p2.IC SCM+FSA by A60,GRFUNC_1:2
.= (( d2.--> 1) +* Start-At(il,SCM+FSA)).IC SCM+FSA by A83,FUNCT_4:13
.= (Start-At(il,SCM+FSA)).IC SCM+FSA by A82,FUNCT_4:13
.= il by FUNCOP_1:72;
d2 <> IC SCM+FSA 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 p2 by A74,XBOOLE_0:def 3;
then s2.d2 = p2.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 q2 by A77,XBOOLE_0:def 3;
then
A89: S2.il = q2.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;
end;
end;
hence contradiction;
end;
hence thesis by AMISTD_5:3;
end;
end;
registration
cluster SCM+FSA -> CurIns-recognized;
coherence
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s be State of SCM+FSA such that
A1: p c= s;
let P be Instruction-Sequence of SCM+FSA such that
A2: q c= P;
let i be Nat;
set Csi = Comput(P,s,i);
set loc = IC Csi;
set loc1 = loc+1;
assume
A3: not IC Comput(P,s,i) in dom q;
set I = intloc 0 := intloc 0;
set q1 = q +* (loc .--> I);
set q2 = q +* (loc .--> halt SCM+FSA);
reconsider P1 = P +* (loc .--> I)
as Instruction-Sequence of SCM+FSA;
reconsider P2 = P +* (loc .--> halt SCM+FSA)
as Instruction-Sequence of SCM+FSA;
A5: loc in dom (loc .--> halt SCM+FSA) by TARSKI:def 1;
A7: loc in dom (loc .--> I) by TARSKI:def 1;
A8: dom q misses dom (loc .--> halt SCM+FSA) by A3,ZFMISC_1:50;
A9: dom q misses dom (loc .--> I) by A3,ZFMISC_1:50;
A10: q1 c= P1 by A2,FUNCT_4:123;
A11: q2 c= P2 by A2,FUNCT_4:123;
set Cs2i = Comput(P2,s,i), Cs1i = Comput(P1,s,i);
p is not q-autonomic
proof
(loc .--> halt SCM+FSA).loc = halt SCM+FSA by FUNCOP_1:72;
then
A12: P2.loc = halt SCM+FSA by A5,FUNCT_4:13;
A13: (loc .--> I).loc = I by FUNCOP_1:72;
take P1, P2;
q c= q1 by A9,FUNCT_4:32;
hence
A14: q c= P1 by A10,XBOOLE_1:1;
q c= q2 by A8,FUNCT_4:32;
hence
A15: q c= P2 by A11,XBOOLE_1:1;
take s, s;
thus p c= s by A1;
A16: (Cs1i|dom p) = (Csi|dom p) by A14,A2,A1,EXTPRO_1:def 10;
thus p c= s by A1;
A17: (Cs1i|dom p) = (Cs2i|dom p) by A14,A15,A1,EXTPRO_1:def 10;
take k = i+1;
set Cs1k = Comput(P1,s,k);
A18: IC SCM+FSA in dom p by AMISTD_5:6;
IC Csi = IC(Csi|dom p) by A18,FUNCT_1:49;
then
IC Cs1i = loc by A16,A18,FUNCT_1:49;
then
A19: CurInstr(P1,Cs1i) = P1.loc by PBOOLE:143
.= I by A13,A7,FUNCT_4:13;
A20: Cs1k = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec(I,Cs1i) by A19;
A21: IC Exec(I,Cs1i) = IC Cs1i + 1 by SCMFSA_2:63;
A22: IC SCM+FSA in dom p by AMISTD_5:6;
A23: IC Csi = IC(Csi|dom p) by A22,FUNCT_1:49;
then
A24: IC Cs1k = loc+1 by A20,A21,A16,A22,FUNCT_1:49
.= loc1;
set Cs2k = Comput(P2,s,k);
A25: Cs2k = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
A26: P2/.IC Cs2i = P2.IC Cs2i by PBOOLE:143;
IC Cs2i = loc by A16,A23,A17,A22,FUNCT_1:49;
then
A27: IC Cs2k = loc by A25,A12,A26,EXTPRO_1:def 3;
IC(Cs1k|dom p) = IC Cs1k & IC(Cs2k|dom p) = IC Cs2k
by A22,FUNCT_1:49;
hence thesis by A24,A27;
end;
hence contradiction;
end;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,i)) = da := db & da in dom p
holds Comput(P1,s1,i).db = Comput(P2,s2,i).db
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
A4: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
assume that
A5: I = da := db and
A6: da in dom p & Comput(P1,s1,i).db <> Comput(P2,s2,i).db;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
then
A7: Cs1i1.da = Cs1i.db by A5,SCMFSA_2:63;
I = CurInstr(P2,Comput(P2,s2,i)) by A1,A2,AMISTD_5:7;
then Cs2i1.da = Cs2i.db by A3,A5,SCMFSA_2:63;
hence contradiction by A4,A6,A7,A2,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,i)) = AddTo(da, db)
& da in dom
p holds Comput(P1,s1,i).da + Comput(P1,s1,i).db =
Comput(P2,s2,i).da + Comput(P2,s2,i).db
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
A4: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
assume that
A5: I = AddTo(da, db) and
A6: da in dom p & Comput(P1,s1,i).da + Comput(P1,s1,i
).db <>
Comput(P2,s2, i).da + Comput(P2,s2,i).db;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
then
A7: Cs1i1.da = Cs1i.da + Cs1i.db by A5,SCMFSA_2:64;
I = CurInstr(P2,Comput(P2,s2,i)) by A1,A2,AMISTD_5:7;
then Cs2i1.da = Cs2i.da + Cs2i.db by A3,A5,SCMFSA_2:64;
hence contradiction by A1,A4,A6,A7,A2,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,
i)) = SubFrom(da, db)
& da in
dom p holds Comput(P1,s1,i).da - Comput(P1,s1,i).db =
Comput(P2,s2,i).da
- Comput(P2,s2,i).db
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
A4: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
assume that
A5: I = SubFrom(da, db) and
A6: da in dom p & Comput(P1,s1,i).da - Comput(P1,s1,i
).db <>
Comput(P2,s2, i).da - Comput(P2,s2,i).db;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
then
A7: Cs1i1.da = Cs1i.da - Cs1i.db by A5,SCMFSA_2:65;
I = CurInstr(P2,Comput(P2,
s2,i)) by A1,A2,AMISTD_5:7;
then Cs2i1.da = Cs2i.da - Cs2i.db by A3,A5,SCMFSA_2:65;
hence contradiction by A1,A4,A6,A7,A2,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,
i)) = MultBy(da, db)
& da in
dom p holds Comput(P1,s1,i).da * Comput(P1,s1,i).db =
Comput(P2,s2,i).da
* Comput(P2,s2,i).db
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
A4: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
assume that
A5: I = MultBy(da, db) and
A6: da in dom p & Comput(P1,s1,i).da * Comput(P1,s1,i
).db <>
Comput(P2,s2, i).da * Comput(P2,s2,i).db;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
then
A7: Cs1i1.da = Cs1i.da * Cs1i.db by A5,SCMFSA_2:66;
I = CurInstr(P2,Comput(P2,
s2,i)) by A1,A2,AMISTD_5:7;
then Cs2i1.da = Cs2i.da * Cs2i.db by A3,A5,SCMFSA_2:66;
hence contradiction by A1,A4,A6,A7,A2,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,
i)) = Divide(da, db)
& da in
dom p & da <> db holds Comput(P1,s1,i).da div
Comput(P1,s1,i).db =
Comput(P2,s2,i).da div Comput(P2,s2,i).db
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
A4: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
assume that
A5: I = Divide(da, db) and
A6: da in dom p and
A7: da <> db and
A8: Comput(P1,s1,i).da div Comput(P1,s1,i).db <>
Comput(P2,s2,i).
da div Comput(P2,s2,i).db;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
then
A9: Cs1i1.da = Cs1i.da div Cs1i.db by A5,A7,SCMFSA_2:67;
I = CurInstr(P2,Comput(P2,
s2,i)) by A1,A2,AMISTD_5:7;
then Cs2i1.da = Cs2i.da div Cs2i.db by A3,A5,A7,SCMFSA_2:67;
hence contradiction by A1,A4,A8,A9,A2,A6,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,i)) = Divide(da, db)
& db in
dom p holds Comput(P1,s1,i).da mod Comput(P1,s1,i).db
= Comput(P2,s2,i).
da mod Comput(P2,s2,i).db
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
assume that
A4: I = Divide(da, db) and
A5: db in dom p and
A6: Comput(P1,s1,i).da mod Comput(P1,s1,i).db <>
Comput(P2,s2,i).
da mod Comput(P2,s2,i).db;
A7: (Cs1i1|dom p).db = Cs1i1.db & (Cs2i1|dom p).db = Cs2i1.db
by A5,FUNCT_1:49;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
then
A8: Cs1i1.db = Cs1i.da mod Cs1i.db by A4,SCMFSA_2:67;
I = CurInstr(P2,Comput(P2,
s2,i)) by A1,A2,AMISTD_5:7;
then Cs2i1.db = Cs2i.da mod Cs2i.db by A3,A4,SCMFSA_2:67;
hence contradiction by A1,A6,A7,A8,A2,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da being Int-Location, loc being Nat st
CurInstr(P1,Comput(P1,s1,i)) = da=0_goto loc &
loc <> (IC Comput(P1,s1,i))+1 holds (
Comput(P1,s1,i).da = 0 iff Comput(P2,s2,i).da = 0)
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da be Int-Location, loc be Nat;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
IC SCM+FSA in dom p by AMISTD_5:6;
then
A5: (Cs1i1|dom p).IC SCM+FSA = Cs1i1.IC SCM+FSA &
(Cs2i1|dom p).IC SCM+FSA =
Cs2i1.IC SCM+FSA by FUNCT_1:49;
assume that
A6: I = da=0_goto loc and
A7: loc <> (IC Comput(P1,s1,i))+1;
A8: I = CurInstr(P2,Comput(P2,s2,i)) by A1,A2,AMISTD_5:7;
A9: now
assume
Comput(P2,s2,i).da = 0 & Comput(P1,s1,i).da <> 0;
then
Cs2i1.IC SCM+FSA = loc & Cs1i1.IC SCM+FSA = IC Cs1i + 1 by A8,A3,A4,A6,
SCMFSA_2:70;
hence contradiction by A1,A5,A7,A2,EXTPRO_1:def 10;
end;
A10: (Cs1i1|dom p) = (Cs2i1|dom p) by A1,A2,EXTPRO_1:def 10;
now
assume
Comput(P1,s1,i).da = 0 & Comput(P2,s2,i).da <> 0;
then
Cs1i1.IC SCM+FSA = loc & Cs2i1.IC SCM+FSA = IC Cs2i + 1 by A8,A3,A4,A6,
SCMFSA_2:70;
hence contradiction by A1,A5,A10,A7,A2,AMISTD_5:7;
end;
hence thesis by A9;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da being Int-Location, loc being Nat st
CurInstr(P1,Comput(P1,s1,i)) = da>0_goto loc &
loc <> (IC Comput(P1,s1,i))+1 holds
Comput(P1,s1,i).da > 0 iff Comput(P2,s2,i).da > 0
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da be Int-Location, loc be Nat;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: (Cs1i1|dom p) = (Cs2i1|dom p) by A1,A2,EXTPRO_1:def 10;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
IC SCM+FSA in dom p by AMISTD_5:6;
then
A5: (Cs1i1|dom p).IC SCM+FSA = Cs1i1.IC SCM+FSA &
(Cs2i1|dom p).IC SCM+FSA =
Cs2i1.IC SCM+FSA by FUNCT_1:49;
A6: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
assume that
A7: I = da>0_goto loc and
A8: loc <> (IC Comput(P1,s1,i))+1;
A9: I = CurInstr(P2,Comput(P2,s2,i)) by A1,A2,AMISTD_5:7;
A10: now
assume that
A11: Comput(P2,s2,i).da > 0 and
A12: Comput(P1,s1,i).da <= 0;
Cs2i1.IC SCM+FSA = loc by A9,A6,A7,A11,SCMFSA_2:71;
hence contradiction by A4,A5,A3,A7,A8,A12,SCMFSA_2:71;
end;
A13: IC Cs1i = IC Cs2i by A1,A2,AMISTD_5:7;
now
assume that
A14: Comput(P1,s1,i).da > 0 and
A15: Comput(P2,s2,i).da <= 0;
Cs1i1.IC SCM+FSA = loc by A4,A7,A14,SCMFSA_2:71;
hence contradiction by A13,A9,A6,A5,A3,A7,A8,A15,SCMFSA_2:71;
end;
hence thesis by A10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)
) =
da := (f,db) & da in dom p for k1,k2 being Element of NAT st k1 = |.
Comput(P1,s1,i).db.| & k2 = |. Comput(P2,s2,i).db.|
holds ( Comput(P1,s1,
i).f)/.k1 = ( Comput(P2,s2,i).f)/.k2
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location, f be FinSeq-Location;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs1i1|dom p = Cs2i1|dom p by A1,A2,EXTPRO_1:def 10;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A5: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
A6: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
assume that
A7: I = da := (f,db) and
A8: da in dom p;
A9: (ex k1 being Nat st k1 = |.Cs1i.db.| & Exec(I, Cs1i).da = (
Cs1i .f)/.k1 )& ex k2 being Nat st k2 = |.Cs2i.db.| &
Exec(I, Cs2i
). da = (Cs2i.f)/.k2 by A7,SCMFSA_2:72;
let i1,i2 be Element of NAT;
assume
i1 = |. Comput(P1,s1,i).db.| & i2 = |. Comput(P2
,s2,i).db.| &
( Comput(P1,s1,i).f)/.i1 <> ( Comput(P2,s2,i).f)/.
i2;
hence contradiction by A1,A4,A6,A5,A3,A9,A8,A2,AMISTD_5:7;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)
) =
(f,db):=da & f in dom p for k1,k2 being Nat st k1 = |. Comput(
P1,s1,i).db.| & k2 = |. Comput(P2,s2,i).db.| holds
Comput(P1,s1,i).f+*(k1,
Comput(P1,s1,i).da) = Comput(P2,s2,i).f+*(k2,
Comput(P2,s2,i).da)
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Int-Location, f be FinSeq-Location;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs1i1|dom p = Cs2i1|dom p by A1,A2,EXTPRO_1:def 10;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A5: f in dom p implies
(Cs1i1|dom p).f = Cs1i1.f & (Cs2i1|dom p).f = Cs2i1.f
by FUNCT_1:49;
A6: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
assume that
A7: I = (f,db):=da and
A8: f in dom p;
A9: (ex k1 being Nat st k1 = |.Cs1i.db.| & Exec(I, Cs1i).f =
Cs1i.f +*(k1,Cs1i.da) )& ex k2 being Nat st k2 = |.Cs2i.db.| &
Exec
(I, Cs2i).f = Cs2i.f+*(k2,Cs2i.da) by A7,SCMFSA_2:73;
let i1, i2 be Nat;
assume i1 = |.Cs1i.db.| & i2 = |.Cs2i.db.| & Cs1i.f+*(i1,Cs1i.da) <> Cs2i
.f+* (i2,Cs2i.da);
hence contradiction by A1,A4,A6,A5,A3,A9,A8,A2,AMISTD_5:7;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da
being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)) =
da :=len f & da in dom p holds len( Comput(P1,s1,i).f)
= len(Comput(P2,s2,i).f)
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da be Int-Location, f be FinSeq-Location;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs1i1|dom p = Cs2i1|dom p by A1,A2,EXTPRO_1:def 10;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A5: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
A6: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
assume that
A7: I = da :=len f and
A8: da in dom p & len( Comput(P1,s1,i).f) <> len( Comput(
P2,s2,i).f);
Exec(I, Cs1i).da = len(Cs1i.f) & Exec(I, Cs2i).da = len(Cs2i.f) by A7,
SCMFSA_2:74;
hence contradiction by A1,A4,A6,A5,A3,A8,A2,AMISTD_5:7;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)) =
f:=<0,...,0>da & f in dom p for k1,k2 being Nat st k1 = |.
Comput(P1,s1,i).da.| & k2 = |. Comput(P2,s2,i).da.|
holds k1 |-> 0 = k2 |-> 0
proof
let q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM+FSA,
s1, s2 be State
of SCM+FSA such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM+FSA
such that
A2: q c= P1 & q c= P2;
let i be Nat, da be Int-Location, f be FinSeq-Location;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: Cs1i1|dom p = Cs2i1|dom p by A1,A2,EXTPRO_1:def 10;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A5: f in dom p implies
(Cs1i1|dom p).f = Cs1i1.f & (Cs2i1|dom p).f = Cs2i1.f
by FUNCT_1:49;
A6: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
assume that
A7: I = f:=<0,...,0>da and
A8: f in dom p;
A9: (ex k1 being Nat st k1 = |.Cs1i.da.| & Exec(I, Cs1i).f = k1
|->0 )& ex k2 being Nat st k2 = |.Cs2i.da.| & Exec(I, Cs2i).f = k2
|->0 by A7,SCMFSA_2:75;
let i1, i2 be Nat;
assume i1 = |.Cs1i.da.| & i2 = |.Cs2i.da.| & i1 |-> 0 <> i2 |->0;
hence contradiction by A1,A4,A6,A5,A3,A9,A8,A2,AMISTD_5:7;
end;