:: An Extension of { \bf SCM }
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 3, 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, AMI_2, XBOOLE_0, TARSKI, CARD_1, FINSEQ_1,
ZFMISC_1, RELAT_1, AMI_1, ORDINAL1, XXREAL_0, FUNCT_1, FUNCOP_1, FUNCT_4,
INT_1, CARD_3, PBOOLE, NAT_1, PARTFUN1, COMPLEX1, FINSEQ_2, FUNCT_2,
FUNCT_5, SCMFSA_1, GROUP_9, RECDEF_2, AFINSQ_1, ARYTM_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
CARD_1, NUMBERS, INT_2, PBOOLE, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
BINOP_1, XCMPLX_0, INT_1, AFINSQ_1, FINSEQ_1, FUNCT_4, FUNCT_5, FINSEQ_2,
CARD_3, FUNCOP_1, FUNCT_7, XXREAL_0, RECDEF_2, MEMSTR_0, SCM_INST, AMI_2,
SCMFSA_I;
constructors INT_2, FUNCT_5, RELSET_1, FUNCT_7, PRE_POLY, AMI_3, SCMFSA_I,
BINOP_1, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1, FINSEQ_1,
CARD_3, AMI_2, RELAT_1, FINSET_1, CARD_1, CARD_2, RELSET_1, FUNCT_2,
AFINSQ_1, COMPOS_0, SCM_INST, SCMFSA_I;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions FUNCT_1;
equalities TARSKI, FUNCOP_1, AMI_2, SCMFSA_I, ORDINAL1;
expansions TARSKI;
theorems ZFMISC_1, FUNCT_2, TARSKI, FUNCOP_1, INT_1, CARD_3, FINSEQ_1,
FUNCT_4, RELAT_1, FUNCT_1, FINSEQ_2, PRE_CIRC, AMI_2, FUNCT_7, RELSET_1,
ORDINAL1, XBOOLE_0, XBOOLE_1, NUMBERS, PARTFUN1, AFINSQ_1, SCMFSA_I,
FUNCT_5, XTUPLE_0;
schemes BINOP_1;
begin
reserve x,y,z for set,
k for Nat;
notation
synonym SCM+FSA-Data-Loc for SCM-Data-Loc;
end;
definition
::$CD
func SCM+FSA-Memory -> set equals
SCM-Memory \/ SCM+FSA-Data*-Loc;
coherence;
end;
registration
cluster SCM+FSA-Memory -> non empty;
coherence;
end;
theorem Th1:
SCM-Memory c= SCM+FSA-Memory by XBOOLE_1:7;
definition
redefine func SCM+FSA-Data-Loc -> Subset of SCM+FSA-Memory; :: redefines SCM+FSA-Data-Loc (SCMFSA_1, synonym) → SCM-Data-Loc (SCM_INST, definition)
coherence
proof
SCM-Data-Loc c= SCM-Memory;
hence thesis by Th1,XBOOLE_1:1;
end;
end;
definition
redefine func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory; :: redefines SCM+FSA-Data*-Loc (SCMFSA_I, definition)
coherence by XBOOLE_1:7;
end;
registration
cluster SCM+FSA-Data*-Loc -> non empty;
coherence;
end;
reserve J,J1,K for Element of Segm 13,
a for Nat,
b,b1,b2,c,c1,c2 for Element of SCM+FSA-Data-Loc,
f,f1,f2 for Element of SCM+FSA-Data*-Loc;
definition
::$CD
func SCM+FSA-OK -> Function of SCM+FSA-Memory, Segm 3 equals
(SCM+FSA-Memory --> 2) +* SCM-OK;
coherence
proof
A1: rng(((SCM+FSA-Memory --> 2) +* SCM-OK)) c= 3
proof
rng(SCM+FSA-Memory --> 2) = {2} by FUNCOP_1:8;
then
A2: rng((SCM+FSA-Memory --> 2) +* SCM-OK) c= {2} \/ rng SCM-OK
by FUNCT_4:17;
rng SCM-OK c= Segm 2 by RELAT_1:def 19;
then {2} \/ rng SCM-OK c= 2 \/ {2} by XBOOLE_1:9;
then rng((SCM+FSA-Memory --> 2) +* SCM-OK)
c= 2 \/ {2} by A2;
then rng((SCM+FSA-Memory --> 2) +* SCM-OK)
c= succ 2;
hence thesis;
end;
dom((SCM+FSA-Memory --> 2) +* SCM-OK) = dom(SCM+FSA-Memory --> 2
) \/ dom SCM-OK by FUNCT_4:def 1
.= SCM+FSA-Memory \/ dom SCM-OK
.= SCM+FSA-Memory \/ SCM-Memory by FUNCT_2:def 1
.= SCM+FSA-Memory by XBOOLE_1:7,12;
then dom((SCM+FSA-Memory --> 2) +* SCM-OK)
= SCM+FSA-Memory
.= SCM+FSA-Memory;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
::$CT 3
theorem Th2:
NAT in SCM+FSA-Memory
proof
NAT in {NAT} by TARSKI:def 1;
then NAT in {NAT} \/ SCM-Data-Loc by XBOOLE_0:def 3;
then NAT in SCM-Memory;
hence thesis by XBOOLE_0:def 3;
end;
::$CT 2
theorem
SCM+FSA-Memory = {NAT} \/ SCM+FSA-Data-Loc \/ SCM+FSA-Data*-Loc;
definition
func SCM*-VAL -> ManySortedSet of Segm 3 equals
<%NAT,INT,INT*%>;
coherence;
end;
Lm1: SCM+FSA-Data*-Loc misses SCM-Memory
proof
assume SCM+FSA-Data*-Loc meets SCM-Memory;
then consider x being object such that
A1: x in SCM+FSA-Data*-Loc and
A2: x in SCM-Memory by XBOOLE_0:3;
A3: x in {NAT} \/ SCM-Data-Loc or x in NAT by A2;
x in NAT \/ [:{0},NAT:] \ {[0,0]} by A1,NUMBERS:def 4;
then
A4: x in NAT or x in [:{0},NAT:] by XBOOLE_0:def 3;
per cases by A3,XBOOLE_0:def 3;
suppose
A5: x in {NAT};
then ex y,z being object st x = [y,z] by A4,RELAT_1:def 1,TARSKI:def 1;
hence contradiction by A5,TARSKI:def 1;
end;
suppose
x in SCM-Data-Loc;
then
A6: ex k st x = [1,k] by AMI_2:23;
then consider y,z being object such that
A7: y in {0} and
z in NAT and
A8: x= [y,z] by A4,ZFMISC_1:84;
y = 0 by A7,TARSKI:def 1;
hence contradiction by A6,A8,XTUPLE_0:1;
end;
suppose
x in NAT;
hence contradiction by A1,XBOOLE_0:def 5;
end;
end;
Lm2: dom SCM-OK c= dom SCM+FSA-OK
proof
dom SCM+FSA-OK = dom(SCM+FSA-Memory --> 2) \/ dom SCM-OK by FUNCT_4:def 1;
hence dom SCM-OK c= dom SCM+FSA-OK by XBOOLE_1:7;
end;
Lm3: NAT in dom SCM+FSA-OK
proof
A1: NAT in dom SCM-OK by AMI_2:22,FUNCT_2:def 1;
dom SCM-OK c= dom SCM+FSA-OK by Lm2;
hence thesis by A1;
end;
Lm4:
SCM+FSA-OK.NAT = 0
proof
A1: NAT in dom SCM-OK by AMI_2:22,FUNCT_2:def 1;
thus SCM+FSA-OK.NAT = ((SCM+FSA-Memory --> 2) +* SCM-OK).NAT
.= SCM-OK.NAT by A1,FUNCT_4:13
.= 0 by AMI_2:22,def 4;
end;
theorem Th4:
(SCM*-VAL*SCM+FSA-OK).NAT = NAT
proof
A1: SCM+FSA-OK.NAT = 0 by Lm4;
thus (SCM*-VAL*SCM+FSA-OK).NAT
= SCM*-VAL.(SCM+FSA-OK.NAT) by Lm3,FUNCT_1:13
.= NAT by A1;
end;
Lm5:
SCM+FSA-OK.b = 1
proof
A1: b in SCM-Data-Loc;
then b in SCM-Memory;
then
A2: b in dom SCM-OK by FUNCT_2:def 1;
thus SCM+FSA-OK.b = ((SCM+FSA-Memory --> 2) +* SCM-OK).b
.= SCM-OK.b by A2,FUNCT_4:13
.= 1 by A1,AMI_2:def 4;
end;
theorem Th5:
(SCM*-VAL*SCM+FSA-OK).b = INT
proof
b in SCM-Data-Loc;
then b in SCM-Memory;
then
A1: b in dom SCM-OK by FUNCT_2:def 1;
A2: SCM+FSA-OK.b = 1 by Lm5;
A3: b in dom SCM+FSA-OK by A1,Lm2;
thus (SCM*-VAL*SCM+FSA-OK).b
= SCM*-VAL.(SCM+FSA-OK.b) by A3,FUNCT_1:13
.= SCM*-VAL.1 by A2
.= INT;
end;
Lm6:
SCM+FSA-OK.f = 2
proof
not f in SCM-Memory by Lm1,XBOOLE_0:3;
then
A1: not f in dom SCM-OK by FUNCT_2:def 1;
thus (SCM+FSA-OK).f = ((SCM+FSA-Memory --> 2) +* SCM-OK).f
.= (SCM+FSA-Memory --> 2).f by A1,FUNCT_4:11
.= 2;
end;
theorem Th6:
(SCM*-VAL*SCM+FSA-OK).f = INT*
proof
A1: (SCM+FSA-OK).f = 2 by Lm6;
f in SCM+FSA-Memory;
then
A2: f in dom SCM+FSA-OK by FUNCT_2:def 1;
thus (SCM*-VAL*SCM+FSA-OK).f
= SCM*-VAL.(SCM+FSA-OK.f) by A2,FUNCT_1:13
.= SCM*-VAL.2 by A1
.= INT*;
end;
Lm7: dom SCM+FSA-OK = SCM+FSA-Memory by PARTFUN1:def 2;
len <%NAT,INT,INT*%> = 3 by AFINSQ_1:39;
then rng SCM+FSA-OK c= dom SCM*-VAL by RELAT_1:def 19;
then
Lm8:
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm7,RELAT_1:27;
registration
cluster (SCM*-VAL*SCM+FSA-OK) -> non-empty;
coherence
proof set F = SCM*-VAL*SCM+FSA-OK;
let n be object;
assume
A1: n in dom F;
dom F = SCM+FSA-Memory by Lm8;
then n in SCM-Memory or n in SCM+FSA-Data*-Loc by A1,XBOOLE_0:def 3;
then per cases by AMI_2:26;
suppose n = NAT;
then (SCM*-VAL*SCM+FSA-OK).n = NAT by Th4;
hence F.n is non empty;
end;
suppose n in SCM-Data-Loc;
then (SCM*-VAL*SCM+FSA-OK).n = INT by Th5;
hence F.n is non empty;
end;
suppose n in SCM+FSA-Data*-Loc;
then (SCM*-VAL*SCM+FSA-OK).n = INT* by Th6;
hence F.n is non empty;
end;
end;
end;
definition
mode SCM+FSA-State is Element of product(SCM*-VAL*SCM+FSA-OK);
end;
::$CT 5
theorem Th7:
for s being SCM+FSA-State, I being Element of SCM-Instr holds s|
SCM-Memory is SCM-State
proof
let s be SCM+FSA-State, I be Element of SCM-Instr;
A1: dom(s|SCM-Memory) = dom s /\ SCM-Memory by RELAT_1:61
.= SCM+FSA-Memory /\ SCM-Memory by Lm8,CARD_3:9
.= SCM-Memory by XBOOLE_1:21;
A2: now
let x be object;
assume x in dom(SCM-VAL*SCM-OK);
then
A3: x in SCM-Memory by AMI_2:27;
then
A4: x in {NAT} \/ SCM-Data-Loc;
per cases by A4,XBOOLE_0:def 3;
suppose
A5: x in {NAT};
A6: (s|SCM-Memory).x = (s|SCM-Memory).x
.= s.x by A1,A3,FUNCT_1:47;
reconsider a = x as Element of SCM+FSA-Memory by A3,Th1;
A7: s.a in pi(product(SCM*-VAL*SCM+FSA-OK),a) by CARD_3:def 6;
A8: x = NAT by A5,TARSKI:def 1;
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then pi(product(SCM*-VAL*SCM+FSA-OK),a) = NAT by A8,Th4,CARD_3:12;
hence (s|SCM-Memory).x in (SCM-VAL*SCM-OK).x
by A8,A6,A7,AMI_2:6;
end;
suppose
A9: x in SCM-Data-Loc;
A10: (s|SCM-Memory).x = (s|SCM-Memory).x
.= s.x by A1,A3,FUNCT_1:47;
reconsider a = x as Element of SCM+FSA-Memory by A3,Th1;
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then
A11: pi(product(SCM*-VAL*SCM+FSA-OK),a)
= (SCM*-VAL*SCM+FSA-OK).a by CARD_3:12
.= INT by A9,Th5;
s.a in pi(product(SCM*-VAL*SCM+FSA-OK),a) by CARD_3:def 6;
hence (s|SCM-Memory).x in (SCM-VAL*SCM-OK).x
by A9,A10,A11,AMI_2:8;
end;
end;
dom(s|SCM-Memory) = dom(s|SCM-Memory)
.= SCM-Memory by A1
.= dom(SCM-VAL*SCM-OK) by AMI_2:27;
hence thesis by A2,CARD_3:9;
end;
theorem Th8:
for s being SCM+FSA-State, s1 being SCM-State
holds s +* s1 is SCM+FSA-State
proof
let s be SCM+FSA-State, s1 be SCM-State;
A1: dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then reconsider
f = (SCM*-VAL*SCM+FSA-OK) as non-empty ManySortedSet of SCM+FSA-Memory
by PARTFUN1:def 2;
A2: dom s1 = dom(SCM-VAL*SCM-OK) by CARD_3:9
.= SCM-Memory by AMI_2:27;
now
let x be set;
assume
A3: x in dom s1;
then
A4: x in {NAT} \/ SCM-Data-Loc by A2;
per cases by A4,XBOOLE_0:def 3;
suppose
A5: x in {NAT};
reconsider a = x as Element of SCM-Memory by A2,A3;
A6: s1.a in pi(product(SCM-VAL*SCM-OK),a) by CARD_3:def 6;
A7: x = NAT by A5,TARSKI:def 1;
dom(SCM-VAL*SCM-OK) = SCM-Memory by AMI_2:27;
then pi(product(SCM-VAL*SCM-OK),a) = (SCM-VAL*SCM-OK).a by CARD_3:12
.= NAT by A7,AMI_2:6;
hence s1.x in f.x by A5,A6,Th4,TARSKI:def 1;
end;
suppose
A8: x in SCM-Data-Loc;
reconsider a = x as Element of SCM-Memory by A2,A3;
A9: s1.a in pi(product(SCM-VAL*SCM-OK),a) by CARD_3:def 6;
dom(SCM-VAL*SCM-OK) = SCM-Memory by AMI_2:27;
then
A10: pi(product(SCM-VAL*SCM-OK),a) = (SCM-VAL*SCM-OK).a by CARD_3:12;
(SCM*-VAL*SCM+FSA-OK).x = INT by A8,Th5;
hence s1.x in f.x by A8,A10,A9,AMI_2:8;
end;
end;
then s +* s1 is SCM+FSA-State by A1,A2,PRE_CIRC:6,XBOOLE_1:7;
hence thesis;
end;
definition
let s be SCM+FSA-State, u be Nat;
func SCM+FSA-Chg(s,u) -> SCM+FSA-State equals
s +* (NAT .--> u);
coherence
proof
A1: now
let x be object;
assume
A2: x in dom(SCM*-VAL*SCM+FSA-OK);
per cases;
suppose
A3: x = NAT;
NAT in dom(NAT .--> u) by TARSKI:def 1;
then (s +* (NAT .--> u)).NAT = (NAT .--> u).NAT by FUNCT_4:13
.= u by FUNCOP_1:72;
hence (s +* (NAT .--> u)).x in (SCM*-VAL*SCM+FSA-OK).x
by A3,Th4,ORDINAL1:def 12;
end;
suppose
A4: x <> NAT;
not x in dom(NAT .--> u) by A4,TARSKI:def 1;
then (s +* (NAT .--> u)).x = s.x by FUNCT_4:11;
hence (s +* (NAT .--> u)).x in (SCM*-VAL*SCM+FSA-OK).x
by A2,CARD_3:9;
end;
end;
A5: dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then dom s = SCM+FSA-Memory by CARD_3:9;
then dom(s +* (NAT .--> u)) = SCM+FSA-Memory \/ dom(NAT .--> u) by
FUNCT_4:def 1
.= SCM+FSA-Memory \/ {NAT}
.= dom(SCM*-VAL*SCM+FSA-OK) by A5,Th2,ZFMISC_1:40;
hence thesis by A1,CARD_3:9;
end;
end;
definition
let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc, u be Integer;
func SCM+FSA-Chg(s,t,u) -> SCM+FSA-State equals
s +* (t .--> u);
coherence
proof
A1: now
let x be object;
assume
A2: x in dom(SCM*-VAL*SCM+FSA-OK);
per cases;
suppose
A3: x = t;
t in dom(t .--> u) by TARSKI:def 1;
then (s +* (t .--> u)).t = (t .--> u).t by FUNCT_4:13
.= u by FUNCOP_1:72;
then (s +* (t .--> u)).t in INT by INT_1:def 2;
hence (s +* (t .--> u)).x in (SCM*-VAL*SCM+FSA-OK).x by A3,Th5;
end;
suppose
A4: x <> t;
not x in dom(t .--> u) by A4,TARSKI:def 1;
then (s +* (t .--> u)).x = s.x by FUNCT_4:11;
hence (s +* (t .--> u)).x in (SCM*-VAL*SCM+FSA-OK).x by A2,CARD_3:9;
end;
end;
A5: dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then dom s = SCM+FSA-Memory by CARD_3:9;
then dom(s +* (t .--> u)) = SCM+FSA-Memory \/ dom(t .--> u) by
FUNCT_4:def 1
.= SCM+FSA-Memory \/ {t}
.= dom(SCM*-VAL*SCM+FSA-OK) by A5,ZFMISC_1:40;
hence thesis by A1,CARD_3:9;
end;
end;
definition
let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc, u be FinSequence
of INT;
func SCM+FSA-Chg(s,t,u) -> SCM+FSA-State equals
s +* (t .--> u);
coherence
proof
A1: now
let x be object;
assume
A2: x in dom(SCM*-VAL*SCM+FSA-OK);
per cases;
suppose
A3: x = t;
t in dom(t .--> u) by TARSKI:def 1;
then (s +* (t .--> u)).t = (t .--> u).t by FUNCT_4:13
.= u by FUNCOP_1:72;
then (s +* (t .--> u)).t in INT* by FINSEQ_1:def 11;
hence (s +* (t .--> u)).x in (SCM*-VAL*SCM+FSA-OK).x by A3,Th6;
end;
suppose
A4: x <> t;
not x in dom(t .--> u) by A4,TARSKI:def 1;
then (s +* (t .--> u)).x = s.x by FUNCT_4:11;
hence (s +* (t .--> u)).x in (SCM*-VAL*SCM+FSA-OK).x by A2,CARD_3:9;
end;
end;
A5: dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then dom s = SCM+FSA-Memory by CARD_3:9;
then dom(s +* (t .--> u)) = SCM+FSA-Memory \/ dom(t .--> u) by
FUNCT_4:def 1
.= SCM+FSA-Memory \/ {t}
.= dom(SCM*-VAL*SCM+FSA-OK) by A5,ZFMISC_1:40;
hence thesis by A1,CARD_3:9;
end;
end;
registration
let s be SCM+FSA-State, a be Element of SCM+FSA-Data-Loc;
cluster s.a -> integer;
coherence
proof
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then
A1: pi(product(SCM*-VAL*SCM+FSA-OK),a) = (SCM*-VAL*SCM+FSA-OK).a by CARD_3:12
.= INT by Th5;
s.a in pi(product(SCM*-VAL*SCM+FSA-OK),a) by CARD_3:def 6;
hence thesis by A1;
end;
end;
definition
let s be SCM+FSA-State, a be Element of SCM+FSA-Data*-Loc;
redefine func s.a -> FinSequence of INT; :: redefines . (FUNCT_1, definition)
coherence
proof
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then
A1: pi(product(SCM*-VAL*SCM+FSA-OK),a) = (SCM*-VAL*SCM+FSA-OK).a by CARD_3:12
.= INT* by Th6;
s.a in pi(product(SCM*-VAL*SCM+FSA-OK),a) by CARD_3:def 6;
hence thesis by A1,FINSEQ_1:def 11;
end;
end;
definition
::$CD 6
let s be SCM+FSA-State;
func IC(s) -> Element of NAT equals
s.NAT;
coherence
proof
reconsider z = NAT as Element of SCM+FSA-Memory by Th2;
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then pi(product(SCM*-VAL*SCM+FSA-OK),NAT) = (SCM*-VAL*SCM+FSA-OK).z
by CARD_3:12
.= NAT by Th4;
hence thesis by CARD_3:def 6;
end;
end;
definition
let x be Element of SCM+FSA-Instr, s be SCM+FSA-State;
func SCM+FSA-Exec-Res(x,s) -> SCM+FSA-State means
ex x9 being Element of SCM-Instr, s9 being SCM-State st
x = x9 & s9 = s|SCM-Memory &
it = s +* SCM-Exec-Res(x9,s9)
if x`1_3 <= 8,
ex i being Integer, k st
k = |.s.(x int_addr2).| & i = (s.(x coll_addr1))/.k &
it = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr1,i),IC s + 1)
if x`1_3 = 9,
ex f being FinSequence of INT,k st
k = |.s.(x int_addr2).| & f = s.(x coll_addr1)+*(k,s.(x int_addr1)) &
it = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr1,f),IC s + 1)
if x`1_3 = 10,
it =
SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr3,len(s.(x coll_addr2))),IC s + 1)
if x`1_3 = 11,
ex f being FinSequence of INT,k st
k = |.s.(x int_addr3).| & f = k |-> 0 &
it = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr2,f),IC s + 1)
if x`1_3 = 12,
ex i being Integer st
i = 1 &
it = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr,i),IC s + 1)
if x`1_3 = 13
otherwise it = s;
existence
proof
hereby
assume x`1_3 <= 8;
then reconsider x9 = x as Element of SCM-Instr by SCMFSA_I:2;
reconsider s9 = s|SCM-Memory as SCM-State by Th7;
reconsider s1 = s +* SCM-Exec-Res(x9,s9) as SCM+FSA-State by Th8;
take s1,x9,s9;
thus x = x9;
thus s9 = s|SCM-Memory;
thus s1 = s +* SCM-Exec-Res(x9,s9);
end;
hereby
reconsider k = |.s.(x int_addr2).| as Nat;
assume x`1_3 = 9;
reconsider i = (s.(x coll_addr1))/.k as Integer;
take s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr1,i),IC s + 1);
take i,k;
thus k = |.s.(x int_addr2).| & i = (s.(x coll_addr1))/.k & s1 =
SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr1,i),IC s + 1);
end;
hereby
reconsider k = |.s.(x int_addr2).| as Nat;
assume x`1_3 = 10;
per cases;
suppose
A1: k in dom( s.(x coll_addr1));
set f = s.(x coll_addr1) +* (k.-->s.(x int_addr1));
A2: {k} c= dom( s.(x coll_addr1)) by A1,ZFMISC_1:31;
dom f = dom(s.(x coll_addr1)) \/ dom((k.-->s.(x int_addr1))) by
FUNCT_4:def 1
.= dom(s.(x coll_addr1)) \/ {k}
.= dom(s.(x coll_addr1)) by A2,XBOOLE_1:12
.= Seg len(s.(x coll_addr1)) by FINSEQ_1:def 3;
then reconsider f as FinSequence by FINSEQ_1:def 2;
s.(x int_addr1) in INT & rng((k.-->s.(x int_addr1))) = {s.(x
int_addr1)} by FUNCOP_1:8,INT_1:def 2;
then
rng(s.(x coll_addr1)) c= INT & rng((k.-->s.(x int_addr1))) c= INT
by FINSEQ_1:def 4,ZFMISC_1:31;
then rng f c= rng(s.(x coll_addr1)) \/ rng((k.-->s.(x int_addr1))) &
rng(s.(x coll_addr1)) \/ rng((k.-->s.(x int_addr1))) c= INT by FUNCT_4:17
,XBOOLE_1:8;
then rng f c= INT;
then reconsider f as FinSequence of INT by FINSEQ_1:def 4;
take s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr1,f),IC s + 1);
take f,k;
thus k = |.s.(x int_addr2).|;
thus f = s.(x coll_addr1) +* (k,s.(x int_addr1)) by A1,FUNCT_7:def 3;
thus s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr1,f),IC s + 1);
end;
suppose
A3: not k in dom( s.(x coll_addr1));
reconsider f = s.(x coll_addr1) as FinSequence of INT;
take s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr1,f),IC s + 1);
take f,k;
thus k = |.s.(x int_addr2).|;
thus f = s.(x coll_addr1) +* (k,s.(x int_addr1)) by A3,FUNCT_7:def 3;
thus s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr1,f),IC s + 1);
end;
end;
thus x`1_3 = 11 implies ex s1 being SCM+FSA-State st s1 = SCM+FSA-Chg(
SCM+FSA-Chg(s,x int_addr3,len(s.(x coll_addr2))),IC s + 1);
hereby
reconsider k = |.s.(x int_addr3).| as Nat;
assume x`1_3 = 12;
0 in INT by INT_1:def 2;
then
A4: {0} c= INT by ZFMISC_1:31;
k |-> 0 = Seg k --> 0 by FINSEQ_2:def 2;
then rng(k |-> 0) c= {0} by FUNCOP_1:13;
then rng(k |-> 0) c= INT by A4;
then reconsider f = k |-> 0 as FinSequence of INT by FINSEQ_1:def 4;
take s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr2,f),IC s + 1);
take f,k;
thus k = |.s.(x int_addr3).| & f = k |-> 0 & s1 = SCM+FSA-Chg(
SCM+FSA-Chg(s,x coll_addr2,f),IC s + 1);
end;
hereby
assume x`1_3 = 13;
reconsider i = 1 as Integer;
take s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr,i),IC s + 1);
take i;
thus i = 1 & s1 = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr,i),IC s + 1);
end;
thus thesis;
end;
uniqueness;
consistency;
end;
definition
func SCM+FSA-Exec -> Action of SCM+FSA-Instr,
product(SCM*-VAL*SCM+FSA-OK) means
for x being Element of SCM+FSA-Instr, y being
SCM+FSA-State holds (it.x).y = SCM+FSA-Exec-Res(x,y);
existence
proof
deffunc U(Element of SCM+FSA-Instr, SCM+FSA-State) = SCM+FSA-Exec-Res($1,
$2);
consider f being
Function of [:SCM+FSA-Instr,product(SCM*-VAL*SCM+FSA-OK):],
product(SCM*-VAL*SCM+FSA-OK) such that
A1: for x being Element of SCM+FSA-Instr, y being SCM+FSA-State holds
f.(x,y) = U(x,y) from BINOP_1:sch 4;
take curry f;
let x be Element of SCM+FSA-Instr, y be SCM+FSA-State;
thus (curry f).x.y = f.(x,y) by FUNCT_5:69
.= SCM+FSA-Exec-Res(x,y) by A1;
end;
uniqueness
proof
let f,g be Function of SCM+FSA-Instr,
Funcs(product(SCM*-VAL*SCM+FSA-OK), product
(SCM*-VAL*SCM+FSA-OK)) such that
A2: for x being Element of SCM+FSA-Instr, y being SCM+FSA-State holds
(f.x qua Element of
Funcs(product(SCM*-VAL*SCM+FSA-OK), product(SCM*-VAL*SCM+FSA-OK))).y =
SCM+FSA-Exec-Res(x,y) and
A3: for x being Element of SCM+FSA-Instr, y being SCM+FSA-State holds
(g.x qua Element of
Funcs(product(SCM*-VAL*SCM+FSA-OK), product(SCM*-VAL*SCM+FSA-OK))).y =
SCM+FSA-Exec-Res(x,y);
now
let x be Element of SCM+FSA-Instr;
reconsider gx=g.x, fx=f.x
as Function of product(SCM*-VAL*SCM+FSA-OK), product
(SCM*-VAL*SCM+FSA-OK);
now
let y be SCM+FSA-State;
thus fx.y = SCM+FSA-Exec-Res(x,y) by A2
.= gx.y by A3;
end;
hence f.x = g.x by FUNCT_2:63;
end;
hence f = g by FUNCT_2:63;
end;
end;
theorem
for s being SCM+FSA-State, u being Nat holds SCM+FSA-Chg(s,
u).NAT = u
proof
let s be SCM+FSA-State, u be Nat;
NAT in dom(NAT .--> u) by TARSKI:def 1;
hence SCM+FSA-Chg(s,u).NAT = (NAT .--> u).NAT by FUNCT_4:13
.= u by FUNCOP_1:72;
end;
theorem
for s being SCM+FSA-State, u being Nat, mk being Element of
SCM+FSA-Data-Loc holds SCM+FSA-Chg(s,u).mk = s.mk
proof
let s be SCM+FSA-State, u be Nat, mk be Element of
SCM+FSA-Data-Loc;
(SCM*-VAL*SCM+FSA-OK).mk = INT & {NAT} = dom(NAT .--> u) by Th5;
then not mk in dom(NAT .--> u) by Th4,NUMBERS:7,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, u being Nat, p being Element of
SCM+FSA-Data*-Loc holds SCM+FSA-Chg(s,u).p = s.p
proof
let s be SCM+FSA-State, u be Nat,
mk be Element of SCM+FSA-Data*-Loc;
A2: SCM+FSA-OK.NAT = 0 by Lm4;
SCM+FSA-OK.mk = 2 by Lm6;
then NAT <> mk by A2;
then not mk in dom(NAT .--> u) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, u,v being Nat
holds SCM+FSA-Chg(s,u).v = s.v
proof
let s be SCM+FSA-State, u,v be Nat;
not v in dom(NAT .--> u) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data-Loc, u
being Integer holds SCM+FSA-Chg(s,t,u).NAT = s.NAT
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc, u be Integer;
(SCM*-VAL*SCM+FSA-OK).t = INT & {t} = dom(t .--> u) by Th5;
then not NAT in dom(t .--> u) by Th4,NUMBERS:7,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data-Loc, u
being Integer holds SCM+FSA-Chg(s,t,u).t = u
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc, u be Integer;
t in dom(t .--> u) by TARSKI:def 1;
hence SCM+FSA-Chg(s,t,u).t = (t .--> u).t by FUNCT_4:13
.= u by FUNCOP_1:72;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data-Loc, u
being Integer, mk being Element of SCM+FSA-Data-Loc st mk <> t holds
SCM+FSA-Chg(s,t,u).mk = s.mk
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc, u be Integer, mk
be Element of SCM+FSA-Data-Loc such that
A1: mk <> t;
not mk in dom(t .--> u) by A1,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data-Loc, u
being Integer, f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-Chg(s,t,u).f
= s.f
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc, u be Integer, mk
be Element of SCM+FSA-Data*-Loc;
(SCM*-VAL*SCM+FSA-OK).t = INT & (SCM*-VAL*SCM+FSA-OK).mk = INT* by Th5,Th6;
then not mk in dom(t .--> u) by FUNCT_7:16,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data*-Loc, u
being FinSequence of INT holds SCM+FSA-Chg(s,t,u).t = u
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc, u be FinSequence
of INT;
t in dom(t .--> u) by TARSKI:def 1;
hence SCM+FSA-Chg(s,t,u).t = (t .--> u).t by FUNCT_4:13
.= u by FUNCOP_1:72;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data*-Loc, u
being FinSequence of INT, mk being Element of SCM+FSA-Data*-Loc st mk <> t
holds SCM+FSA-Chg(s,t,u).mk = s.mk
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc, u be FinSequence
of INT, mk be Element of SCM+FSA-Data*-Loc such that
A1: mk <> t;
not mk in dom(t .--> u) by A1,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM+FSA-State, t being Element of SCM+FSA-Data*-Loc, u
being FinSequence of INT, a being Element of SCM+FSA-Data-Loc holds SCM+FSA-Chg
(s,t,u).a = s.a
proof
let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc, u be FinSequence
of INT, mk be Element of SCM+FSA-Data-Loc;
(SCM*-VAL*SCM+FSA-OK).t = INT* & (SCM*-VAL*SCM+FSA-OK).mk = INT by Th5,Th6;
then not mk in dom(t .--> u) by FUNCT_7:16,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
SCM+FSA-Data*-Loc misses SCM-Memory by Lm1;
::$CT
theorem
dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
theorem
for s being SCM+FSA-State holds dom s = SCM+FSA-Memory by Lm8,CARD_3:9;