:: Some Remarks on Simple Concrete Model of Computer
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993-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, STRUCT_0, AMI_1, AMI_2, FUNCT_7, XBOOLE_0,
RELAT_1, TARSKI, CAT_1, FSM_1, FUNCT_1, INT_1, NAT_1, GRAPHSP, FINSEQ_1,
CARD_1, ARYTM_3, ARYTM_1, FUNCOP_1, XXREAL_0, GLIB_000, FUNCT_4, AMI_3,
RECDEF_2, QUANTAL1, XCMPLX_0, MEMSTR_0, GOBRD13;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, ORDINAL1, XCMPLX_0,
RELAT_1, FUNCT_1, XXREAL_0, INT_1, FUNCOP_1, CARD_1, FUNCT_4, FUNCT_7,
FINSEQ_1, RECDEF_2, NUMBERS, MEASURE6, STRUCT_0, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, SCM_INST, AMI_2;
constructors DOMAIN_1, FINSEQ_4, CAT_2, AMI_2, RELSET_1, EXTPRO_1, FUNCT_7,
MEASURE6, XTUPLE_0, FUNCT_4;
registrations XBOOLE_0, SETFAM_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1, CARD_3,
AMI_2, FUNCT_1, FINSEQ_1, EXTPRO_1, FUNCT_4, MEMSTR_0, RELAT_1, COMPOS_0,
SCM_INST, XTUPLE_0, ORDINAL2, CARD_1, FACIRC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1;
equalities TARSKI, COMPOS_1, EXTPRO_1, FUNCOP_1, AMI_2, STRUCT_0, MEMSTR_0,
COMPOS_0, SCM_INST;
expansions EXTPRO_1, AMI_2, STRUCT_0, MEMSTR_0;
theorems TARSKI, ZFMISC_1, ENUMSET1, AMI_2, FUNCOP_1, FUNCT_4, CARD_3, INT_1,
ORDINAL1, XBOOLE_0, XBOOLE_1, XXREAL_0, NAT_1, RELAT_1, FUNCT_1,
PARTFUN1, SCM_INST, XTUPLE_0, SUBSET_1;
begin :: A small concrete machine
reserve i,j,k for Nat;
:: registration
:: cluster -> with_zero for non zero Nat;
:: coherence
:: proof let n be non zero Nat;
:: {} in n by ORDINAL3:8;
:: hence thesis;
:: end;
:: end;
reserve I,J,K for Element of Segm 9,
a,a1,a2 for Nat,
b,b1,b2,c,c1 for Element of SCM-Data-Loc;
reserve T for InsType of SCM-Instr,
I for Element of SCM-Instr;
registration let n be non zero Nat;
cluster Segm n -> with_zero;
coherence;
end;
definition
func SCM -> strict AMI-Struct over Segm 2 equals
AMI-Struct(#
SCM-Memory,In(NAT,SCM-Memory),SCM-Instr,SCM-OK,SCM-VAL,
SCM-Exec#);
coherence;
end;
registration
cluster SCM -> non empty;
coherence;
end;
Lm1: the_Values_of SCM = (the ValuesF of SCM)*(the Object-Kind of SCM)
.= SCM-VAL*SCM-OK;
registration
cluster SCM -> with_non-empty_values;
coherence;
end;
registration
cluster SCM -> IC-Ins-separated;
coherence
by AMI_2:22,SUBSET_1:def 8,AMI_2:6;
end;
registration
cluster Int-like for Object of SCM;
existence
proof
reconsider x = the Element of SCM-Data-Loc as Object of SCM;
take x;
thus thesis;
end;
end;
definition
mode Data-Location is Int-like Object of SCM;
end;
registration
let s be State of SCM, d be Data-Location;
cluster s.d -> integer;
coherence
proof
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider S = s as SCM-State by CARD_3:107;
S.D = s.d;
hence thesis;
end;
end;
reserve a,b,c for Data-Location,
loc for Nat,
I for Instruction of SCM;
definition
::$CD
let a,b;
func a := b -> Instruction of SCM equals
[ 1, {}, <*a, b*>];
correctness
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
1 in { 1,2,3,4,5} by ENUMSET1:def 3;
then [ 1, {}, <*mk, ml*>] in SCM-Instr by SCM_INST:4;
hence thesis;
end;
func AddTo(a,b) -> Instruction of SCM equals
[ 2, {}, <*a, b*>];
correctness
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
2 in { 1,2,3,4,5} by ENUMSET1:def 3;
then [ 2, {}, <*mk, ml*>] in SCM-Instr by SCM_INST:4;
hence thesis;
end;
func SubFrom(a,b) -> Instruction of SCM equals
[ 3, {}, <*a, b*>];
correctness
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
3 in { 1,2,3,4,5} by ENUMSET1:def 3;
then [ 3, {}, <*mk, ml*>] in SCM-Instr by SCM_INST:4;
hence thesis;
end;
func MultBy(a,b) -> Instruction of SCM equals
[ 4, {}, <*a, b*>];
correctness
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
4 in { 1,2,3,4,5} by ENUMSET1:def 3;
then [ 4, {}, <*mk, ml*>] in SCM-Instr by SCM_INST:4;
hence thesis;
end;
func Divide(a,b) -> Instruction of SCM equals
[ 5, {}, <*a, b*>];
correctness
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
5 in { 1,2,3,4,5} by ENUMSET1:def 3;
then [ 5, {}, <*mk, ml*>] in SCM-Instr by SCM_INST:4;
hence thesis;
end;
end;
definition
let loc;
func SCM-goto loc -> Instruction of SCM equals
[ 6, <*loc*>, {} ];
correctness
by SCM_INST:2;
let a;
func a=0_goto loc -> Instruction of SCM equals
[ 7, <*loc*>, <*a*>];
correctness
proof
reconsider a as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider loc as Nat;
7 in { 7,8 } by TARSKI:def 2;
then [ 7, <*loc*>, <*a*>] in SCM-Instr by SCM_INST:3;
hence thesis;
end;
func a>0_goto loc -> Instruction of SCM equals
[ 8, <*loc*>, <*a*>];
correctness
proof
reconsider a as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider loc as Nat;
8 in { 7,8 } by TARSKI:def 2;
then [ 8, <*loc*>, <*a*>] in SCM-Instr by SCM_INST:3;
hence thesis;
end;
end;
reserve s for State of SCM;
theorem Th1:
IC SCM = NAT by AMI_2:22,SUBSET_1:def 8;
begin :: Users guide
theorem Th2:
Exec(a:=b, s).IC SCM = IC s + 1 & Exec(a:=b, s).a = s.b & for c
st c <> a holds Exec(a:=b, s).c = s.c
proof
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = a:=b as Element of SCM-Instr;
set S1 = SCM-Chg(S, I address_1,S.(I address_2));
reconsider i = 1 as Element of Segm 9 by NAT_1:44;
A1: I = [ i, {}, <*mk, ml*>];
then
A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1,SCM_INST:5;
A4: Exec(a:=b, s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= (SCM-Chg(S1, IC S + 1)) by A1,AMI_2:def 14;
hence Exec(a:=b, s).IC SCM = IC s + 1 by Th1,AMI_2:11;
thus Exec(a:=b, s).a = S1.mk by A4,AMI_2:12
.= s.b by A2,A3,AMI_2:15;
let c;
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
assume
A5: c <> a;
thus Exec(a:=b, s).c = S1.mn by A4,AMI_2:12
.= s.c by A2,A5,AMI_2:16;
end;
theorem Th3:
Exec(AddTo(a,b), s).IC SCM = 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
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = AddTo(a,b) as Element of SCM-Instr;
set S1 = SCM-Chg(S, I address_1,S.(I address_1)+S.(I address_2));
reconsider i = 2 as Element of Segm 9 by NAT_1:44;
A1: I = [ i, {}, <*mk, ml*>];
then
A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1,SCM_INST:5;
A4: Exec(AddTo(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= (SCM-Chg(S1, IC S + 1)) by A1,AMI_2:def 14;
hence Exec(AddTo(a,b), s).IC SCM = IC s + 1 by Th1,AMI_2:11;
thus Exec(AddTo(a,b), s).a = S1.mk by A4,AMI_2:12
.= s.a + s.b by A2,A3,AMI_2:15;
let c;
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
assume
A5: c <> a;
thus Exec(AddTo(a,b), s).c = S1.mn by A4,AMI_2:12
.= s.c by A2,A5,AMI_2:16;
end;
theorem Th4:
Exec(SubFrom(a,b), s).IC SCM = 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
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = SubFrom(a,b) as Element of SCM-Instr;
set S1 = SCM-Chg(S, I address_1,S.(I address_1)-S.(I address_2));
reconsider i = 3 as Element of Segm 9 by NAT_1:44;
A1: I = [ i, {}, <*mk, ml*>];
then
A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1,SCM_INST:5;
A4: Exec(SubFrom(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= (SCM-Chg(S1, IC S + 1)) by A1,AMI_2:def 14;
hence Exec(SubFrom(a,b), s).IC SCM = IC s + 1 by Th1,AMI_2:11;
thus Exec(SubFrom(a,b), s).a = S1.mk by A4,AMI_2:12
.= s.a - s.b by A2,A3,AMI_2:15;
let c;
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
assume
A5: c <> a;
thus Exec(SubFrom(a,b), s).c = S1.mn by A4,AMI_2:12
.= s.c by A2,A5,AMI_2:16;
end;
theorem Th5:
Exec(MultBy(a,b), s).IC SCM = 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
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = MultBy(a,b) as Element of SCM-Instr;
set S1 = SCM-Chg(S, I address_1,S.(I address_1)*S.(I address_2));
reconsider i = 4 as Element of Segm 9 by NAT_1:44;
A1: I = [ i, {}, <*mk, ml*>];
then
A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1,SCM_INST:5;
A4: Exec(MultBy(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= (SCM-Chg(S1, IC S + 1)) by A1,AMI_2:def 14;
hence Exec(MultBy(a,b), s).IC SCM = IC s + 1 by Th1,AMI_2:11;
thus Exec(MultBy(a,b), s).a = S1.mk by A4,AMI_2:12
.= s.a * s.b by A2,A3,AMI_2:15;
let c;
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
assume
A5: c <> a;
thus Exec(MultBy(a,b), s).c = S1.mn by A4,AMI_2:12
.= s.c by A2,A5,AMI_2:16;
end;
theorem Th6:
Exec(Divide(a,b), s).IC SCM = IC s + 1 & (a <> b implies Exec(
Divide(a,b), s).a = s.a div s.b) & Exec(Divide(a,b), s).b = s.a mod s.b & for c
st c <> a & c <> b holds Exec(Divide(a,b), s).c = s.c
proof
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = Divide(a,b) as Element of SCM-Instr;
set S1 = SCM-Chg(S, I address_1,S.(I address_1) div S.(I address_2));
set S19 = SCM-Chg(S1, I address_2,S.(I address_1) mod S.(I address_2));
reconsider i = 5 as Element of Segm 9 by NAT_1:44;
A1: I = [ i, {}, <*mk, ml*>];
then
A2: I address_1 = mk by SCM_INST:5;
A3: Exec(Divide(a,b), s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= (SCM-Chg(S19, IC S + 1)) by A1,AMI_2:def 14;
hence Exec(Divide(a,b), s).IC SCM = IC s + 1 by Th1,AMI_2:11;
A4: I address_2 = ml by A1,SCM_INST:5;
hereby
assume
A5: a <> b;
thus Exec(Divide(a,b), s).a = S19.mk by A3,AMI_2:12
.= S1.mk by A4,A5,AMI_2:16
.= s.a div s.b by A2,A4,AMI_2:15;
end;
thus Exec(Divide(a,b), s).b = S19.ml by A3,AMI_2:12
.= s.a mod s.b by A2,A4,AMI_2:15;
let c;
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
assume that
A6: c <> a and
A7: c <> b;
thus Exec(Divide(a,b), s).c = S19.mn by A3,AMI_2:12
.= S1.mn by A4,A7,AMI_2:16
.= s.c by A2,A6,AMI_2:16;
end;
theorem
Exec(SCM-goto loc, s).IC SCM = loc & Exec(SCM-goto loc, s).c = s.c
proof
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider mj = loc as Element of NAT by ORDINAL1:def 12;
reconsider I = SCM-goto loc as Element of SCM-Instr;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 6 as Element of Segm 9 by NAT_1:44;
A1: I = [ i, <*mj*>, {} ];
A2: Exec(SCM-goto loc, s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= (SCM-Chg(S,I jump_address)) by AMI_2:def 14;
I jump_address = mj by A1,SCM_INST:6;
hence Exec(SCM-goto loc, s).IC SCM = loc by A2,Th1,AMI_2:11;
thus Exec(SCM-goto loc, s).c = S.mn by A2,AMI_2:12
.= s.c;
end;
theorem Th8:
(s.a = 0 implies Exec(a =0_goto loc, s).IC SCM = loc) & (s.a <>
0 implies Exec(a=0_goto loc, s).IC SCM = IC s + 1) & Exec(a=0_goto loc, s).c =
s.c
proof
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = a=0_goto loc as Element of SCM-Instr;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 7 as Element of Segm 9 by NAT_1:44;
reconsider a9 = a as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider mj = loc as Element of NAT by ORDINAL1:def 12;
A1: I = [ i, <*mj*>, <*a9*>];
A2: Exec(a=0_goto loc, s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= SCM-Chg(S,IFEQ(S.(I cond_address),0,I cjump_address,IC S + 1)) by A1,
AMI_2:def 14;
thus s.a = 0 implies Exec(a=0_goto loc, s).IC SCM = loc
proof
assume s.a = 0;
then
A3: S.(I cond_address)=0 by A1,SCM_INST:7;
thus Exec(a=0_goto loc, s).IC SCM = IFEQ(S.(I cond_address),0,I
cjump_address,IC S + 1) by A2,Th1,AMI_2:11
.= I cjump_address by A3,FUNCOP_1:def 8
.= loc by A1,SCM_INST:7;
end;
thus s.a <> 0 implies Exec(a=0_goto loc, s).IC SCM = IC s + 1
proof
assume s.a <> 0;
then
A4: S.(I cond_address) <> 0 by A1,SCM_INST:7;
thus Exec(a=0_goto loc, s).IC SCM = IFEQ(S.(I cond_address),0,I
cjump_address,IC S + 1) by A2,Th1,AMI_2:11
.= IC s + 1 by A4,Th1,FUNCOP_1:def 8;
end;
thus Exec(a=0_goto loc, s).c = S.mn by A2,AMI_2:12
.= s.c;
end;
theorem Th9:
(s.a > 0 implies Exec(a >0_goto loc, s).IC SCM = loc) & (s.a <=
0 implies Exec(a>0_goto loc, s).IC SCM = IC s + 1) & Exec(a>0_goto loc, s).c =
s.c
proof
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = a>0_goto loc as Element of SCM-Instr;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 8 as Element of Segm 9 by NAT_1:44;
reconsider a9 = a as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider mj = loc as Nat;
A1: I = [ i, <*mj*>, <*a9*>];
A2: Exec(a>0_goto loc, s) = SCM-Exec-Res(I,S) by AMI_2:def 15
.= SCM-Chg(S,IFGT(S.(I cond_address),0,I cjump_address,IC S + 1)) by A1,
AMI_2:def 14;
thus s.a > 0 implies Exec(a>0_goto loc, s).IC SCM = loc
proof
assume s.a > 0;
then
A3: S.(I cond_address) > 0 by A1,SCM_INST:7;
thus Exec(a>0_goto loc, s).IC SCM = IFGT(S.(I cond_address),0,I
cjump_address,IC S + 1) by A2,Th1,AMI_2:11
.= I cjump_address by A3,XXREAL_0:def 11
.= loc by A1,SCM_INST:7;
end;
thus s.a <= 0 implies Exec(a>0_goto loc, s).IC SCM = IC s + 1
proof
assume s.a <= 0;
then
A4: S.(I cond_address) <= 0 by A1,SCM_INST:7;
thus Exec(a>0_goto loc, s).IC SCM = IFGT(S.(I cond_address),0,I
cjump_address,IC S + 1) by A2,Th1,AMI_2:11
.= IC s + 1 by A4,Th1,XXREAL_0:def 11;
end;
thus Exec(a>0_goto loc, s).c = S.mn by A2,AMI_2:12
.= s.c;
end;
reserve Y,K,T for Element of Segm 9,
a1,a2,a3 for Nat,
b1,b2,c1,c2,
c3 for Element of SCM-Data-Loc;
Lm2: for I being Instruction of SCM st ex s st Exec(I,s).IC SCM = IC s + 1
holds I is non halting
proof
let I be Instruction of SCM;
given s such that
A1: Exec(I, s).IC SCM = IC s + 1;
assume I is halting;
then Exec(I,s).IC SCM = s.NAT by Th1;
hence contradiction by A1,Th1;
IC s = s.NAT by AMI_2:22,SUBSET_1:def 8;
then reconsider w = s.NAT as Nat;
end;
Lm3: for I being Instruction of SCM st I = [0,{},{}] holds I is halting
proof
let I be Instruction of SCM;
assume
A1: I = [0,{},{}];
then
A2: I`3_3 = {};
then
A3: ( not(ex mk, ml being Element of SCM-Data-Loc st I = [ 1, {}, <*mk, ml*>]))
&
not( ex mk, ml being Element of SCM-Data-Loc st I = [ 2, {}, <*mk, ml*>]);
A4: ( not(ex mk being Nat, ml being Element of SCM-Data-Loc st I
= [ 7, <*mk*>, <*ml*>]))& not(ex mk being Nat, ml being Element of
SCM-Data-Loc st I = [ 8, <*mk*>, <*ml*>]) by A2;
I`2_3 = {} by A1;
then
A5: ( not(ex mk, ml being Element of SCM-Data-Loc st
I = [ 5, {}, <*mk, ml*>]))
&
not( ex mk being Nat st I = [ 6, <*mk*>, {}])
by A2;
reconsider L = I as Element of SCM-Instr;
let s be State of SCM;
reconsider t = s as SCM-State by CARD_3:107;
A6: ( not(ex mk, ml being Element of SCM-Data-Loc st I = [ 3, {}, <*mk, ml*>]))
&
not( ex mk, ml being Element of SCM-Data-Loc st I = [ 4, {}, <*mk, ml*>])
by A2;
thus Exec(I,s) = SCM-Exec-Res(L,t) by AMI_2:def 15
.= s by A3,A6,A5,A4,AMI_2:def 14;
end;
Lm4: a := b is non halting
proof
set s =the State of SCM;
Exec(a:=b,s).IC SCM = IC s + 1 by Th2;
hence thesis by Lm2;
end;
Lm5: AddTo(a,b) is non halting
proof
set s =the State of SCM;
Exec(AddTo(a,b),s).IC SCM = IC s + 1 by Th3;
hence thesis by Lm2;
end;
Lm6: SubFrom(a,b) is non halting
proof
set s =the State of SCM;
Exec(SubFrom(a,b),s).IC SCM = IC s + 1 by Th4;
hence thesis by Lm2;
end;
Lm7: MultBy(a,b) is non halting
proof
set s =the State of SCM;
Exec(MultBy(a,b),s).IC SCM = IC s + 1 by Th5;
hence thesis by Lm2;
end;
Lm8: Divide(a,b) is non halting
proof
set s =the State of SCM;
Exec(Divide(a,b),s).IC SCM = IC s + 1 by Th6;
hence thesis by Lm2;
end;
Lm9: SCM-goto loc is non halting
proof
set f = the_Values_of SCM;
set s =the SCM-State;
assume
A1: SCM-goto loc is halting;
reconsider a3 = loc as Nat;
reconsider V = SCM-goto loc as Element of SCM-Instr;
set t = s +* (NAT.--> (a3+1));
A2: dom s = the carrier of SCM by AMI_2:28;
NAT in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then
A4: t.NAT = (NAT.--> (a3+1)).NAT by FUNCT_4:13
.= a3+1 by FUNCOP_1:72;
A5: for x being object st x in dom f holds t.x in f.x
proof
let x be object such that
A6: x in dom f;
per cases;
suppose
A7: x = NAT;
then f.x = NAT by AMI_2:6;
hence thesis by A4,A7,ORDINAL1:def 12;
end;
suppose
x <> NAT;
then not x in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A6,CARD_3:9;
end;
end;
A8: {NAT} c= SCM-Memory by AMI_2:22,ZFMISC_1:31;
A9: dom t = dom s \/ dom (NAT.--> (a3+1)) by FUNCT_4:def 1
.= SCM-Memory \/ dom (NAT.--> (a3+1)) by A2
.= SCM-Memory \/ {NAT}
.= SCM-Memory by A8,XBOOLE_1:12;
dom f = SCM-Memory by AMI_2:27;
then reconsider t as State of SCM by A9,A5,FUNCT_1:def 14,PARTFUN1:def 2
,RELAT_1:def 18;
reconsider w = t as SCM-State by CARD_3:107;
NAT in dom (NAT .--> loc) by TARSKI:def 1;
then
A10: (w +* (NAT .--> loc)).NAT = (NAT .--> loc).NAT by FUNCT_4:13
.= loc by FUNCOP_1:72;
6 is Element of Segm 9 by NAT_1:44;
then w +* (NAT .--> loc) = SCM-Chg(w,V jump_address) by SCM_INST:6
.= SCM-Exec-Res(V,w) by AMI_2:def 14
.= Exec(SCM-goto loc,t) by AMI_2:def 15
.= t by A1;
hence contradiction by A4,A10;
end;
Lm10: a=0_goto loc is non halting
proof
set f = the_Values_of SCM;
set s =the SCM-State;
reconsider V = a=0_goto loc as Element of SCM-Instr;
reconsider a3 = loc as Nat;
set t = s +* (NAT.--> (a3+1));
A1: {NAT} c= SCM-Memory by AMI_2:22,ZFMISC_1:31;
A2: dom s = the carrier of SCM by AMI_2:28;
A3: dom t = dom s \/ dom (NAT.--> (a3+1)) by FUNCT_4:def 1
.= SCM-Memory \/ dom (NAT.--> (a3+1)) by A2
.= SCM-Memory \/ {NAT}
.= SCM-Memory by A1,XBOOLE_1:12;
A4: 7 is Element of Segm 9 by NAT_1:44;
NAT in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then
A6: t.NAT = (NAT.--> (a3+1)).NAT by FUNCT_4:13
.= a3+1 by FUNCOP_1:72;
A7: for x being object st x in dom f holds t.x in f.x
proof
let x be object such that
A8: x in dom f;
per cases;
suppose
A9: x = NAT;
then f.x = NAT by AMI_2:6;
hence thesis by A6,A9,ORDINAL1:def 12;
end;
suppose
x <> NAT;
then not x in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A8,CARD_3:9;
end;
end;
dom f = SCM-Memory by AMI_2:27;
then reconsider t as State of SCM by A3,A7,FUNCT_1:def 14,PARTFUN1:def 2
,RELAT_1:def 18;
reconsider w = t as SCM-State by CARD_3:107;
NAT in dom (NAT .--> loc) by TARSKI:def 1;
then
A10: (w +* (NAT .--> loc)).NAT = (NAT .--> loc).NAT by FUNCT_4:13
.= loc by FUNCOP_1:72;
assume
A11: a=0_goto loc is halting;
A12: a is Element of SCM-Data-Loc by AMI_2:def 16;
per cases;
suppose
A13: w.(V cond_address) <> 0;
IC w = w.NAT;
then reconsider e = w.NAT as Nat;
IC t = IC w & t.a <> 0 by A4,A12,A13,AMI_2:22,SCM_INST:7,SUBSET_1:def 8;
then
A14: Exec(a=0_goto loc,t).IC SCM = e+1 by Th8;
Exec(a=0_goto loc,t).IC SCM = w.NAT by A11,Th1;
hence contradiction by A14;
end;
suppose
w.(V cond_address) = 0;
then IFEQ(w.(V cond_address),0,V cjump_address,IC w + 1) = V
cjump_address by FUNCOP_1:def 8;
then w +* (NAT .--> loc) = SCM-Chg(w,IFEQ(w.(V cond_address),0,V
cjump_address,IC w + 1)) by A4,A12,SCM_INST:7
.= SCM-Exec-Res(V,w) by A12,AMI_2:def 14
.= Exec(a=0_goto loc,t) by AMI_2:def 15
.= t by A11;
hence contradiction by A6,A10;
end;
end;
Lm11: a>0_goto loc is non halting
proof
set f = the_Values_of SCM;
set s =the SCM-State;
reconsider V = a>0_goto loc as Element of SCM-Instr;
reconsider a3 = loc as Nat;
set t = s +* (NAT.--> (a3+1));
A1: {NAT} c= SCM-Memory by AMI_2:22,ZFMISC_1:31;
A2: dom s = the carrier of SCM by AMI_2:28;
A3: dom t = dom s \/ dom (NAT.--> (a3+1)) by FUNCT_4:def 1
.= SCM-Memory \/ dom (NAT.--> (a3+1)) by A2
.= SCM-Memory \/ {NAT}
.= SCM-Memory by A1,XBOOLE_1:12;
A4: 8 is Element of Segm 9 by NAT_1:44;
NAT in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then
A6: t.NAT = (NAT.--> (a3+1)).NAT by FUNCT_4:13
.= a3 + 1 by FUNCOP_1:72;
A7: for x being object st x in dom f holds t.x in f.x
proof
let x be object such that
A8: x in dom f;
per cases;
suppose
A9: x = NAT;
then f.x = NAT by AMI_2:6;
hence thesis by A6,A9,ORDINAL1:def 12;
end;
suppose
x <> NAT;
then not x in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A8,CARD_3:9;
end;
end;
dom f = SCM-Memory by AMI_2:27;
then reconsider t as State of SCM by A3,A7,FUNCT_1:def 14,PARTFUN1:def 2
,RELAT_1:def 18;
reconsider w = t as SCM-State by CARD_3:107;
NAT in dom (NAT .--> loc) by TARSKI:def 1;
then
A10: (w +* (NAT .--> loc)).NAT = (NAT .--> loc).NAT by FUNCT_4:13
.= loc by FUNCOP_1:72;
assume
A11: a>0_goto loc is halting;
A12: a is Element of SCM-Data-Loc by AMI_2:def 16;
per cases;
suppose
A13: w.(V cond_address) <= 0;
IC w = w.NAT;
then reconsider e = w.NAT as Nat;
IC t = IC w & t.a <= 0 by A4,A12,A13,AMI_2:22,SCM_INST:7,SUBSET_1:def 8;
then
A14: Exec(a>0_goto loc,t).IC SCM = e+1 by Th9;
Exec(a>0_goto loc,t).IC SCM = w.NAT by A11,Th1;
hence contradiction by A14;
end;
suppose
w.(V cond_address) > 0;
then IFGT(w.(V cond_address),0,V cjump_address,IC w + 1) = V
cjump_address by XXREAL_0:def 11;
then w +* (NAT .--> loc) = SCM-Chg(w,IFGT(w.(V cond_address),0,V
cjump_address,IC w + 1)) by A4,A12,SCM_INST:7
.= SCM-Exec-Res(V,w) by A12,AMI_2:def 14
.= Exec(a>0_goto loc,t) by AMI_2:def 15
.= t by A11;
hence contradiction by A6,A10;
end;
end;
Lm12: for I being set holds I is Instruction of SCM 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 a,b st I = Divide(a,b)) or (ex loc st I =
SCM-goto loc) or (ex a,loc st I = a=0_goto loc) or ex a,loc
st I = a>0_goto loc
proof
let I be set;
thus I is Instruction of SCM implies 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 a,b st I = Divide(a,b)) or (ex loc st I = SCM-goto loc)
or (ex
a,loc st I = a=0_goto loc) or ex a,loc st I = a>0_goto loc
proof
assume I is Instruction of SCM;
then
I in { [SCM-Halt,{},{}] } \/ { [Y,<*a3*>,{}] : Y = 6 }
\/ { [K,<*a1*>, <*b1*>] :
K in { 7,8 } } or I in { [T,{},<*c2,c3*>] : T in { 1,2,3,4,5 } } by
XBOOLE_0:def 3;
then
A1: I in { [SCM-Halt,{},{}] } \/ { [Y,<*a3*>,{}] : Y = 6 } or
I in { [K,<*a1*>,<*b1*>]: K in { 7,8 } }
or I in { [T,{},<*c2,c3*>] : T in { 1,2,3,4,5 } } by XBOOLE_0:def 3;
per cases by A1,XBOOLE_0:def 3;
suppose
I in { [SCM-Halt,{},{}] };
hence thesis by TARSKI:def 1;
end;
suppose
I in { [Y,<*a3*>,{}] : Y = 6 };
then consider Y, a3 such that
A2: I = [Y,<*a3*>,{}] & Y = 6;
I = SCM-goto a3 by A2;
hence thesis;
end;
suppose
I in { [K,<*a1*>,<*b1*>]: K in { 7,8 } };
then consider K, a1, b1 such that
A3: I = [K,<*a1*>,<*b1*>]& K in { 7,8 };
reconsider a = b1 as Data-Location by AMI_2:def 16;
reconsider loc = a1 as Nat;
I = a=0_goto a1 or I = a>0_goto a1 by A3,TARSKI:def 2;
hence thesis;
end;
suppose
I in { [T,{},<*c2,c3*>] : T in { 1,2,3,4,5 } };
then consider T, c2, c3 such that
A4: I = [T,{},<*c2,c3*>] & T in { 1,2,3,4,5 };
reconsider a = c2, b = c3 as Data-Location by AMI_2:def 16;
I = a:=b or I = AddTo(a,b) or I = SubFrom(a,b) or I = MultBy(a,b)
or I = Divide(a,b) by A4,ENUMSET1:def 3;
hence thesis;
end;
end;
thus thesis by SCM_INST:1;
end;
Lm13: for W being Instruction of SCM st W is halting holds W = [0,{},{}]
proof
set I = [0,{},{}];
let W be Instruction of SCM such that
A1: W is halting;
assume
A2: I <> W;
per cases by Lm12;
suppose
W = [0,{},{}];
hence thesis by A2;
end;
suppose
ex a,b st W = a:=b;
hence thesis by A1,Lm4;
end;
suppose
ex a,b st W = AddTo(a,b);
hence thesis by A1,Lm5;
end;
suppose
ex a,b st W = SubFrom(a,b);
hence thesis by A1,Lm6;
end;
suppose
ex a,b st W = MultBy(a,b);
hence thesis by A1,Lm7;
end;
suppose
ex a,b st W = Divide(a,b);
hence thesis by A1,Lm8;
end;
suppose
ex loc st W = SCM-goto loc;
hence thesis by A1,Lm9;
end;
suppose
ex a,loc st W = a=0_goto loc;
hence thesis by A1,Lm10;
end;
suppose
ex a,loc st W = a>0_goto loc;
hence thesis by A1,Lm11;
end;
end;
registration
cluster SCM -> halting;
coherence
by Lm3;
end;
begin :: Small concrete model
definition
let k be Nat;
func dl.k -> Data-Location equals
[1,k];
coherence
proof
reconsider k as Element of NAT by ORDINAL1:def 12;
1 in {1} by TARSKI:def 1;
then [1,k] in SCM-Data-Loc by ZFMISC_1:87;
hence thesis by AMI_2:def 16;
end;
end;
reserve i,j,k for Nat;
theorem
i <> j implies dl.i <> dl.j by XTUPLE_0:1;
theorem Th11:
for l being Data-Location holds Values l = INT
by AMI_2:def 16,AMI_2:7;
definition
let la be Data-Location;
let a be Integer;
redefine func la .--> a -> PartState of SCM; :: redefines .--> (FUNCOP_1, definition)
coherence
proof
A1: a is Element of INT & Values la = INT by Th11,INT_1:def 2;
then reconsider a as Element of (the_Values_of SCM).la;
la .--> a is PartState of SCM by A1;
hence thesis;
end;
end;
definition
let la,lb be Data-Location;
let a, b be Integer;
redefine func (la,lb) --> (a,b) -> PartState of SCM; :: redefines --> (FUNCT_4, definition)
coherence
proof
A1: a is Element of INT & b is Element of INT by INT_1:def 2;
A2: Values la = INT & Values lb = INT by Th11;
then reconsider a as Element of Values la by A1;
reconsider b as Element of Values lb by A1,A2;
(la,lb) --> (a,b) is PartState of SCM;
hence thesis;
end;
end;
theorem
dl.i <> j;
theorem
IC SCM <> dl.i & IC SCM <> i
by Th1;
begin :: Halt Instruction
theorem
for I being Instruction of SCM st ex s st Exec(I,s).IC SCM = IC s + 1
holds I is non halting by Lm2;
theorem
for I being Instruction of SCM st I = [0,{},{}] holds I is halting by Lm3;
theorem
a := b is non halting by Lm4;
theorem
AddTo(a,b) is non halting by Lm5;
theorem
SubFrom(a,b) is non halting by Lm6;
theorem
MultBy(a,b) is non halting by Lm7;
theorem
Divide(a,b) is non halting by Lm8;
theorem
SCM-goto loc is non halting by Lm9;
theorem
a=0_goto loc is non halting by Lm10;
theorem
a>0_goto loc is non halting by Lm11;
theorem
for I being set holds I is Instruction of SCM 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 a,b st I = Divide(a,b)) or (ex loc st I =
SCM-goto loc) or (ex a,loc st I = a=0_goto loc) or
ex a,loc st I = a>0_goto loc by Lm12;
theorem
for I being Instruction of SCM st I is halting holds I = halt SCM by Lm13;
theorem
halt SCM = [0,{},{}];
theorem Th27:
Data-Locations SCM = SCM-Data-Loc
proof
SCM-Data-Loc misses {NAT} by AMI_2:20,ZFMISC_1:50;
then
A1: SCM-Data-Loc misses {NAT};
thus Data-Locations SCM = {NAT} \/ SCM-Data-Loc \ ({NAT}) by AMI_2:22
,SUBSET_1:def 8
.= SCM-Data-Loc \/ ({NAT}) \ ({NAT})
.= SCM-Data-Loc \ ({NAT}) by XBOOLE_1:40
.= SCM-Data-Loc by A1,XBOOLE_1:83;
end;
theorem
for d being Data-Location holds d in Data-Locations SCM by Th27,AMI_2:def 16;
theorem
for s being SCM-State holds s is State of SCM by Lm1;
theorem
for l being Element of SCM-Instr holds InsCode l <= 8 by SCM_INST:10;