:: The Basic Properties of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-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, CARD_1, XBOOLE_0, STRUCT_0, FUNCSDOM, AMI_3,
AMI_1, AMI_2, FUNCT_7, TARSKI, RELAT_1, FSM_1, FUNCT_1, CAT_1, FINSEQ_1,
GRAPHSP, FUNCT_2, CARD_3, ARYTM_3, ARYTM_1, SUPINF_2, FUNCOP_1, SCMRING1,
GLIB_000, FUNCT_4, RECDEF_2, GOBRD13, MEMSTR_0, NAT_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
ORDINAL1, CARD_1, FUNCT_2, RECDEF_2, XCMPLX_0, STRUCT_0, ALGSTR_0,
VECTSP_1, CARD_3, FINSEQ_1, NUMBERS, FUNCOP_1, FUNCT_4, FUNCT_7,
MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, SCMRINGI, SCMRING1;
constructors FINSEQ_4, REALSET1, AMI_3, SCMRING1, PRE_POLY, FUNCT_7, RELSET_1;
registrations ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_1, CARD_3, STRUCT_0, AMI_3,
SCMRING1, AMI_2, FUNCT_1, EXTPRO_1, SCMRINGI, SCM_INST, XTUPLE_0, NAT_1,
XCMPLX_0, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1, MEMSTR_0;
equalities XBOOLE_0, STRUCT_0, FUNCOP_1, SCMRING1, COMPOS_1, EXTPRO_1, AMI_2,
MEMSTR_0, COMPOS_0, SCMRINGI;
expansions EXTPRO_1, AMI_2, MEMSTR_0;
theorems AMI_2, AMI_3, CARD_3, FUNCOP_1, ENUMSET1, FUNCT_4, SCMRING1, TARSKI,
ZFMISC_1, XBOOLE_0, XBOOLE_1, NAT_1, FUNCT_1, PARTFUN1, RELAT_1,
SCMRINGI, SUBSET_1, ORDINAL1;
begin :: { \bf SCM } over ring
reserve I for Element of Segm 8,
S for non empty 1-sorted,
t for Element of S,
x for set,
k for Element of NAT;
reserve R for Ring, T for InsType of SCM-Instr R;
definition
let R be Ring;
func SCM R -> strict AMI-Struct over Segm 2 means
:Def1:
the carrier of it = SCM-Memory & the ZeroF of it = NAT &
the InstructionsF of it = SCM-Instr R &
the Object-Kind of it = SCM-OK &
the ValuesF of it = SCM-VAL R &
the Execution of it = SCM-Exec R;
existence
proof
take AMI-Struct (#SCM-Memory,In(NAT,SCM-Memory),
SCM-Instr R,
SCM-OK, SCM-VAL R, SCM-Exec R#);
thus thesis by AMI_2:22,SUBSET_1:def 8;
end;
uniqueness;
end;
registration
let R be Ring;
cluster SCM R -> non empty;
coherence by Def1;
end;
Lm1:
now let R be Ring;
thus the_Values_of SCM R = (the ValuesF of SCM R)*(the Object-Kind of SCM R)
.= (the ValuesF of SCM R)*SCM-OK by Def1
.= (SCM-VAL R)*SCM-OK by Def1;
end;
registration
let R be Ring;
cluster SCM R -> with_non-empty_values;
coherence
proof
the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
hence the_Values_of SCM R is non-empty;
end;
end;
Lm2: for R being Ring holds
(the carrier of SCM R) \ {NAT} = SCM-Data-Loc
proof let R be Ring;
A1: not NAT in SCM-Data-Loc by AMI_2:20;
thus (the carrier of SCM R) \ {NAT}
= SCM-Memory \ {NAT} by Def1
.= {NAT} \/ SCM-Data-Loc \ {NAT}
.= SCM-Data-Loc by A1,ZFMISC_1:117;
end;
registration
let R be Ring;
cluster Int-like for Object of SCM R;
existence
proof
the carrier of SCM R = SCM-Memory by Def1;
then reconsider x = the Element of SCM-Data-Loc as Object of SCM R;
take x;
thus thesis;
end;
end;
definition
let R be Ring;
mode Data-Location of R is Int-like Object of SCM R;
::$CD
end;
reserve R for Ring,
r for Element of R,
a, b, c, d1, d2 for Data-Location of R,
i1 for Nat;
theorem Th1:
x is Data-Location of R iff x in Data-Locations SCM
by Def1,AMI_2:def 16,AMI_3:27;
definition
let R be Ring, s be State of SCM R, a be Data-Location of R;
redefine func s.a -> Element of R; :: redefines . (FUNCT_1, definition)
coherence
proof
the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
then reconsider S = s as SCM-State of R by CARD_3:107;
a is Element of Data-Locations SCM by Th1;
then reconsider a as Element of SCM-Data-Loc by AMI_3:27;
S.a in the carrier of R;
hence thesis;
end;
end;
theorem
[0,{},{}] is Instruction of SCM R
proof
halt SCM R = [0,{},{}];
hence thesis;
end;
theorem Th3:
x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S
proof
reconsider d1,d2 as Element of SCM-Data-Loc by Th1,AMI_3:27;
x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S by SCMRINGI:8;
hence thesis;
end;
theorem Th4:
[5,{},<*d1,t*>] in SCM-Instr S
proof
reconsider d1 as Element of SCM-Data-Loc by Th1,AMI_3:27;
[5,{},<*d1,t*>] in SCM-Instr S by SCMRINGI:9;
hence thesis;
end;
theorem Th5:
[6,<*i1*>,{}] in SCM-Instr S by SCMRINGI:10;
theorem Th6:
[7,<*i1*>,<*d1*>] in SCM-Instr S
proof
reconsider d1 as Element of SCM-Data-Loc by Th1,AMI_3:27;
[7,<*i1*>,<*d1*>] in SCM-Instr S by SCMRINGI:11;
hence thesis;
end;
definition
let R be Ring, a, b be Data-Location of R;
func a := b -> Instruction of SCM R equals
[1,{},<*a,b*>];
coherence
proof
1 in { 1,2,3,4} by ENUMSET1:def 2;
then [1,{},<*a,b*>] in SCM-Instr R by Th3;
hence thesis by Def1;
end;
func AddTo(a,b) -> Instruction of SCM R equals
[2,{},<*a,b*>];
coherence
proof
2 in { 1,2,3,4} by ENUMSET1:def 2;
then [2,{},<*a,b*>] in SCM-Instr R by Th3;
hence thesis by Def1;
end;
func SubFrom(a,b) -> Instruction of SCM R equals
[3,{},<*a,b*>];
coherence
proof
3 in { 1,2,3,4} by ENUMSET1:def 2;
then [3,{},<*a,b*>] in SCM-Instr R by Th3;
hence thesis by Def1;
end;
func MultBy(a,b) -> Instruction of SCM R equals
[4,{},<*a,b*>];
coherence
proof
4 in { 1,2,3,4} by ENUMSET1:def 2;
then [4,{},<*a,b*>] in SCM-Instr R by Th3;
hence thesis by Def1;
end;
end;
definition
let R be Ring, a be Data-Location of R, r be Element of R;
func a := r -> Instruction of SCM R equals
[5,{},<*a,r*>];
coherence
proof
[5,{},<*a,r*>] in SCM-Instr R by Th4;
hence thesis by Def1;
end;
end;
definition
let R be Ring, l be Nat;
func goto(l,R) -> Instruction of SCM R equals
[6,<*l*>,{}];
coherence
proof
[6,<*l*>,{}] in SCM-Instr R by Th5;
hence thesis by Def1;
end;
end;
definition
let R be Ring, l be Nat, a be Data-Location
of R;
func a=0_goto l -> Instruction of SCM R equals
[7,<*l*>,<*a*>];
coherence
proof
[7,<*l*>,<*a*>] in SCM-Instr R by Th6;
hence thesis by Def1;
end;
end;
theorem Th7:
for I being set holds I is Instruction of SCM R iff I = [0,{},{}] or
(ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex a,b st I = SubFrom(a,
b)) or (ex a,b st I = MultBy(a,b)) or (ex i1 st I = goto(i1,R)) or
(ex a,i1 st I =
a=0_goto i1) or ex a,r st I = a:=r
proof
let J be set;
A1: the InstructionsF of SCM R = SCM-Instr R by Def1;
thus J is Instruction of SCM R implies J = [0,{},{}] or
(ex a,b st J = a:=b) or
(ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J =
MultBy(a,b)) or (ex i1 st J = goto(i1,R)) or
(ex a,i1 st J = a=0_goto i1) or ex a,
r st J = a:=r
proof
assume J is Instruction of SCM R;
then
J in { [0,{},{}] } \/ { [I,{},<*a,b*>]
where I is Element of Segm 8, a, b is
Element of Data-Locations SCM: I in { 1,2,3,4 } } \/ the set of all
[6,<*i*>,{}]
where i is Nat \/ the set of all [7,<*i*>,<*a*>]
where i is Nat, a is
Element of Data-Locations SCM or
J in the set of all [5,{},<*a,r*>] where a is
Element of Data-Locations SCM, r is Element of R
by A1,AMI_3:27,XBOOLE_0:def 3;
then
J in { [0,{},{}] } \/ { [I,{},<*a,b*>]
where I is Element of Segm 8, a, b is
Element of Data-Locations SCM: I in { 1,2,3,4 } } \/ the set of all
[6,<*i*>,{}]
where i is Nat or J in the set of all [7,<*i*>,<*a*>]
where i is Nat, a
is Element of Data-Locations SCM or J in the set of all [5,{},<*a,r*>]
where a
is Element of Data-Locations SCM, r is Element of R
by XBOOLE_0:def 3;
then
A2: J in { [0,{},{}] } \/ { [I,{},<*a,b*>]
where I is Element of Segm 8, a, b is
Element of Data-Locations SCM: I in { 1,2,3,4 } } or J in the set of all
[6,<*i*>,{}]
where i is Nat or J in the set of all [7,<*i*>,<*a*>]
where i is Nat, a is Element of Data-Locations SCM
or J in the set of all [5,{},<*a,r*>]
where a is Element of Data-Locations SCM, r is Element of R by XBOOLE_0:def 3;
per cases by A2,XBOOLE_0:def 3;
suppose
J in { [0,{},{}] };
hence thesis by TARSKI:def 1;
end;
suppose
J in the set of all [6,<*i*>,{}] where i is Nat;
then consider i being Nat such that
A3: J = [6,<*i*>,{}] and
not contradiction;
J = goto(i,R) by A3;
hence thesis;
end;
suppose
J in the set of all [7,<*i*>,<*a*>] where i is Nat, a is Element of
Data-Locations SCM;
then consider
i being Nat, a being Element of Data-Locations SCM such
that
A4: J = [7,<*i*>,<*a*>] and
not contradiction;
reconsider A = a as Data-Location of R by Th1,AMI_3:27;
J = A=0_goto i by A4;
hence thesis;
end;
suppose
J in the set of all
[5,{},<*a,r*>] where a is Element of Data-Locations SCM, r is
Element of R;
then consider
a being Element of Data-Locations SCM, r being Element of R such that
A5: J = [5,{},<*a,r*>] and
not contradiction;
reconsider A = a as Data-Location of R by Th1,AMI_3:27;
J = A:=r by A5;
hence thesis;
end;
suppose
J in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is
Element of Data-Locations SCM: I in { 1,2,3,4 } };
then consider
I being Element of Segm 8, a, b being Element of Data-Locations SCM
such that
A6: J = [I,{},<*a,b*>] & I in { 1,2,3,4 };
reconsider A = a, B = b as Data-Location of R by Th1,AMI_3:27;
J = A:=B or J = AddTo(A,B) or J = SubFrom(A,B) or J = MultBy(A,B)
by A6,ENUMSET1:def 2;
hence thesis;
end;
end;
thus thesis by A1,SCMRINGI:6;
end;
reserve s for State of SCM R;
registration
let R be non empty Ring;
cluster SCM R -> IC-Ins-separated;
coherence
proof
A1: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
IC SCM R = NAT by Def1;
then Values IC SCM R = NAT by A1,SCMRING1:2;
hence SCM R is IC-Ins-separated;
end;
end;
theorem
IC SCM R = NAT by Def1;
theorem
for S being SCM-State of R st S = s holds IC s = IC S by Def1;
theorem Th10:
for I being Instruction of SCM R for i being Element of
SCM-Instr R st i = I for S being SCM-State of R st S = s holds Exec(I,s) =
SCM-Exec-Res(i,S)
proof
let I be Instruction of SCM R, i be Element of SCM-Instr R such that
A1: i = I;
let S be SCM-State of R;
assume S = s;
hence Exec(I,s) = ((SCM-Exec R).i qua Element of
Funcs(product((SCM-VAL R)*SCM-OK),
product((SCM-VAL R)*SCM-OK))).S by A1,Def1
.= SCM-Exec-Res(i,S) by SCMRING1:def 15;
end;
begin :: Users guide
theorem Th11:
Exec(a := b, s).IC SCM R = IC s + 1 & Exec(a := b, s).a = s.b &
for c st c <> a holds Exec(a := b, s).c = s.c
proof
A1: a is Element of Data-Locations SCM by Th1;
A2: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A2,CARD_3:107;
reconsider I = a := b as Element of SCM-Instr R by Def1;
set S1 = SCM-Chg(S, I address_1,S.(I address_2));
reconsider i = 1 as Element of Segm 8 by NAT_1:44;
A3: IC s = IC S by Def1;
A4: b is Element of Data-Locations SCM by Th1;
A5: Exec(a := b, s) = SCM-Exec-Res(I,S) by Th10
.= (SCM-Chg(S1, IC S + 1)) by A1,A4,AMI_3:27,SCMRING1:def 14;
A6: I = [i,{},<*a,b*>];
then
A7: I address_1 = a by A1,A4,AMI_3:27,SCMRINGI:1;
A8: I address_2 = b by A6,A1,A4,AMI_3:27,SCMRINGI:1;
thus Exec(a := b, s).IC SCM R = Exec(a := b, s).NAT by Def1
.= IC s + 1 by A3,A5,SCMRING1:7;
thus Exec(a := b, s).a = S1.a by A1,A5,AMI_3:27,SCMRING1:8
.= s.b by A7,A8,SCMRING1:11;
let c;
assume
A9: c <> a;
A10: c is Element of Data-Locations SCM by Th1;
hence Exec(a := b, s).c = S1.c by A5,AMI_3:27,SCMRING1:8
.= s.c by A7,A9,A10,AMI_3:27,SCMRING1:12;
end;
theorem Th12:
Exec(AddTo(a,b), s).IC SCM R = IC s + 1 & Exec(AddTo(a,b), s).a
= s.a + s.b & for c st c <> a holds Exec(AddTo(a,b), s).c = s.c
proof
A1: a is Element of Data-Locations SCM by Th1;
A2: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A2,CARD_3:107;
reconsider I = AddTo(a,b) as Element of SCM-Instr R by Def1;
set S1 = SCM-Chg(S, I address_1,S.(I address_1)+S.(I address_2));
reconsider i = 2 as Element of Segm 8 by NAT_1:44;
A3: IC s = IC S by Def1;
A4: b is Element of Data-Locations SCM by Th1;
A5: Exec(AddTo(a,b), s) = SCM-Exec-Res(I,S) by Th10
.= (SCM-Chg(S1, IC S + 1)) by A1,A4,AMI_3:27,SCMRING1:def 14;
A6: I = [i,{},<*a,b*>];
then
A7: I address_1 = a by A1,A4,AMI_3:27,SCMRINGI:1;
A8: I address_2 = b by A6,A1,A4,AMI_3:27,SCMRINGI:1;
thus Exec(AddTo(a,b), s).IC SCM R = Exec(AddTo(a,b), s).NAT by Def1
.= IC s + 1 by A3,A5,SCMRING1:7;
thus Exec(AddTo(a,b), s).a = S1.a by A1,A5,AMI_3:27,SCMRING1:8
.= s.a + s.b by A7,A8,SCMRING1:11;
let c;
assume
A9: c <> a;
A10: c is Element of Data-Locations SCM by Th1;
hence Exec(AddTo(a,b), s).c = S1.c by A5,AMI_3:27,SCMRING1:8
.= s.c by A7,A9,A10,AMI_3:27,SCMRING1:12;
end;
theorem Th13:
Exec(SubFrom(a,b), s).IC SCM R = IC s + 1 & Exec(SubFrom(a,b),
s).a = s.a - s.b & for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c
proof
A1: a is Element of Data-Locations SCM by Th1;
A2: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A2,CARD_3:107;
reconsider I = SubFrom(a,b) as Element of SCM-Instr R by Def1;
set S1 = SCM-Chg(S, I address_1,S.(I address_1)-S.(I address_2));
reconsider i = 3 as Element of Segm 8 by NAT_1:44;
A3: IC s = IC S by Def1;
A4: b is Element of Data-Locations SCM by Th1;
A5: Exec(SubFrom(a,b), s) = SCM-Exec-Res(I,S) by Th10
.= (SCM-Chg(S1, IC S + 1)) by A1,A4,AMI_3:27,SCMRING1:def 14;
A6: I = [i,{},<*a,b*>];
then
A7: I address_1 = a by A1,A4,AMI_3:27,SCMRINGI:1;
A8: I address_2 = b by A6,A1,A4,AMI_3:27,SCMRINGI:1;
thus Exec(SubFrom(a,b), s).IC SCM R = Exec(SubFrom(a,b), s).NAT by Def1
.= IC s + 1 by A3,A5,SCMRING1:7;
thus Exec(SubFrom(a,b), s).a = S1.a by A1,A5,AMI_3:27,SCMRING1:8
.= s.a - s.b by A7,A8,SCMRING1:11;
let c;
assume
A9: c <> a;
A10: c is Element of Data-Locations SCM by Th1;
hence Exec(SubFrom(a,b), s).c = S1.c by A5,AMI_3:27,SCMRING1:8
.= s.c by A7,A9,A10,AMI_3:27,SCMRING1:12;
end;
theorem Th14:
Exec(MultBy(a,b), s).IC SCM R = IC s + 1 & Exec(MultBy(a,b), s)
.a = s.a * s.b & for c st c <> a holds Exec(MultBy(a,b), s).c = s.c
proof
A1: a is Element of Data-Locations SCM by Th1;
A2: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A2,CARD_3:107;
reconsider I = MultBy(a,b) as Element of SCM-Instr R by Def1;
set S1 = SCM-Chg(S, I address_1,S.(I address_1)*S.(I address_2));
reconsider i = 4 as Element of Segm 8 by NAT_1:44;
A3: IC s = IC S by Def1;
A4: b is Element of Data-Locations SCM by Th1;
A5: Exec(MultBy(a,b), s) = SCM-Exec-Res(I,S) by Th10
.= (SCM-Chg(S1, IC S + 1)) by A1,A4,AMI_3:27,SCMRING1:def 14;
A6: I = [i,{},<*a,b*>];
then
A7: I address_1 = a by A1,A4,AMI_3:27,SCMRINGI:1;
A8: I address_2 = b by A6,A1,A4,AMI_3:27,SCMRINGI:1;
thus Exec(MultBy(a,b), s).IC SCM R = Exec(MultBy(a,b), s).NAT by Def1
.= IC s + 1 by A3,A5,SCMRING1:7;
thus Exec(MultBy(a,b), s).a = S1.a by A1,A5,AMI_3:27,SCMRING1:8
.= s.a * s.b by A7,A8,SCMRING1:11;
let c;
assume
A9: c <> a;
A10: c is Element of Data-Locations SCM by Th1;
hence Exec(MultBy(a,b), s).c = S1.c by A5,AMI_3:27,SCMRING1:8
.= s.c by A7,A9,A10,AMI_3:27,SCMRING1:12;
end;
theorem
Exec(goto(i1,R), s).IC SCM R = i1 & Exec(goto(i1,R), s).c = s.c
proof
A1: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A1,CARD_3:107;
reconsider i = 6 as Element of Segm 8 by NAT_1:44;
reconsider I = goto(i1,R) as Element of SCM-Instr R by Def1;
I = [i,<*i1*>,{}];
then
A2: I jump_address = i1 by SCMRINGI:2;
A3: i1 in NAT by ORDINAL1:def 12;
A4: Exec(goto(i1,R), s) = SCM-Exec-Res(I,S) by Th10
.= (SCM-Chg(S,I jump_address)) by SCMRING1:def 14,A3;
thus Exec(goto(i1,R), s).IC SCM R = Exec(goto(i1,R), s).NAT by Def1
.= i1 by A4,A2,SCMRING1:7;
c is Element of Data-Locations SCM by Th1;
hence thesis by A4,AMI_3:27,SCMRING1:8;
end;
theorem Th16:
(s.a = 0.R implies Exec(a =0_goto i1, s).IC SCM R = i1) & (s.a
<> 0.R implies Exec(a =0_goto i1, s).IC SCM R = IC s + 1) & Exec(a =0_goto i1,
s).c = s.c
proof
A1: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A1,CARD_3:107;
reconsider I = a =0_goto i1 as Element of SCM-Instr R by Def1;
reconsider i = 7 as Element of Segm 8 by NAT_1:44;
A2: a is Element of Data-Locations SCM & i1 is Element of NAT
by Th1, ORDINAL1:def 12;
A3: Exec(a =0_goto i1, s) = SCM-Exec-Res(I,S) by Th10
.= SCM-Chg(S,IFEQ(S.(I cond_address),0.R,I cjump_address,IC S + 1)) by A2,
AMI_3:27,SCMRING1:def 14;
A4: I = [i,<*i1*>,<*a*>];
thus s.a = 0.R implies Exec(a =0_goto i1, s).IC SCM R = i1
proof
assume s.a = 0.R;
then
A5: S.(I cond_address)=0.R by A4,A2,AMI_3:27,SCMRINGI:3;
thus Exec(a =0_goto i1, s).IC SCM R = Exec(a =0_goto i1, s).NAT by Def1
.= IFEQ(S.(I cond_address),0.R,I cjump_address,IC S + 1) by A3,
SCMRING1:7
.= I cjump_address by A5,FUNCOP_1:def 8
.= i1 by A4,A2,AMI_3:27,SCMRINGI:3;
end;
A6: IC s = IC S by Def1;
thus s.a <> 0.R implies Exec(a =0_goto i1, s).IC SCM R = IC s + 1
proof
assume s.a <> 0.R;
then
A7: S.(I cond_address) <> 0.R by A4,A2,AMI_3:27,SCMRINGI:3;
thus Exec(a =0_goto i1, s).IC SCM R = Exec(a =0_goto i1, s).NAT by Def1
.= IFEQ(S.(I cond_address),0.R,I cjump_address,IC S + 1) by A3,
SCMRING1:7
.= IC s + 1 by A6,A7,FUNCOP_1:def 8;
end;
c is Element of Data-Locations SCM by Th1;
hence thesis by A3,AMI_3:27,SCMRING1:8;
end;
theorem Th17:
Exec(a := r, s).IC SCM R = IC s + 1 & Exec(a := r, s).a = r &
for c st c <> a holds Exec(a := r, s).c = s.c
proof
A1: a is Element of Data-Locations SCM by Th1;
A2: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider S = s as SCM-State of R by A2,CARD_3:107;
reconsider I = a := r as Element of SCM-Instr R by Def1;
set S1 = SCM-Chg(S, I const_address, I const_value);
reconsider i = 5 as Element of Segm 8 by NAT_1:44;
A3: IC s = IC S by Def1;
A4: I = [ i,{}, <*a, r*>];
then
A5: I const_address = a by A1,AMI_3:27,SCMRINGI:4;
A6: I const_value = r by A4,A1,AMI_3:27,SCMRINGI:4;
A7: Exec(a := r, s) = SCM-Exec-Res(I,S) by Th10
.= (SCM-Chg(S1, IC S + 1)) by A1,AMI_3:27,SCMRING1:def 14;
thus Exec(a := r, s).IC SCM R = Exec(a := r, s).NAT by Def1
.= IC s + 1 by A3,A7,SCMRING1:7;
thus Exec(a := r, s).a = S1.a by A1,A7,AMI_3:27,SCMRING1:8
.= r by A5,A6,SCMRING1:11;
let c;
assume
A8: c <> a;
A9: c is Element of Data-Locations SCM by Th1;
hence Exec(a := r, s).c = S1.c by A7,AMI_3:27,SCMRING1:8
.= s.c by A5,A8,A9,AMI_3:27,SCMRING1:12;
end;
begin :: Halt instruction
theorem Th18:
for I being Instruction of SCM R st ex s st Exec(I,s).IC SCM R =
IC s + 1 holds I is non halting
proof
let I be Instruction of SCM R;
given s such that
A1: Exec(I, s).IC SCM R = IC s + 1;
A2: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider t = s as SCM-State of R by A2,CARD_3:107;
IC t = t.NAT;
then reconsider w = t.NAT as Element of NAT;
A3: Exec(I,s).IC SCM R = w+1 by A1,Def1;
assume
A4: I is halting;
IC t = IC s by Def1;
then Exec(I,s).IC SCM R = t.NAT by A4;
hence contradiction by A3;
end;
theorem Th19:
for I being Instruction of SCM R st I = [0,{},{}] holds I is
halting
proof
let I be Instruction of SCM R such that
A1: I = [0,{},{}];
A2: I`3_3 = {} by A1;
then
A3: ( not(ex mk, ml being Element of Data-Locations SCM st
I = [ 1,{}, <*mk, ml*>]))&
not( ex mk, ml being Element of Data-Locations SCM st I =
[ 2, {}, <*mk, ml*>]);
A4: not(ex mk being Element of Data-Locations SCM, r being Element of R
st I = [ 5,{}, <*mk,r*>]) by A2;
I`2_3 = {} by A1;
then
A5: ( not(ex mk being Element of NAT st I = [ 6, <*mk*>,{}]))&
not(ex mk being
Element of NAT, ml being Element of Data-Locations SCM st
I = [ 7,<*mk*>,<*ml*>]);
reconsider L = I as Element of SCM-Instr R by A1,SCMRINGI:6;
let s be State of SCM R;
A6: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider t = s as SCM-State of R by A6,CARD_3:107;
A7: ( not(ex mk, ml being Element of Data-Locations SCM
st I = [ 3,{}, <*mk, ml*>]))&
not( ex mk, ml being Element of Data-Locations SCM
st I = [ 4,{}, <*mk, ml*>]) by A2;
thus Exec(I,s) = SCM-Exec-Res(L,t) by Th10
.= s by A3,A7,A5,A4,AMI_3:27,SCMRING1:def 14;
end;
Lm3: a := b is non halting
proof
set s =the State of SCM R;
Exec(a := b,s).IC SCM R = IC s + 1 by Th11;
hence thesis by Th18;
end;
Lm4: AddTo(a,b) is non halting
proof
set s =the State of SCM R;
Exec(AddTo(a,b),s).IC SCM R = IC s + 1 by Th12;
hence thesis by Th18;
end;
Lm5: SubFrom(a,b) is non halting
proof
set s =the State of SCM R;
Exec(SubFrom(a,b),s).IC SCM R = IC s + 1 by Th13;
hence thesis by Th18;
end;
Lm6: MultBy(a,b) is non halting
proof
set s =the State of SCM R;
Exec(MultBy(a,b),s).IC SCM R = IC s + 1 by Th14;
hence thesis by Th18;
end;
Lm7: goto(i1,R) is non halting
proof
reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;
set s =the SCM-State of R;
set t = s +* (NAT .--> (i1+1));
set f = the_Values_of SCM R;
A1: {NAT} c= SCM-Memory by AMI_2:22,ZFMISC_1:31;
A2: dom t = dom s \/ dom (NAT .--> (i1+1)) by FUNCT_4:def 1
.= SCM-Memory \/ dom (NAT .--> (i1+1)) by SCMRING1:19
.= SCM-Memory \/ {NAT}
.= SCM-Memory by A1,XBOOLE_1:12;
A3: f = (SCM-VAL R)*SCM-OK by Lm1;
NAT in dom (NAT .--> (i1+1)) by TARSKI:def 1;
then
A5: t.NAT = (NAT .--> (i1+1)).NAT by FUNCT_4:13
.= i5+1 by FUNCOP_1:72;
A6: dom t = the carrier of SCM R by A2,Def1
.= dom f by PARTFUN1:def 2;
A7: for x being object st x in dom t holds t.x in f.x
proof
let x be object such that
A8: x in dom t;
per cases;
suppose
A9: x = NAT;
then f.x = NAT by A3,SCMRING1:2;
hence thesis by A5,A9,ORDINAL1:def 12;
end;
suppose
x <> NAT;
then not x in dom (NAT .--> (i1+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A3,A8,A6,CARD_3:9;
end;
end;
A10: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
dom t = the carrier of SCM R by A2,Def1;
then reconsider t as PartState of SCM R by A7,FUNCT_1:def 14,RELAT_1:def 18;
dom t = the carrier of SCM R by A2,Def1;
then reconsider t as State of SCM R by PARTFUN1:def 2;
reconsider w = t as SCM-State of R by A10,CARD_3:107;
A11: i1 in NAT by ORDINAL1:def 12;
NAT in dom (NAT .--> i1) by TARSKI:def 1;
then
A12: (w +* (NAT .--> i1)).NAT = (NAT .--> i1).NAT by FUNCT_4:13
.= i1 by FUNCOP_1:72;
reconsider V = goto(i1,R) as Element of SCM-Instr R by Def1;
assume
A13: goto(i1,R) is halting;
A14: 6 is Element of Segm 8 by NAT_1:44;
w +* (NAT .--> i1) = SCM-Chg(w,i5)
.= SCM-Chg(w,V jump_address) by A14,SCMRINGI:2
.= SCM-Exec-Res(V,w) by SCMRING1:def 14,A11
.= Exec(goto(i1,R),t) by Th10
.= t by A13;
hence contradiction by A5,A12;
end;
Lm8: a =0_goto i1 is non halting
proof
reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;
set s =the SCM-State of R;
set t = s +* (NAT .--> (i1+1));
set f = the_Values_of SCM R;
reconsider V = a =0_goto i1 as Element of SCM-Instr R by Def1;
A1: {NAT} c= SCM-Memory by AMI_2:22,ZFMISC_1:31;
A2: dom t = dom s \/ dom (NAT .--> (i1+1)) by FUNCT_4:def 1
.= SCM-Memory \/ dom (NAT .--> (i1+1)) by SCMRING1:19
.= SCM-Memory \/ {NAT}
.= SCM-Memory by A1,XBOOLE_1:12;
A3: f = (SCM-VAL R)*SCM-OK by Lm1;
NAT in dom (NAT .--> (i1+1)) by TARSKI:def 1;
then
A5: t.NAT = (NAT .--> (i1+1)).NAT by FUNCT_4:13
.= i5+1 by FUNCOP_1:72;
A6: dom t = the carrier of SCM R by A2,Def1
.= dom f by PARTFUN1:def 2;
A7: for x being object st x in dom t holds t.x in f.x
proof
let x be object such that
A8: x in dom t;
per cases;
suppose
A9: x = NAT;
then f.x = NAT by A3,SCMRING1:2;
hence thesis by A5,A9,ORDINAL1:def 12;
end;
suppose
x <> NAT;
then not x in dom (NAT .--> (i1+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A3,A8,A6,CARD_3:9;
end;
end;
dom t = the carrier of SCM R by A2,Def1;
then reconsider t as PartState of SCM R by A7,FUNCT_1:def 14,RELAT_1:def 18;
dom t = the carrier of SCM R by A2,Def1;
then reconsider t as State of SCM R by PARTFUN1:def 2;
A10: the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
reconsider w = t as SCM-State of R by A10,CARD_3:107;
NAT in dom (NAT .--> i1) by TARSKI:def 1;
then
A11: (w +* (NAT .--> i1)).NAT = (NAT .--> i1).NAT by FUNCT_4:13
.= i1 by FUNCOP_1:72;
A12: 7 is Element of Segm 8 by NAT_1:44;
A13: a is Element of Data-Locations SCM by Th1;
assume
A14: a =0_goto i1 is halting;
A15: i1 in NAT by ORDINAL1:def 12;
per cases;
suppose
A16: w.(V cond_address) <> 0.R;
IC w = w.NAT;
then reconsider e = w.NAT as Element of NAT;
A17: IC t = IC w by Def1;
then
A18: Exec(a =0_goto i1,t).IC SCM R = w.NAT by A14;
a is Element of Data-Locations SCM by Th1;
then t.a <> 0.R by A12,A16,AMI_3:27,SCMRINGI:3,A15;
then Exec(a =0_goto i1,t).IC SCM R = e+1 by A17,Th16;
hence contradiction by A18;
end;
suppose
A19: w.(V cond_address) = 0.R;
w +* (NAT .--> i1) = SCM-Chg(w,i5)
.= SCM-Chg(w,V cjump_address) by A12,A13,AMI_3:27,SCMRINGI:3
.= SCM-Chg(w,IFEQ(w.(V cond_address),0.R,V cjump_address,IC w + 1))
by A19,FUNCOP_1:def 8
.= SCM-Exec-Res(V,w) by A13,AMI_3:27,SCMRING1:def 14,A15
.= Exec(a =0_goto i1,t) by Th10
.= t by A14;
hence contradiction by A5,A11;
end;
end;
Lm9: a := r is non halting
proof
set s =the State of SCM R;
Exec(a := r,s).IC SCM R = IC s + 1 by Th17;
hence thesis by Th18;
end;
registration
let R, a, b;
cluster a:=b -> non halting;
coherence by Lm3;
cluster AddTo(a,b) -> non halting;
coherence by Lm4;
cluster SubFrom(a,b) -> non halting;
coherence by Lm5;
cluster MultBy(a,b) -> non halting;
coherence by Lm6;
end;
registration
let R, i1;
cluster goto(i1,R) -> non halting;
coherence by Lm7;
end;
registration
let R, a, i1;
cluster a =0_goto i1 -> non halting;
coherence by Lm8;
end;
registration
let R, a, r;
cluster a:=r -> non halting;
coherence by Lm9;
end;
Lm10: for W being Instruction of SCM R st W is halting holds W = [0,{},{}]
proof
set I = [0,{},{}];
let W be Instruction of SCM R such that
A1: W is halting;
assume
A2: I <> W;
per cases by Th7;
suppose
W = [0,{},{}];
hence thesis by A2;
end;
suppose
ex a,b st W = a := b;
hence thesis by A1;
end;
suppose
ex a,b st W = AddTo(a,b);
hence thesis by A1;
end;
suppose
ex a,b st W = SubFrom(a,b);
hence thesis by A1;
end;
suppose
ex a,b st W = MultBy(a,b);
hence thesis by A1;
end;
suppose
ex i1 st W = goto(i1,R);
hence thesis by A1;
end;
suppose
ex a,i1 st W = a =0_goto i1;
hence thesis by A1;
end;
suppose
ex a,r st W = a := r;
hence thesis by A1;
end;
end;
registration
let R;
cluster SCM R -> halting;
coherence
by Th19;
end;
theorem
for I being Instruction of SCM R st I is halting holds I = halt
SCM R by Lm10;
theorem
halt SCM R = [0,{},{}];
theorem Th22:
Data-Locations SCM R = Data-Locations SCM
proof
Data-Locations SCM misses {NAT} by AMI_2:20,AMI_3:27,ZFMISC_1:50;
then
A1: Data-Locations SCM misses {NAT};
thus Data-Locations SCM R = SCM-Memory \ ({IC SCM R}) by Def1
.= SCM-Memory \ ({NAT}) by Def1
.= Data-Locations SCM \/ ({NAT}) \ ({NAT})
by AMI_3:27
.= Data-Locations SCM \ ({NAT}) by XBOOLE_1:40
.= Data-Locations SCM by A1,XBOOLE_1:83;
end;
theorem
x is Data-Location of R iff x in Data-Locations SCM R
proof
Data-Locations SCM R = Data-Locations SCM by Th22;
hence thesis by Th1;
end;
theorem
for R being Ring
holds the_Values_of SCM R = (SCM-VAL R)*SCM-OK by Lm1;
theorem
for R being Ring holds
(the carrier of SCM R) \ {NAT} = SCM-Data-Loc by Lm2;