Copyright (c) 2000 Association of Mizar Users
environ
vocabulary AMI_3, ORDINAL2, ARYTM, AMI_1, RELAT_1, BOOLE, FUNCT_1, FUNCT_4,
FINSET_1, TARSKI, CARD_1, ARYTM_1, FRAENKEL, SETFAM_1, CARD_3, PRALG_2,
FINSEQ_2, FINSEQ_1, CAT_1, FUNCOP_1, GOBOARD5, WAYBEL_0, AMISTD_1,
MCART_1, AMI_5, UNIALG_1, REALSET1, SGRAPH1, CARD_5, FRECHET, PRE_TOPC,
RELOC, FUNCT_7, ORDINAL1, SQUARE_1, SCMFSA6A, AMISTD_2, MEMBERED;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, REAL_1, SETFAM_1,
MEMBERED, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, FRAENKEL,
REALSET1, FUNCT_4, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, CARD_3, CARD_1,
FINSEQ_1, FINSEQ_2, CQC_LANG, BINARITH, FUNCT_7, STRUCT_0, AMI_1, AMI_3,
AMI_5, SCMFSA_4, PRE_CIRC, PRALG_2, AMISTD_1;
constructors AMI_5, BINARITH, DOMAIN_1, FUNCT_7, PRE_CIRC, AMISTD_1, REAL_1,
SCMFSA_4, WELLORD2, PRALG_2;
clusters AMI_1, AMISTD_1, XREAL_0, FINSEQ_1, FINSEQ_2, FINSET_1, FRAENKEL,
FUNCT_7, INT_1, PRELAMB, RELAT_1, RELSET_1, SUBSET_1, NAT_1, SCMFSA_4,
TEX_2, WAYBEL12, YELLOW13, XBOOLE_0, MEMBERED, PRE_CIRC, NUMBERS,
ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, RELAT_1, FUNCT_1, WELLORD2, FRAENKEL, REAL_1, FUNCT_7,
AMI_1, AMI_3, PRALG_2, YELLOW_8, AMISTD_1, XBOOLE_0;
theorems AMI_1, AMI_3, AMI_5, AXIOMS, BINARITH, CARD_1, CARD_2, AMISTD_1,
CQC_LANG, CQC_THE1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2,
FUNCT_4, FUNCOP_1, GOBOARD9, GRFUNC_1, INT_1, JORDAN4, KNASTER, MCART_1,
SCMFSA6A, CATALG_1, NAT_1, PRE_CIRC, REAL_1, REAL_2, REALSET1, RELAT_1,
RLVECT_1, SETFAM_1, SQUARE_1, TARSKI, YELLOW_8, ZFMISC_1, CARD_3,
PRALG_2, SCMFSA_7, ORDINAL2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes FUNCT_7, MATRIX_2, ZFREFLE1, XBOOLE_0;
begin :: Preliminaries
reserve k, m for natural number,
x, X for set,
N for with_non-empty_elements set;
Lm1:
for R being Relation st dom R <> {} holds R <> {}
proof
let R be Relation;
assume
A1: dom R <> {} & R = {};
dom {} = {};
hence thesis by A1;
end;
definition
let f be Function,
g be non empty Function;
cluster f +* g -> non empty;
coherence
proof
dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
hence thesis by Lm1;
end;
cluster g +* f -> non empty;
coherence
proof
dom (g+*f) = dom g \/ dom f by FUNCT_4:def 1;
hence thesis by Lm1;
end;
end;
definition
let f, g be finite Function;
cluster f +* g -> finite;
coherence
proof
dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
hence thesis by AMI_1:21;
end;
end;
theorem Th1:
for f, g being Function holds
dom f,dom g are_equipotent iff f,g are_equipotent
proof
let f, g be Function;
A1: Card f = Card dom f & Card g = Card dom g by PRE_CIRC:21;
hereby
assume dom f,dom g are_equipotent;
then Card dom f = Card dom g by CARD_1:21;
hence f,g are_equipotent by A1,CARD_1:21;
end;
assume f,g are_equipotent;
then Card f = Card g by CARD_1:21;
hence dom f,dom g are_equipotent by A1,CARD_1:21;
end;
theorem Th2:
for f, g being finite Function st dom f misses dom g
holds card (f +* g) = card f + card g
proof
let f, g be finite Function such that
A1: dom f misses dom g;
thus card (f +* g) = card dom (f +* g) by PRE_CIRC:21
.= card (dom f \/ dom g) by FUNCT_4:def 1
.= card dom f + card dom g by A1,CARD_2:53
.= card dom f + card g by PRE_CIRC:21
.= card f + card g by PRE_CIRC:21;
end;
definition
let f be Function,
A be set;
cluster f \ A -> Function-like Relation-like;
coherence by GRFUNC_1:38;
end;
theorem Th3:
for f, g being Function st x in dom f \ dom g holds (f \ g).x = f.x
proof
let f, g be Function such that
A1: x in dom f \ dom g;
A2: dom f \ dom g c= dom (f \ g) by RELAT_1:15;
f \ g c= f by XBOOLE_1:36;
hence (f \ g).x = f.x by A1,A2,GRFUNC_1:8;
end;
theorem Th4:
for F being non empty finite set holds card F - 1 = card F -' 1
proof
let F be non empty finite set;
card F <> 0 by CARD_2:59;
then card F >= 1 by RLVECT_1:99;
then card F - 1 >= 0 by SQUARE_1:12;
hence thesis by BINARITH:def 3;
end;
begin :: Product like sets
definition
let S be functional set;
func PA S -> Function means :Def1:
(for x being set holds x in dom it iff
for f being Function st f in S holds x in dom f) &
(for i being set st i in dom it holds it.i = pi(S,i)) if S is non empty
otherwise it = {};
existence
proof
thus S is non empty implies ex g being Function st
(for x being set holds x in dom g iff
for f being Function st f in S holds x in dom f) &
(for i being set st i in dom g holds g.i = pi(S,i))
proof
assume S is non empty;
then reconsider S1 = S as non empty functional set;
set D = {dom f where f is Element of S1: not contradiction};
defpred P[set,set] means $2 = pi(S,$1);
A1: for e being set st e in meet D ex u being set st P[e,u];
consider g being Function such that
A2: dom g = meet D and
A3: for e being set st e in meet D holds P[e,g.e] from NonUniqFuncEx(A1);
take g;
hereby
let x be set;
hereby
assume
A4: x in dom g;
let f be Function;
assume f in S;
then dom f in D;
hence x in dom f by A2,A4,SETFAM_1:def 1;
end;
assume
A5: for f being Function st f in S holds x in dom f;
consider f being Element of S1;
A6: dom f in D;
for Y being set holds Y in D implies x in Y
proof
let Y be set;
assume Y in D;
then ex f being Element of S1 st Y = dom f & not contradiction;
hence x in Y by A5;
end;
hence x in dom g by A2,A6,SETFAM_1:def 1;
end;
thus thesis by A2,A3;
end;
thus thesis;
end;
uniqueness
proof
let A, B be Function;
thus S is non empty &
(for x being set holds x in dom A iff
for f being Function st f in S holds x in dom f) &
(for i being set st i in dom A holds A.i = pi(S,i)) &
(for x being set holds x in dom B iff
for f being Function st f in S holds x in dom f) &
(for i being set st i in dom B holds B.i = pi(S,i))
implies A = B
proof
defpred _P[set] means for f being Function st f in S holds $1 in dom f;
assume that
S is non empty and
A7: for x being set holds x in dom A iff _P[x] and
A8: for i being set st i in dom A holds A.i = pi(S,i) and
A9: for x being set holds x in dom B iff _P[x] and
A10: for i being set st i in dom B holds B.i = pi(S,i);
A11: dom A = dom B from Extensionality(A7,A9);
now
let i be set;
assume
A12: i in dom A;
hence A.i = pi(S,i) by A8
.= B.i by A10,A11,A12;
end;
hence A = B by A11,FUNCT_1:9;
end;
thus thesis;
end;
consistency;
end;
theorem
for S being non empty functional set holds
dom PA S = meet {dom f where f is Element of S: not contradiction}
proof
let S be non empty functional set;
set D = {dom f where f is Element of S: not contradiction};
hereby
let x be set;
assume
A1: x in dom PA S;
consider f being Element of S;
A2: dom f in D;
for Y being set holds Y in D implies x in Y
proof
let Y be set;
assume Y in D;
then ex f being Element of S st Y = dom f & not contradiction;
hence x in Y by A1,Def1;
end;
hence x in meet D by A2,SETFAM_1:def 1;
end;
let x be set;
assume
A3: x in meet D;
for f being Function st f in S holds x in dom f
proof
let f be Function;
assume f in S;
then dom f in D;
hence x in dom f by A3,SETFAM_1:def 1;
end;
hence thesis by Def1;
end;
theorem
for S being non empty functional set,
i being set st i in dom PA S holds
(PA S).i = {f.i where f is Element of S: not contradiction}
proof
let S be non empty functional set,
i be set;
assume
A1: i in dom PA S;
hereby
let x be set;
assume x in (PA S).i;
then x in pi(S,i) by A1,Def1;
then ex f being Function st f in S & x = f.i by CARD_3:def 6;
hence x in {f.i where f is Element of S: not contradiction};
end;
let x be set;
assume x in {f.i where f is Element of S: not contradiction};
then ex f being Element of S st x = f.i & not contradiction;
then x in pi(S,i) by CARD_3:def 6;
hence thesis by A1,Def1;
end;
definition
let S be set;
attr S is product-like means :Def2:
ex f being Function st S = product f;
end;
definition
let f be Function;
cluster product f -> product-like;
coherence by Def2;
end;
definition
cluster product-like -> functional with_common_domain set;
coherence
proof
let S be set;
given f being Function such that
A1: S = product f;
thus S is functional by A1;
let h, g be Function such that
A2: h in S and
A3: g in S;
thus dom h = dom f by A1,A2,CARD_3:18
.= dom g by A1,A3,CARD_3:18;
end;
end;
definition
cluster product-like non empty set;
existence
proof
consider B being with_non-empty_elements set,
f being Function of 0,B;
take product f;
thus thesis;
end;
end;
theorem Th7:
for S being functional with_common_domain set holds dom PA S = DOM S
proof
let S be functional with_common_domain set;
per cases;
suppose
A1: S is empty;
hence dom PA S = {} by Def1,RELAT_1:60
.= DOM S by A1,PRALG_2:def 2;
suppose
A2: S is non empty;
consider f being Element of S;
hereby
let x be set;
assume x in dom PA S;
then x in dom f by A2,Def1;
hence x in DOM S by A2,PRALG_2:def 2;
end;
let x be set;
assume
x in DOM S;
then for f being Function st f in S holds x in dom f by PRALG_2:def 2;
hence thesis by A2,Def1;
end;
theorem
for S being functional set, i being set st i in dom PA S
holds (PA S).i = pi(S,i)
proof
let S be functional set,
i be set;
per cases;
suppose S = {};
then dom PA S = dom {} by Def1;
hence thesis;
suppose
A1: S <> {};
assume i in dom PA S;
hence thesis by A1,Def1;
end;
theorem Th9:
for S being functional with_common_domain set holds S c= product PA S
proof
let S be functional with_common_domain set;
let f be set;
assume
A1: f in S;
then reconsider f as Element of S;
A2: dom f = DOM S by A1,PRALG_2:def 2
.= dom PA S by Th7;
for i being set st i in dom PA S holds f.i in (PA S).i
proof
let i be set;
assume i in dom PA S;
then (PA S).i = pi(S,i) by A1,Def1;
hence f.i in (PA S).i by A1,CARD_3:def 6;
end;
hence thesis by A2,CARD_3:18;
end;
theorem Th10:
for S being non empty product-like set holds S = product PA S
proof
let S be non empty product-like set;
thus S c= product PA S by Th9;
let x be set;
assume x in product PA S;
then consider g being Function such that
A1: x = g and
A2: dom g = dom PA S and
A3: for z being set st z in dom PA S holds g.z in (PA S).z by CARD_3:def 5;
consider p being Function such that
A4: S = product p by Def2;
consider s being Element of S;
A5: dom g = DOM S by A2,Th7
.= dom s by PRALG_2:def 2
.= dom p by A4,CARD_3:18;
for z being set st z in dom p holds g.z in p.z
proof
let z be set;
assume
A6: z in dom p;
then g.z in (PA S).z by A2,A3,A5;
then g.z in pi(S,z) by A2,A5,A6,Def1;
then ex f being Function st f in S & g.z = f.z by CARD_3:def 6;
hence g.z in p.z by A4,A6,CARD_3:18;
end;
hence x in S by A1,A4,A5,CARD_3:18;
end;
definition
let D be set;
cluster -> functional FinSequenceSet of D;
coherence
proof
let f be FinSequenceSet of D;
let x be set;
thus x in f implies x is Function by FINSEQ_2:def 3;
end;
end;
definition
let i be Nat, D be set;
cluster i-tuples_on D -> with_common_domain;
coherence
proof
set S = i-tuples_on D;
let f, g be Function such that
A1: f in S & g in S;
S = { s where s is Element of D*: len s = i } by FINSEQ_2:def 4;
then (ex s being Element of D* st f = s & len s = i) &
(ex s being Element of D* st g = s & len s = i) by A1;
hence dom f = dom g by FINSEQ_3:31;
end;
end;
definition
let i be Nat, D be set;
cluster i-tuples_on D -> product-like;
coherence
proof
set S = i-tuples_on D;
per cases;
suppose D = {} & i = 0;
then S = { <*>D } by FINSEQ_2:112
.= {{}};
hence thesis by CARD_3:19;
suppose D = {} & i <> 0;
then A1: S = {} by CATALG_1:7;
take f = 0 .--> {};
rng f = {{}} by CQC_LANG:5;
then {} in rng f by TARSKI:def 1;
hence thesis by A1,CARD_3:37;
suppose D <> {};
then reconsider D as non empty set;
set S = i-tuples_on D;
take PA S;
S = product PA S
proof
thus S c= product PA S by Th9;
let x be set;
assume x in product PA S;
then consider g being Function such that
A2: x = g and
A3: dom g = dom PA S and
A4: for z being set st z in dom PA S holds g.z in (PA S).z by CARD_3:def 5;
A5: S = { s where s is Element of D*: len s = i } by FINSEQ_2:def 4;
consider s being Element of S;
s in S;
then consider t being Element of D* such that
A6: s = t and
A7: len t = i by A5;
A8: dom g = DOM S by A3,Th7
.= dom s by PRALG_2:def 2;
dom s = Seg len t by A6,FINSEQ_1:def 3;
then A9: g is FinSequence by A8,FINSEQ_1:def 2;
rng g c= D
proof
let y be set;
assume y in rng g;
then consider a being set such that
A10: a in dom g and
A11: g.a = y by FUNCT_1:def 5;
g.a in (PA S).a by A3,A4,A10;
then g.a in pi(S,a) by A3,A10,Def1;
then consider f being Function such that
A12: f in S and
A13: g.a = f.a by CARD_3:def 6;
consider w being Element of D* such that
A14: f = w and
len w = i by A5,A12;
A15: rng w c= D by FINSEQ_1:def 4;
dom g = dom w by A8,A12,A14,PRALG_2:def 1;
then w.a in rng w by A10,FUNCT_1:def 5;
hence y in D by A11,A13,A14,A15;
end;
then reconsider g as FinSequence of D by A9,FINSEQ_1:def 4;
A16: g in D* by FINSEQ_1:def 11;
len g = i by A6,A7,A8,FINSEQ_3:31;
hence thesis by A2,A5,A16;
end;
hence thesis;
end;
end;
Lm2:
for a, b being Real holds a - 1 + (b - 1) = a + b - 2
proof
let a, b be Real;
thus a - 1 + (b - 1) = a + (b - 1) - 1 by XCMPLX_1:29
.= a + b - 1 - 1 by XCMPLX_1:29
.= a + b - (1 + 1) by XCMPLX_1:36
.= a + b - 2;
end;
Lm3:
-1 < k
proof
-1 < 0 & 0 <= k by NAT_1:18;
hence thesis;
end;
Lm4:
for a, b, c being Nat st 1 <= a & 2 <= b holds
k < a - 1 or a <= k & k <= a + b - 3 or k = a + b - 2 or
a + b - 2 < k or k = a - 1
proof
let a, b, c be Nat such that
A1: 1 <= a and
A2: 2 <= b and
A3: a - 1 <= k and
A4: (a > k or k > a + b - 3) and
A5: k <> a + b - 2 and
A6: k <= a + b - 2;
A7: a - 1 is Nat by A1,INT_1:18;
now per cases by A4;
case k < a;
then k < a - 1 + 1 by XCMPLX_1:27;
hence k <= a - 1 by A7,NAT_1:38;
case
A8: a + b - 3 < k;
1 + 2 <= a + b by A1,A2,REAL_1:55;
then A9: a + b - 3 is Nat by INT_1:18;
k < a + b - (3 - 1) by A5,A6,REAL_1:def 5;
then k < a + b - 3 + 1 by XCMPLX_1:37;
hence k <= a - 1 by A8,A9,NAT_1:38;
end;
hence a - 1 = k by A3,AXIOMS:21;
end;
begin :: Properties of AMI-Struct
theorem Th11:
for N be set,
S being AMI-Struct over N,
F being FinPartState of S holds F \ X is FinPartState of S
proof
let N be set,
S be AMI-Struct over N,
F be FinPartState of S;
F \ X c= F by XBOOLE_1:36;
then F \ X in sproduct the Object-Kind of S by AMI_1:40;
hence F \ X is FinPartState of S by AMI_1:def 24;
end;
theorem Th12:
for S being IC-Ins-separated definite (non empty non void AMI-Struct over N),
F being programmed FinPartState of S
holds F \ X is programmed FinPartState of S
proof
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
F be programmed FinPartState of S;
reconsider G = F \ X as FinPartState of S by Th11;
per cases;
suppose G is empty;
then reconsider H = G as empty FinPartState of S;
H is programmed;
hence thesis;
suppose G is non empty;
then reconsider G as non empty FinPartState of S;
G is programmed
proof
G c= F by XBOOLE_1:36;
then A1: dom G c= dom F by GRFUNC_1:8;
dom F c= the Instruction-Locations of S by AMI_3:def 13;
hence dom G c= the Instruction-Locations of S by A1,XBOOLE_1:1;
end;
hence thesis;
end;
definition
let N be with_non-empty_elements set,
S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
i1, i2 be Instruction-Location of S,
I1, I2 be Element of the Instructions of S;
redefine func (i1,i2) --> (I1,I2) -> FinPartState of S;
coherence
proof
ObjectKind i1 = the Instructions of S &
ObjectKind i2 = the Instructions of S by AMI_1:def 14;
hence thesis by AMI_1:58;
end;
end;
definition
let N be with_non-empty_elements set;
let S be halting (non void AMI-Struct over N);
cluster halting Instruction of S;
existence
proof
take halt S;
thus thesis;
end;
end;
theorem Th13:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being lower programmed FinPartState of S,
G being programmed FinPartState of S st dom F = dom G
holds G is lower
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower programmed FinPartState of S,
G be programmed FinPartState of S;
assume dom F = dom G;
hence for l being Instruction-Location of S st l in dom G
holds for m being Instruction-Location of S st m <= l holds m in dom G
by AMISTD_1:def 20;
end;
theorem Th14:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being lower programmed FinPartState of S,
f being Instruction-Location of S st f in dom F
holds locnum f < card F
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower programmed FinPartState of S,
f be Instruction-Location of S such that
A1: f in dom F;
f = il.(S,locnum f) by AMISTD_1:def 13;
hence thesis by A1,AMISTD_1:50;
end;
theorem Th15:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being lower programmed FinPartState of S
holds dom F = { il.(S,k) where k is Nat: k < card F }
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower programmed FinPartState of S;
A1: dom F c= the Instruction-Locations of S by AMI_3:def 13;
hereby
let x be set;
assume
A2: x in dom F;
then reconsider f = x as Instruction-Location of S by A1;
A3: locnum f < card F by A2,Th14;
reconsider i = locnum f as Element of NAT;
f = il.(S,i) by AMISTD_1:def 13;
hence x in { il.(S,k) where k is Nat: k < card F } by A3;
end;
let x be set;
assume x in { il.(S,k) where k is Nat: k < card F };
then ex k being Nat st x = il.(S,k) & k < card F;
hence thesis by AMISTD_1:50;
end;
definition
let N be set;
let S be AMI-Struct over N;
let I be Element of the Instructions of S;
func AddressPart I equals :Def3:
I`2;
coherence;
end;
definition
let N be set;
let S be AMI-Struct over N;
let I be Element of the Instructions of S;
redefine func AddressPart I -> FinSequence of (union N) \/ the carrier of S;
coherence
proof
AddressPart I = I`2 by Def3;
hence thesis by FINSEQ_1:def 11;
end;
end;
theorem Th16:
for N being set,
S being AMI-Struct over N,
I, J being Element of the Instructions of S holds
InsCode I = InsCode J & AddressPart I = AddressPart J implies I = J
proof
let N be set,
S be AMI-Struct over N,
I, J be Element of the Instructions of S;
assume
A1: InsCode I = InsCode J & AddressPart I = AddressPart J;
(ex x, y being set st x in the Instruction-Codes of S &
y in ((union N) \/ the carrier of S)* & I = [x,y]) &
(ex x, y being set st x in the Instruction-Codes of S &
y in ((union N) \/
the carrier of S)* & J = [x,y]) by ZFMISC_1:def 2;
then A2: I = [I`1,I`2] & J = [J`1,J`2] by MCART_1:8;
InsCode I = I`1 & InsCode J = J`1 &
AddressPart I = I`2 & AddressPart J = J`2 by Def3,AMI_5:def 1;
hence thesis by A1,A2;
end;
definition
let N be set;
let S be AMI-Struct over N;
attr S is homogeneous means :Def4:
for I, J being Instruction of S st InsCode I = InsCode J holds
dom AddressPart I = dom AddressPart J;
end;
theorem Th17:
for I being Instruction of STC N holds AddressPart I = 0
proof
let I be Instruction of STC N;
the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
then A1: I = [0,0] or I = [1,0] by TARSKI:def 2;
thus AddressPart I = I`2 by Def3
.= 0 by A1,MCART_1:def 2;
end;
definition
let N be set;
let S be AMI-Struct over N;
let T be InsType of S;
func AddressParts T equals :Def5:
{ AddressPart I where I is Instruction of S: InsCode I = T };
coherence;
end;
definition
let N be set;
let S be AMI-Struct over N;
let T be InsType of S;
cluster AddressParts T -> functional;
coherence
proof
A1: AddressParts T = { AddressPart I where I is Instruction of S:
InsCode I = T } by Def5;
let f be set;
assume f in AddressParts T;
then ex I being Instruction of S st f = AddressPart I & InsCode I = T by A1
;
hence f is Function;
end;
end;
definition
let N be with_non-empty_elements set,
S be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of S;
attr I is with_explicit_jumps means :Def6:
for f being set st f in JUMP I holds
ex k being set st k in dom AddressPart I & f = (AddressPart I).k &
(PA AddressParts InsCode I).k = the Instruction-Locations of S;
attr I is without_implicit_jumps means :Def7:
for f being set st
ex k being set st k in dom AddressPart I & f = (AddressPart I).k &
(PA AddressParts InsCode I).k = the Instruction-Locations of S
holds f in JUMP I;
end;
definition
let N be with_non-empty_elements set,
S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
attr S is with_explicit_jumps means :Def8:
for I being Instruction of S holds I is with_explicit_jumps;
attr S is without_implicit_jumps means :Def9:
for I being Instruction of S holds I is without_implicit_jumps;
end;
definition
let N be set,
S be AMI-Struct over N;
attr S is with-non-trivial-Instruction-Locations means :Def10:
the Instruction-Locations of S is non trivial;
end;
definition
let N be with_non-empty_elements set;
cluster standard -> with-non-trivial-Instruction-Locations
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
coherence
proof
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
given f being Function of NAT, the Instruction-Locations of S such that
A1: f is bijective and
for m, n being Nat holds m <= n iff f.m <= f.n;
A2: NAT,the Instruction-Locations of S are_equipotent by A1,KNASTER:13;
thus the Instruction-Locations of S is non trivial
proof
assume not thesis;
then reconsider a = the Instruction-Locations of S as trivial set;
a is finite;
hence thesis by A2,CARD_1:68;
end;
end;
end;
definition
let N be with_non-empty_elements set;
cluster standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
existence
proof
take STC N;
thus thesis;
end;
end;
definition
let N be with_non-empty_elements set,
S be with-non-trivial-Instruction-Locations AMI-Struct over N;
cluster the Instruction-Locations of S -> non trivial;
coherence by Def10;
end;
theorem Th18:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S
st for f being Instruction-Location of S holds NIC(I,f)={NextLoc f}
holds JUMP I is empty
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S;
assume
A1: for f being Instruction-Location of S holds NIC(I,f)={NextLoc f};
consider p, q being Element of the Instruction-Locations of S such that
A2: p <> q by YELLOW_8:def 1;
set X = { NIC(I,f) where f is Instruction-Location of S:
not contradiction };
assume not thesis;
then meet X is non empty by AMISTD_1:def 6;
then consider x being set such that
A3: x in meet X by XBOOLE_0:def 1;
NIC(I,p) = {NextLoc p} & NIC(I,q) = {NextLoc q} by A1;
then {NextLoc p} in X & {NextLoc q} in X;
then x in {NextLoc p} & x in {NextLoc q} by A3,SETFAM_1:def 1;
then x = NextLoc p & x = NextLoc q by TARSKI:def 1;
hence contradiction by A2,AMISTD_1:36;
end;
definition
let N be with_non-empty_elements set,
I be Instruction of STC N;
cluster JUMP I -> empty;
coherence
proof
per cases by AMISTD_1:22;
suppose InsCode I = 0;
then I is halting by AMISTD_1:20;
then for f being Instruction-Location of STC N holds NIC(I,f)={f}
by AMISTD_1:15;
hence thesis by AMISTD_1:14;
suppose
InsCode I = 1;
then for f being Instruction-Location of STC N holds NIC(I,f)={NextLoc f}
by AMISTD_1:39;
hence thesis by Th18;
end;
end;
definition
let N be set;
let S be AMI-Struct over N;
attr S is regular means :Def11:
for T being InsType of S holds AddressParts T is product-like;
end;
definition let N be set;
cluster regular -> homogeneous AMI-Struct over N;
coherence
proof
let S be AMI-Struct over N such that
A1: for T being InsType of S holds AddressParts T is product-like;
let I, J be Instruction of S such that
A2: InsCode I = InsCode J;
AddressParts InsCode I is product-like by A1;
then consider f being Function such that
A3: AddressParts InsCode I = product f by Def2;
AddressParts InsCode I =
{ AddressPart A where A is Instruction of S: InsCode A = InsCode I }
by Def5;
then A4: AddressPart I in AddressParts InsCode I &
AddressPart J in AddressParts InsCode I by A2;
hence dom AddressPart I = dom f by A3,CARD_3:18
.= dom AddressPart J by A3,A4,CARD_3:18;
end;
end;
theorem Th19:
for T being InsType of STC N holds AddressParts T = {0}
proof
let T be InsType of STC N;
set A = { AddressPart I where
I is Instruction of STC N: InsCode I = T };
{0} = A
proof
hereby
let a be set;
assume a in {0};
then A1: a = 0 by TARSKI:def 1;
A2: the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
A3: the Instruction-Codes of STC N = {0,1} by AMISTD_1:def 11;
per cases by A3,TARSKI:def 2;
suppose
A4: T = 0;
[0,0] in {[0,0],[1,0]} by TARSKI:def 2;
then reconsider I = [0,0] as Instruction of STC N by A2;
A5: AddressPart I = 0 by Th17;
InsCode I = I`1 by AMI_5:def 1
.= 0 by MCART_1:def 1;
hence a in A by A1,A4,A5;
suppose
A6: T = 1;
[1,0] in {[0,0],[1,0]} by TARSKI:def 2;
then reconsider I = [1,0] as Instruction of STC N by A2;
A7: AddressPart I = 0 by Th17;
InsCode I = I`1 by AMI_5:def 1
.= 1 by MCART_1:def 1;
hence a in A by A1,A6,A7;
end;
let a be set;
assume a in A;
then ex I being Instruction of STC N st a = AddressPart I & InsCode I =
T;
then a = 0 by Th17;
hence a in {0} by TARSKI:def 1;
end;
hence thesis by Def5;
end;
definition
let N be with_non-empty_elements set;
cluster STC N -> with_explicit_jumps without_implicit_jumps regular;
coherence
proof
thus STC N is with_explicit_jumps
proof
let I be Instruction of STC N;
let f be set;
thus thesis;
end;
thus STC N is without_implicit_jumps
proof
let I be Instruction of STC N;
let f be set;
the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
then A1: I = [0,0] or I = [1,0] by TARSKI:def 2;
AddressPart I = I`2 by Def3
.= 0 by A1,MCART_1:def 2;
hence thesis by FINSEQ_1:26;
end;
let T be InsType of STC N;
take {};
thus thesis by Th19,CARD_3:19;
end;
end;
definition
let N be with_non-empty_elements set;
cluster standard regular halting realistic steady-programmed programmable
with_explicit_jumps without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
existence
proof
take STC N;
thus thesis;
end;
end;
definition
let N be with_non-empty_elements set;
let S be regular AMI-Struct over N;
let T be InsType of S;
cluster AddressParts T -> product-like;
coherence by Def11;
end;
definition
let N be with_non-empty_elements set;
let S be homogeneous AMI-Struct over N;
let T be InsType of S;
cluster AddressParts T -> with_common_domain;
coherence
proof
A1: AddressParts T = { AddressPart I where I is Instruction of S:
InsCode I = T } by Def5;
let f, g be Function;
assume f in AddressParts T & g in AddressParts T;
then (ex I being Instruction of S st f = AddressPart I & InsCode I = T) &
ex J being Instruction of S st g = AddressPart J & InsCode J = T by A1;
hence dom f = dom g by Def4;
end;
end;
theorem Th20:
for S being homogeneous non empty non void AMI-Struct over N,
I being Instruction of S,
x being set st x in dom AddressPart I holds
(PA AddressParts InsCode I).x = the Instruction-Locations of S implies
(AddressPart I).x is Instruction-Location of S
proof
let S be homogeneous non empty non void AMI-Struct over N,
I be Instruction of S,
x be set such that
A1: x in dom AddressPart I;
A2: AddressParts InsCode I =
{ AddressPart J where J is Instruction of S: InsCode J = InsCode I }
by Def5;
then A3: AddressPart I in AddressParts InsCode I;
assume
A4: (PA AddressParts InsCode I).x = the Instruction-Locations of S;
for f being Function st f in AddressParts InsCode I holds x in dom f
proof
let f be Function;
assume f in AddressParts InsCode I;
then ex J being Instruction of S st f = AddressPart J & InsCode I =
InsCode J
by A2;
hence x in dom f by A1,Def4;
end;
then x in dom PA AddressParts InsCode I by A3,Def1;
then (PA AddressParts InsCode I).x = pi(AddressParts InsCode I,x)
by A3,Def1;
hence (AddressPart I).x is Instruction-Location of S by A3,A4,CARD_3:def 6
;
end;
definition
let N be with_non-empty_elements set;
let S be with_explicit_jumps (IC-Ins-separated
definite (non empty non void AMI-Struct over N));
cluster -> with_explicit_jumps Instruction of S;
coherence by Def8;
end;
definition
let N be with_non-empty_elements set;
let S be without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster -> without_implicit_jumps Instruction of S;
coherence by Def9;
end;
theorem Th21:
for S being with-non-trivial-Instruction-Locations
realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I being Instruction of S st I is halting
holds JUMP I is empty
proof
let S be with-non-trivial-Instruction-Locations
realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be Instruction of S;
assume I is halting;
then for l being Instruction-Location of S holds NIC(I,l)={l} by AMISTD_1:
15;
hence thesis by AMISTD_1:14;
end;
definition
let N be with_non-empty_elements set,
S be with-non-trivial-Instruction-Locations halting realistic
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be halting Instruction of S;
cluster JUMP I -> empty;
coherence by Th21;
end;
definition
let N be with_non-empty_elements set,
S be with-non-trivial-Instruction-Locations IC-Ins-separated definite
(non empty non void AMI-Struct over N);
cluster non trivial programmed FinPartState of S;
existence
proof
consider l1, l2 being Element of the Instruction-Locations of S such that
A1: l1 <> l2 by YELLOW_8:def 1;
consider I being Instruction of S;
take f = (l1,l2) --> (I,I);
thus f is non trivial
proof
f = { [l1,I], [l2,I] } by A1,FUNCT_4:71;
then reconsider x = [l1,I], y = [l2,I] as Element of f by TARSKI:def 2;
take x, y;
thus x <> y by A1,ZFMISC_1:33;
end;
let a be set;
assume a in dom f;
then a in {l1,l2} by FUNCT_4:65;
then a = l1 or a = l2 by TARSKI:def 2;
hence thesis;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
cluster trivial -> unique-halt (non empty programmed FinPartState of S);
coherence
proof
let F be non empty programmed FinPartState of S;
assume
A1: F is trivial;
let f be Instruction-Location of S such that
F.f = halt S and
A2: f in dom F;
consider x being set such that
A3: F = {x} by A1,REALSET1:def 12;
x in F by A3,TARSKI:def 1;
then consider a, b being set such that
A4: [a,b] = x by RELAT_1:def 1;
A5: LastLoc F in dom F by AMISTD_1:51;
A6: dom F = {a} by A3,A4,RELAT_1:23;
hence f = a by A2,TARSKI:def 1
.= LastLoc F by A5,A6,TARSKI:def 1;
end;
end;
definition
let N be set;
let S be AMI-Struct over N;
let I be Instruction of S;
attr I is ins-loc-free means :Def12:
for x being set st x in dom AddressPart I
holds (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
end;
theorem
for S being halting with_explicit_jumps
with-non-trivial-Instruction-Locations
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S st I is ins-loc-free
holds JUMP I is empty
proof
let S be halting with_explicit_jumps
with-non-trivial-Instruction-Locations
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S such that
A1: for x being set st x in dom AddressPart I
holds (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
assume JUMP I is non empty;
then consider f being set such that
A2: f in JUMP I by XBOOLE_0:def 1;
ex k being set st k in dom AddressPart I & f = (AddressPart I).k &
(PA AddressParts InsCode I).k = the Instruction-Locations of S
by A2,Def6;
hence thesis by A1;
end;
theorem Th23:
for S being without_implicit_jumps with-non-trivial-Instruction-Locations
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S st I is halting
holds I is ins-loc-free
proof
let S be without_implicit_jumps with-non-trivial-Instruction-Locations
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S such that
A1: I is halting;
let x be set such that
A2: x in dom AddressPart I;
assume (PA AddressParts InsCode I).x = the Instruction-Locations of S;
then (AddressPart I).x in JUMP I by A2,Def7;
hence contradiction by A1,Th21;
end;
definition
let N be with_non-empty_elements set,
S be without_implicit_jumps
with-non-trivial-Instruction-Locations
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
cluster halting -> ins-loc-free Instruction of S;
coherence by Th23;
end;
theorem Th24:
for S being standard without_implicit_jumps
(IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S st I is sequential
holds I is ins-loc-free
proof
let S be standard without_implicit_jumps
(IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S;
assume
A1: I is sequential;
assume not thesis;
then consider k being set such that
A2: k in dom AddressPart I &
(PA AddressParts InsCode I).k = the Instruction-Locations of S
by Def12;
(AddressPart I).k in JUMP I by A2,Def7;
hence thesis by A1,AMISTD_1:43;
end;
definition
let N be with_non-empty_elements set,
S be standard without_implicit_jumps
(IC-Ins-separated definite
(non empty non void AMI-Struct over N));
cluster sequential -> ins-loc-free Instruction of S;
coherence by Th24;
end;
definition
let N be with_non-empty_elements set,
S be standard halting
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
func Stop S -> FinPartState of S equals :Def13:
il.(S,0) .--> halt S;
coherence;
end;
Lm5:
now
let N be with_non-empty_elements set,
S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
thus dom Stop S = dom (il.(S,0) .--> halt S) by Def13
.= {il.(S,0)} by CQC_LANG:5;
hence il.(S,0) in dom Stop S by TARSKI:def 1;
end;
Lm6:
now
let N be with_non-empty_elements set,
S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
thus (Stop S).il.(S,0) = (il.(S,0) .--> halt S).il.(S,0) by Def13
.= halt S by CQC_LANG:6;
end;
definition
let N be with_non-empty_elements set,
S be standard halting
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster Stop S -> lower non empty programmed trivial;
coherence
proof
Stop S = il.(S,0) .--> halt S by Def13;
hence thesis by AMISTD_1:48;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard realistic halting
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster Stop S -> closed;
coherence
proof
Stop S = il.(S,0) .--> halt S by Def13;
hence thesis by AMISTD_1:46;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard halting steady-programmed
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster Stop S -> autonomic;
coherence
proof
Stop S = il.(S,0) .--> halt S by Def13;
hence thesis by AMISTD_1:12;
end;
end;
theorem Th25:
for S being standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N))
holds card Stop S = 1
proof
let S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
thus card Stop S = card (il.(S,0) .--> halt S) by Def13
.= card {[il.(S,0),halt S]} by AMI_1:19
.= 1 by CARD_1:79;
end;
theorem Th26:
for S being standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being pre-Macro of S st card F = 1 holds F = Stop S
proof
let S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be pre-Macro of S;
assume
A1: card F = 1;
then consider x being set such that
A2: F = {x} by CARD_2:60;
x in F by A2,TARSKI:def 1;
then consider a, b being set such that
A3: [a,b] = x by RELAT_1:def 1;
A4: dom F = {a} by A2,A3,RELAT_1:23;
A5: il.(S,0) in dom F by AMISTD_1:49;
then A6: a = il.(S,0) by A4,TARSKI:def 1;
card F -' 1 = card F - 1 by Th4
.= 0 by A1;
then LastLoc F = il.(S,0) by AMISTD_1:55;
then F.il.(S,0) = halt S by AMISTD_1:def 22;
then halt S in rng F by A5,FUNCT_1:def 5;
then halt S in {b} by A2,A3,RELAT_1:23;
then F = {[il.(S,0),halt S]} by A2,A3,A6,TARSKI:def 1
.= il.(S,0) .--> halt S by AMI_1:19;
hence F = Stop S by Def13;
end;
Lm7:
for S being standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N))
holds card Stop S -' 1 = 0
proof
let S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
thus card Stop S -' 1 = card Stop S - 1 by Th4
.= 1 - 1 by Th25
.= 0;
end;
theorem Th27:
for S being standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N))
holds LastLoc Stop S = il.(S,0)
proof
let S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
card Stop S -' 1 = 0 by Lm7;
hence LastLoc Stop S = il.(S,0) by AMISTD_1:55;
end;
definition
let N be with_non-empty_elements set,
S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
cluster Stop S -> halt-ending unique-halt;
coherence
proof
thus (Stop S).(LastLoc Stop S)
= (Stop S).il.(S,0) by Th27
.= (il.(S,0) .--> halt S).il.(S,0) by Def13
.= halt S by CQC_LANG:6;
let l be Instruction-Location of S such that (Stop S).l = halt S;
assume l in dom Stop S;
then l in {il.(S,0)} by Lm5;
then l = il.(S,0) by TARSKI:def 1;
hence l = LastLoc Stop S by Th27;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
redefine func Stop S -> pre-Macro of S;
coherence;
end;
begin :: On the composition of macro instructions
definition
let N be with_non-empty_elements set;
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let I be Element of the Instructions of S;
let k be natural number;
func IncAddr(I,k) -> Instruction of S means :Def14:
InsCode it = InsCode I &
dom AddressPart it = dom AddressPart I &
for n being set st n in dom AddressPart I holds
((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
ex f being Instruction-Location of S st
f = (AddressPart I).n & (AddressPart it).n = il.(S,k + locnum f)) &
((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
(AddressPart it).n = (AddressPart I).n);
existence
proof
set D = (union N) \/ the carrier of S;
defpred P[set,set] means
((PA AddressParts InsCode I).$1 = the Instruction-Locations of S implies
ex il being Instruction-Location of S st
il = (AddressPart I).$1 & $2 = il.(S,k + locnum il)) &
((PA AddressParts InsCode I).$1 <> the Instruction-Locations of S implies
$2 = (AddressPart I).$1);
A2: for m being Nat st m in Seg len AddressPart I
ex x being Element of D st P[m,x]
proof
let m be Nat;
assume m in Seg len AddressPart I;
then A3: m in dom AddressPart I by FINSEQ_1:def 3;
then A4: (AddressPart I).m in rng AddressPart I by FUNCT_1:def 5;
per cases;
suppose
A5: (PA AddressParts InsCode I).m = the Instruction-Locations of S;
then reconsider il = (AddressPart I).m as Instruction-Location of S
by A3,Th20;
reconsider x = il.(S,k + locnum il) as Element of D by XBOOLE_0:def 2;
take x;
thus thesis by A5;
suppose
A6: (PA AddressParts InsCode I).m <> the Instruction-Locations of S;
rng AddressPart I c= D by FINSEQ_1:def 4;
then reconsider x = (AddressPart I).m as Element of D by A4;
take x;
thus thesis by A6;
end;
consider p being FinSequence of D such that
A7: dom p = Seg len AddressPart I and
A8: for k being Nat st k in Seg len AddressPart I holds P[k,p.k]
from SeqDEx(A2);
set f = PA AddressParts InsCode I;
A9: AddressParts InsCode I =
{ AddressPart J where J is Instruction of S: InsCode J = InsCode I }
by Def5;
then A10: AddressPart I in AddressParts InsCode I;
then A11: AddressParts InsCode I = product f by Th10;
A12: dom p = dom AddressPart I by A7,FINSEQ_1:def 3
.= DOM AddressParts InsCode I by A10,PRALG_2:def 2
.= dom f by Th7;
for z being set st z in dom p holds p.z in f.z
proof
let z be set;
assume
A13: z in dom p;
then A14: f.z = pi(AddressParts InsCode I,z) by A10,A12,Def1;
reconsider z as Nat by A13;
per cases;
suppose
A15: f.z = the Instruction-Locations of S;
then ex il being Instruction-Location of S st
il = (AddressPart I).z & p.z = il.(S,k + locnum il) by A7,A8,A13;
hence thesis by A15;
suppose f.z <> the Instruction-Locations of S;
then p.z = (AddressPart I).z by A7,A8,A13;
hence thesis by A10,A14,CARD_3:def 6;
end;
then p in AddressParts InsCode I by A11,A12,CARD_3:18;
then consider IT being Instruction of S such that
A16: p = AddressPart IT and
A17: InsCode I = InsCode IT by A9;
take IT;
thus InsCode IT = InsCode I by A17;
thus dom AddressPart IT = dom AddressPart I by A7,A16,FINSEQ_1:def 3;
let n be set;
assume n in dom AddressPart I;
then n in Seg len AddressPart I by FINSEQ_1:def 3;
hence thesis by A8,A16;
end;
uniqueness
proof
let a, b be Instruction of S such that
A18: InsCode a = InsCode I and
A19: dom AddressPart a = dom AddressPart I and
A20: for n being set st n in dom AddressPart I holds
((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
ex f being Instruction-Location of S st
f = (AddressPart I).n & (AddressPart a).n = il.(S,k + locnum f)) &
((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
(AddressPart a).n = (AddressPart I).n) and
A21: InsCode b = InsCode I and
A22: dom AddressPart b = dom AddressPart I and
A23: for n being set st n in dom AddressPart I holds
((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
ex f being Instruction-Location of S st
f = (AddressPart I).n & (AddressPart b).n = il.(S,k + locnum f)) &
((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
(AddressPart b).n = (AddressPart I).n);
A24: Seg len AddressPart a = dom AddressPart a by FINSEQ_1:def 3;
for n being Nat st n in Seg len AddressPart a holds
(AddressPart a).n = (AddressPart b).n
proof
let n be Nat;
assume n in Seg len AddressPart a;
then ((PA AddressParts InsCode I).n = the Instruction-Locations of S
implies
ex f being Instruction-Location of S st
f = (AddressPart I).n & (AddressPart a).n = il.(S,k + locnum f)) &
((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
(AddressPart a).n = (AddressPart I).n) &
((PA AddressParts InsCode I).n = the Instruction-Locations of S implies
ex f being Instruction-Location of S st
f = (AddressPart I).n & (AddressPart b).n = il.(S,k + locnum f)) &
((PA AddressParts InsCode I).n <> the Instruction-Locations of S implies
(AddressPart b).n = (AddressPart I).n)
by A19,A20,A23,A24;
hence (AddressPart a).n = (AddressPart b).n;
end;
then AddressPart a = AddressPart b by A19,A22,A24,FINSEQ_1:17;
hence thesis by A18,A21,Th16;
end;
end;
theorem Th28:
for S being regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I being Element of the Instructions of S
holds IncAddr(I, 0) = I
proof
let S be regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be Element of the Instructions of S;
A1: InsCode IncAddr(I, 0) = InsCode I by Def14;
A2: dom AddressPart I = dom AddressPart IncAddr(I, 0) by Def14;
for k being Nat st k in dom AddressPart I holds
(AddressPart IncAddr(I, 0)).k = (AddressPart I).k
proof
let k be Nat;
assume
A3: k in dom AddressPart I;
per cases;
suppose (PA AddressParts InsCode I).k = the Instruction-Locations of S;
then ex f being Instruction-Location of S st
f = (AddressPart I).k &
(AddressPart IncAddr(I,0)).k = il.(S,0 + locnum f) by A3,Def14;
hence thesis by AMISTD_1:def 13;
suppose (PA AddressParts InsCode I).k <> the Instruction-Locations of S;
hence thesis by A3,Def14;
end;
then AddressPart IncAddr(I, 0) = AddressPart I by A2,FINSEQ_1:17;
hence IncAddr(I, 0) = I by A1,Th16;
end;
theorem Th29:
for S being regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I being Instruction of S st I is ins-loc-free
holds IncAddr(I, k) = I
proof
let S be regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be Instruction of S such that
A1: for x being set st x in dom AddressPart I
holds (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
set f = IncAddr(I, k);
A2: InsCode f = InsCode I by Def14;
A3: dom AddressPart f = dom AddressPart I by Def14;
for x being set st x in dom AddressPart I holds
(AddressPart f).x = (AddressPart I).x
proof
let x be set such that
A4: x in dom AddressPart I;
(PA AddressParts InsCode I).x = the Instruction-Locations of S or
(PA AddressParts InsCode I).x <> the Instruction-Locations of S;
hence thesis by A1,A4,Def14;
end;
then AddressPart f = AddressPart I by A3,FUNCT_1:9;
hence thesis by A2,Th16;
end;
theorem Th30:
for S being halting standard without_implicit_jumps realistic
regular (IC-Ins-separated definite
(non empty non void AMI-Struct over N))
holds IncAddr(halt S, k) = halt S
proof
let S be halting standard without_implicit_jumps realistic
regular (IC-Ins-separated definite (non empty non void AMI-Struct over N));
thus thesis by Th29;
end;
definition
let N be with_non-empty_elements set,
S be halting standard without_implicit_jumps
realistic regular
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be halting Instruction of S,
k be natural number;
cluster IncAddr(I,k) -> halting;
coherence by Th29;
end;
theorem Th31:
for S being regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I being Instruction of S
holds AddressParts InsCode I = AddressParts InsCode IncAddr(I,k)
proof
let S be regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be Instruction of S;
set A = { AddressPart J where J is Instruction of S:
InsCode I = InsCode J },
B = { AddressPart J where J is Instruction of S:
InsCode IncAddr(I,k) = InsCode J };
A1: A = B
proof
hereby
let a be set;
assume a in A;
then consider J being Instruction of S such that
A2: a = AddressPart J and
A3: InsCode J = InsCode I;
InsCode J = InsCode IncAddr(I,k) by A3,Def14;
hence a in B by A2;
end;
let a be set;
assume a in B;
then consider J being Instruction of S such that
A4: a = AddressPart J and
A5: InsCode J = InsCode IncAddr(I,k);
InsCode J = InsCode I by A5,Def14;
hence a in A by A4;
end;
thus AddressParts InsCode I = A by Def5
.= AddressParts InsCode IncAddr(I,k) by A1,Def5;
end;
theorem Th32:
for S being regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I, J being Instruction of S st
(ex k being natural number st IncAddr(I,k) = IncAddr(J,k))
holds
(PA AddressParts InsCode I).x = the Instruction-Locations of S implies
(PA AddressParts InsCode J).x = the Instruction-Locations of S
proof
let S be regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I, J be Instruction of S;
given k being natural number such that
A1: IncAddr(I,k) = IncAddr(J,k);
assume
A2: (PA AddressParts InsCode I).x = the Instruction-Locations of S;
assume
A3: (PA AddressParts InsCode J).x <> the Instruction-Locations of S;
(PA AddressParts InsCode IncAddr(I,k)).x = the Instruction-Locations of S
by A2,Th31;
hence thesis by A1,A3,Def14;
end;
theorem Th33:
for S being regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I, J being Instruction of S st
(ex k being natural number st IncAddr(I,k) = IncAddr(J,k))
holds
(PA AddressParts InsCode I).x <> the Instruction-Locations of S implies
(PA AddressParts InsCode J).x <> the Instruction-Locations of S
proof
let S be regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I, J be Instruction of S;
given k being natural number such that
A1: IncAddr(I,k) = IncAddr(J,k);
assume
A2: (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
assume
(PA AddressParts InsCode J).x = the Instruction-Locations of S;
then (PA AddressParts InsCode IncAddr(J,k)).x = the Instruction-Locations
of S
by Th31;
hence contradiction by A1,A2,Th31;
end;
theorem Th34:
for S being regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I, J being Instruction of S st
ex k being natural number st IncAddr(I,k) = IncAddr(J,k)
holds I = J
proof
let S be regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I, J be Instruction of S;
given k being natural number such that
A1: IncAddr(I,k) = IncAddr(J,k);
A2: InsCode I = InsCode IncAddr(I,k) by Def14
.= InsCode J by A1,Def14;
then A3: dom AddressPart I = dom AddressPart J by Def4;
for x being set st x in dom AddressPart I holds
(AddressPart I).x = (AddressPart J).x
proof
let x be set;
assume
A4: x in dom AddressPart I;
per cases;
suppose
A5: (PA AddressParts InsCode I).x = the Instruction-Locations of S;
then consider f being Instruction-Location of S such that
A6: f = (AddressPart I).x and
A7: (AddressPart IncAddr(I,k)).x = il.(S,k + locnum f) by A4,Def14;
(PA AddressParts InsCode J).x = the Instruction-Locations of S
by A1,A5,Th32;
then consider g being Instruction-Location of S such that
A8: g = (AddressPart J).x and
A9: (AddressPart IncAddr(J,k)).x = il.(S,k + locnum g) by A3,A4,Def14;
k + locnum f = k + locnum g by A1,A7,A9,AMISTD_1:25;
then locnum f = locnum g by XCMPLX_1:2;
hence (AddressPart I).x = (AddressPart J).x by A6,A8,AMISTD_1:27;
suppose
A10: (PA AddressParts InsCode I).x <> the Instruction-Locations of S;
then A11: (PA AddressParts InsCode J).x <> the Instruction-Locations of S
by A1,Th33;
thus (AddressPart I).x = (AddressPart IncAddr(I,k)).x by A4,A10,Def14
.= (AddressPart J).x by A1,A3,A4,A11,Def14;
end;
then AddressPart I = AddressPart J by A3,FUNCT_1:9;
hence I = J by A2,Th16;
end;
theorem Th35:
for S being regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S st IncAddr(I,k) = halt S
holds I = halt S
proof
let S be regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S;
assume IncAddr(I,k) = halt S;
then IncAddr(I,k) = IncAddr(halt S,k) by Th30;
hence I = halt S by Th34;
end;
theorem
for S being regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S st I is sequential
holds IncAddr(I,k) is sequential
proof
let S be regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S;
assume
A1: I is sequential;
then I is ins-loc-free by Th24;
hence thesis by A1,Th29;
end;
theorem Th37:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of S
holds IncAddr(IncAddr(I,k),m) = IncAddr(I,k+m)
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S;
A1: InsCode IncAddr(IncAddr(I,k),m)
= InsCode IncAddr(I,k) by Def14
.= InsCode I by Def14
.= InsCode IncAddr(I,k+m) by Def14;
A2: dom AddressPart IncAddr(I,k+m)
= dom AddressPart I by Def14
.= dom AddressPart IncAddr(I,k) by Def14
.= dom AddressPart IncAddr(IncAddr(I,k),m) by Def14;
for n being set st n in dom AddressPart IncAddr(IncAddr(I,k),m) holds
(AddressPart IncAddr(IncAddr(I,k),m)).n = (AddressPart IncAddr(I,k+m)).n
proof
let n be set such that
A3: n in dom AddressPart IncAddr(IncAddr(I,k),m);
A4: n in dom AddressPart IncAddr(I,k) by A3,Def14;
then A5: n in dom AddressPart I by Def14;
per cases;
suppose
A6: (PA AddressParts InsCode I).n = the Instruction-Locations of S;
then consider f being Instruction-Location of S such that
A7: f = (AddressPart I).n and
A8: (AddressPart IncAddr(I,k)).n = il.(S,k + locnum f) by A5,Def14;
(PA AddressParts InsCode IncAddr(I,k)).n =
the Instruction-Locations of S by A6,Th31;
then consider g being Instruction-Location of S such that
A9: g = (AddressPart IncAddr(I,k)).n and
A10: (AddressPart IncAddr(IncAddr(I,k),m)).n = il.(S,m + locnum g)
by A4,Def14;
consider h being Instruction-Location of S such that
A11: h = (AddressPart I).n and
A12: (AddressPart IncAddr(I,k+m)).n = il.(S,k + m + locnum h)
by A5,A6,Def14;
locnum g = k + locnum f by A8,A9,AMISTD_1:def 13;
hence (AddressPart IncAddr(IncAddr(I,k),m)).n
= (AddressPart IncAddr(I,k+m)).n by A7,A10,A11,A12,XCMPLX_1:1;
suppose
A13: (PA AddressParts InsCode I).n <> the Instruction-Locations of S;
then (PA AddressParts InsCode IncAddr(I,k)).n <>
the Instruction-Locations of S by Def14;
hence (AddressPart IncAddr(IncAddr(I,k),m)).n
= (AddressPart IncAddr(I,k)).n by A4,Def14
.= (AddressPart I).n by A5,A13,Def14
.= (AddressPart IncAddr(I,k+m)).n by A5,A13,Def14;
end;
then AddressPart IncAddr(IncAddr(I,k),m) = AddressPart IncAddr(I,k+m)
by A2,FUNCT_1:9;
hence IncAddr(IncAddr(I,k),m) = IncAddr(I,k+m) by A1,Th16;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
p be programmed FinPartState of S,
k be natural number;
A1: dom p c= the Instruction-Locations of S by AMI_3:def 13;
func IncAddr(p,k) -> FinPartState of S means :Def15:
dom it = dom p &
for m being natural number st il.(S,m) in dom p holds
it.il.(S,m) = IncAddr(pi(p,il.(S,m)),k);
existence
proof
defpred P[set,set] means ex m being Nat st $1 = il.(S,m) &
$2 = IncAddr(pi(p,il.(S,m)),k);
A2: for e being set st e in dom p ex u being set st P[e,u]
proof
let e be set;
assume e in dom p;
then consider m being natural number such that
A3: e = il.(S,m) by A1,AMISTD_1:26;
take IncAddr(pi(p,il.(S,m)),k);
reconsider m as Element of NAT by ORDINAL2:def 21;
e = il.(S,m) by A3;
hence thesis;
end;
consider f being Function such that
A4: dom f = dom p and
A5: for e being set st e in dom p holds P[e,f.e] from NonUniqFuncEx(A2);
dom p c= the carrier of S by A1,XBOOLE_1:1;
then A6: dom f c= dom the Object-Kind of S by A4,FUNCT_2:def 1;
for x being set st x in dom f holds f.x in (the Object-Kind of S).x
proof
let x be set;
assume
A7: x in dom f;
then A8: ex m being Nat st x = il.(S,m) & f.x = IncAddr(pi
(p,il.(S,m)),k) by A4,A5;
reconsider y = x as Instruction-Location of S by A1,A4,A7;
(the Object-Kind of S).y = ObjectKind y by AMI_1:def 6
.= the Instructions of S by AMI_1:def 14;
hence f.x in (the Object-Kind of S).x by A8;
end;
then reconsider f as Element of sproduct the Object-Kind of S by A6,AMI_1:
def 16
;
f is finite by A4,AMI_1:21;
then reconsider f as FinPartState of S by AMI_1:def 24;
take f;
thus dom f = dom p by A4;
let m be natural number;
assume il.(S,m) in dom p;
then ex j being Nat st il.(S,m) = il.(S,j) &
f.il.(S,m) = IncAddr(pi(p,il.(S,j)),k) by A5;
hence f.il.(S,m) = IncAddr(pi(p,il.(S,m)),k);
end;
uniqueness
proof
let IT1,IT2 be FinPartState of S such that
A9: dom IT1 = dom p and
A10: for m being natural number st il.(S,m) in dom p holds
IT1.il.(S,m) = IncAddr(pi(p,il.(S,m)),k)
and
A11: dom IT2 = dom p and
A12: for m being natural number st il.(S,m) in dom p holds
IT2.il.(S,m) = IncAddr(pi(p,il.(S,m)),k);
for x being set st x in dom p holds IT1.x = IT2.x
proof
let x be set;
assume
A13: x in dom p;
then consider m being natural number such that
A14: x = il.(S,m) by A1,AMISTD_1:26;
reconsider m as Element of NAT by ORDINAL2:def 21;
A15: x = il.(S,m) by A14;
hence IT1.x = IncAddr(pi(p,il.(S,m)),k) by A10,A13
.= IT2.x by A12,A13,A15;
end;
hence IT1=IT2 by A9,A11,FUNCT_1:9;
end;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be programmed FinPartState of S,
k be natural number;
cluster IncAddr(F,k) -> programmed;
coherence
proof
dom IncAddr(F,k) = dom F by Def15;
hence dom IncAddr(F,k) c= the Instruction-Locations of S by AMI_3:def 13;
end;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be empty programmed FinPartState of S,
k be natural number;
cluster IncAddr(F,k) -> empty;
coherence
proof
assume not thesis;
then reconsider f = IncAddr(F,k) as non empty Function;
A1: dom f <> {};
dom IncAddr(F,k) = dom F by Def15;
hence thesis by A1;
end;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be non empty programmed FinPartState of S,
k be natural number;
cluster IncAddr(F,k) -> non empty;
coherence
proof
dom IncAddr(F,k) = dom F by Def15;
hence thesis by Lm1;
end;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower programmed FinPartState of S,
k be natural number;
cluster IncAddr(F,k) -> lower;
coherence
proof
dom IncAddr(F,k) = dom F by Def15;
hence thesis by Th13;
end;
end;
theorem Th38:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being programmed FinPartState of S
holds IncAddr(F,0) = F
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be programmed FinPartState of S;
for m being natural number st il.(S,m) in dom F holds
F.il.(S,m) = IncAddr(pi(F,il.(S,m)),0)
proof
let m be natural number;
assume il.(S,m) in dom F;
then pi(F,il.(S,m)) = F.il.(S,m) by AMI_5:def 5;
hence F.il.(S,m) = IncAddr(pi(F,il.(S,m)),0) by Th28;
end;
hence thesis by Def15;
end;
theorem
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being lower programmed FinPartState of S
holds IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m)
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower programmed FinPartState of S;
A1: dom IncAddr(IncAddr(F,k),m) = dom IncAddr(F,k) by Def15
.= dom F by Def15;
A2: dom IncAddr(F,k+m) = dom F by Def15;
for x being set st x in dom F holds
IncAddr(IncAddr(F,k),m).x = IncAddr(F,k+m).x
proof
let x be set such that
A3: x in dom F;
dom F c= the Instruction-Locations of S by AMI_3:def 13;
then reconsider x as Instruction-Location of S by A3;
A4: x = il.(S,locnum x) by AMISTD_1:def 13;
then A5: il.(S,locnum x) in dom IncAddr(F,k) by A3,Def15;
A6: IncAddr(pi(F,il.(S,locnum x)),k) = IncAddr(F,k).il.(S,locnum x)
by A3,A4,Def15
.= pi(IncAddr(F,k),il.(S,locnum x)) by A5,AMI_5:def 5;
IncAddr(IncAddr(F,k),m).il.(S,locnum x)
= IncAddr(pi(IncAddr(F,k),il.(S,locnum x)),m) by A5,Def15
.= IncAddr(pi(F,il.(S,locnum x)),k+m) by A6,Th37
.= IncAddr(F,k+m).il.(S,locnum x) by A3,A4,Def15;
hence thesis by A4;
end;
hence IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m) by A1,A2,FUNCT_1:9;
end;
definition
let N be with_non-empty_elements set,
S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
p be FinPartState of S,
k be natural number;
func Shift(p,k) -> FinPartState of S means :Def16:
dom it = { il.(S,m+k) where m is Nat: il.(S,m) in dom p } &
for m being Nat st il.(S,m) in dom p holds it.il.(S,m+k) = p.il.(S,m);
existence
proof
deffunc _F(Nat) = il.(S,$1+k);
deffunc _G(Nat) = il.(S,$1);
set A = { _F(m) where m is Nat: _G(m) in dom p };
defpred P [set,set] means
ex m being Nat st $1 = il.(S,m+k) & $2 = p.il.(S,m);
A1: for e being set st e in A ex u being set st P[e,u]
proof
let e be set;
assume e in A;
then consider m being Nat such that
A2: e = il.(S,m+k) & il.(S,m) in dom p;
take p.il.(S,m);
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = A and
A4: for e being set st e in A holds P[e,f.e] from NonUniqFuncEx(A1);
A5: A c= the Instruction-Locations of S
proof
let x be set;
assume x in A;
then ex m being Nat st x = il.(S,m+k) & il.(S,m) in dom p;
hence x in the Instruction-Locations of S;
end;
then A c= the carrier of S by XBOOLE_1:1;
then A6: dom f c= dom the Object-Kind of S by A3,FUNCT_2:def 1;
for x being set st x in dom f holds f.x in (the Object-Kind of S).x
proof
let x be set;
assume
A7: x in dom f;
then consider m being Nat such that
A8: x = il.(S,m+k) and
A9: f.x = p.il.(S,m) by A3,A4;
reconsider y = x as Instruction-Location of S by A3,A5,A7;
A10: (the Object-Kind of S).x = ObjectKind y by AMI_1:def 6
.= the Instructions of S by AMI_1:def 14;
consider s being State of S such that
A11: p c= s by AMI_3:39;
consider j being Nat such that
A12: il.(S,m+k) = il.(S,j+k) and
A13: il.(S,j) in dom p by A3,A7,A8;
j+k = m+k by A12,AMISTD_1:25;
then A14: il.(S,m) in dom p by A13,XCMPLX_1:2;
s.il.(S,m) in the Instructions of S;
hence f.x in (the Object-Kind of S).x by A9,A10,A11,A14,GRFUNC_1:8;
end;
then reconsider f as Element of sproduct the Object-Kind of S
by A6,AMI_1:def 16
;
A15:dom p is finite;
A16:for m1, m2 being Nat st _G(m1) = _G(m2) holds m1 = m2 by AMISTD_1:25;
A is finite from FinMono(A15,A16);
then f is finite by A3,AMI_1:21;
then reconsider f as FinPartState of S by AMI_1:def 24;
take f;
thus dom f = { il.(S,m+k) where m is Nat: il.(S,m) in dom p } by A3;
let m be Nat;
assume il.(S,m) in dom p;
then il.(S,m+k) in A;
then consider j being Nat such that
A17: il.(S,m+k) = il.(S,j+k) and
A18: f.il.(S,m+k) = p.il.(S,j) by A4;
m+k = j+k by A17,AMISTD_1:25;
hence f.il.(S,m+k) = p.il.(S,m) by A18,XCMPLX_1:2;
end;
uniqueness
proof
let IT1, IT2 be FinPartState of S such that
A19: dom IT1 = { il.(S,m+k) where m is Nat: il.(S,m) in dom p } and
A20: for m being Nat st il.(S,m) in dom p holds IT1.il.(S,m+k) = p.il.(S,m)
and
A21: dom IT2 = { il.(S,m+k) where m is Nat: il.(S,m) in dom p } and
A22: for m being Nat st il.(S,m) in dom p holds IT2.il.(S,m+k) = p.il.(S,m);
for x being set st x in { il.(S,m+k) where m is Nat: il.(S,m) in dom p }
holds IT1.x = IT2.x
proof
let x be set;
assume x in { il.(S,m+k) where m is Nat: il.(S,m) in dom p };
then consider m being Nat such that
A23: x = il.(S,m+k) and
A24: il.(S,m) in dom p;
thus IT1.x = p.il.(S,m) by A20,A23,A24
.= IT2.x by A22,A23,A24;
end;
hence IT1=IT2 by A19,A21,FUNCT_1:9;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be FinPartState of S,
k be natural number;
cluster Shift(F,k) -> programmed;
coherence
proof
A1: dom Shift(F,k) = { il.(S,m+k) where m is Nat: il.(S,m) in dom F }
by Def16;
let x be set;
assume x in dom Shift(F,k);
then ex m being Nat st x = il.(S,m+k) & il.(S,m) in dom F by A1;
hence x in the Instruction-Locations of S;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be empty FinPartState of S,
k be natural number;
cluster Shift(F,k) -> empty;
coherence
proof
A1: dom Shift(F,k) = { il.(S,m+k) where m is Nat: il.(S,m) in dom F }
by Def16;
assume Shift(F,k) is non empty;
then reconsider f = Shift(F,k) as non empty Function;
dom f is non empty;
then consider a being set such that
A2: a in dom Shift(F,k) by XBOOLE_0:def 1;
ex m being Nat st a = il.(S,m+k) & il.(S,m) in dom F by A1,A2;
hence thesis;
end;
end;
definition
let N be with_non-empty_elements set,
S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be non empty programmed FinPartState of S,
k be natural number;
cluster Shift(F,k) -> non empty;
coherence
proof
A1: dom Shift(F,k) = { il.(S,m+k) where m is Nat: il.(S,m) in dom F }
by Def16;
consider a being set such that
A2: a in dom F by XBOOLE_0:def 1;
dom F c= the Instruction-Locations of S by AMI_3:def 13;
then reconsider a as Instruction-Location of S by A2;
consider m being natural number such that
A3: a = il.(S,m) by AMISTD_1:26;
reconsider m as Element of NAT by ORDINAL2:def 21;
il.(S,m+k) in dom Shift(F,k) by A1,A2,A3;
hence thesis by Lm1;
end;
end;
theorem Th40:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being programmed FinPartState of S
holds Shift(F,0) = F
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be programmed FinPartState of S;
A1: dom F c= the Instruction-Locations of S by AMI_3:def 13;
A2: dom F = { il.(S,m+0) where m is Nat: il.(S,m) in dom F }
proof
hereby
let a be set;
assume
A3: a in dom F;
then consider k being natural number such that
A4: a = il.(S,k) by A1,AMISTD_1:26;
reconsider k as Element of NAT by ORDINAL2:def 21;
a = il.(S,k+0) by A4;
hence a in { il.(S,m+0) where m is Nat: il.(S,m) in dom F } by A3;
end;
let a be set;
assume a in { il.(S,m+0) where m is Nat: il.(S,m) in dom F };
then ex m being Nat st a = il.(S,m+0) & il.(S,m) in dom F;
hence thesis;
end;
for m being Nat st il.(S,m) in dom F holds F.il.(S,m+0) = F.il.(S,m);
hence thesis by A2,Def16;
end;
theorem Th41:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being FinPartState of S,
k being natural number st k > 0
holds not il.(S,0) in dom Shift(F,k)
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be FinPartState of S,
k be natural number such that
A1: k > 0 and
A2: il.(S,0) in dom Shift(F,k);
dom Shift(F,k) = { il.(S,m+k) where m is Nat: il.(S,m) in dom F }
by Def16;
then consider m being Nat such that
A3: il.(S,0) = il.(S,m+k) and
il.(S,m) in dom F by A2;
m+k=0 by A3,AMISTD_1:25;
hence contradiction by A1,NAT_1:23;
end;
theorem
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being FinPartState of S
holds Shift(Shift(F,m),k) = Shift(F,m+k)
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be FinPartState of S;
set A = {il.(S,l+m) where l is Nat: il.(S,l) in dom F};
A1: dom Shift(F,m) = A by Def16;
{il.(S,r+k) where r is Nat: il.(S,r) in A} =
{il.(S,q+(m+k)) where q is Nat: il.(S,q) in dom F}
proof
hereby
let x be set;
assume x in {il.(S,r+k) where r is Nat: il.(S,r) in A };
then consider r being Nat such that
A2: x = il.(S,r+k) and
A3: il.(S,r) in A;
consider l being Nat such that
A4: il.(S,r) = il.(S,l+m) and
A5: il.(S,l) in dom F by A3;
r = l+m by A4,AMISTD_1:25;
then x = il.(S,l+(m+k)) by A2,XCMPLX_1:1;
hence x in {il.(S,q+(m+k)) where q is Nat: il.(S,q) in dom F} by A5;
end;
let x be set;
assume x in {il.(S,q+(m+k)) where q is Nat: il.(S,q) in dom F};
then consider q being Nat such that
A6: x = il.(S,q+(m+k)) and
A7: il.(S,q) in dom F;
A8: x = il.(S,q+m+k) by A6,XCMPLX_1:1;
A9: q+m is Nat by ORDINAL2:def 21;
il.(S,q+m) in A by A7;
hence x in {il.(S,r+k) where r is Nat: il.(S,r) in A} by A8,A9;
end;
then A10: dom Shift(Shift(F,m),k)
= {il.(S,l+(m+k)) where l is Nat: il.(S,l) in dom F} by A1,Def16;
now
let l be Nat;
assume
A11: il.(S,l) in dom F;
then A12: il.(S,l+m) in dom Shift(F,m) by A1;
A13: l+m is Nat by ORDINAL2:def 21;
thus Shift(Shift(F,m),k).il.(S,l+(m+k))
= Shift(Shift(F,m),k).il.(S,l+m+k) by XCMPLX_1:1
.= Shift(F,m).il.(S,l+m) by A12,A13,Def16
.= F.il.(S,l) by A11,Def16;
end;
hence Shift(Shift(F,m),k) = Shift(F,m+k) by A10,Def16;
end;
theorem Th43:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being programmed FinPartState of S
holds dom F,dom Shift(F,k) are_equipotent
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be programmed FinPartState of S;
A1: dom F c= the Instruction-Locations of S by AMI_3:def 13;
defpred P[set,set] means
ex il being Instruction-Location of S st $1 = il & $2 = il.(S,k+locnum il);
A2: for e being set st e in dom F ex u being set st P[e,u]
proof
let e be set;
assume e in dom F;
then reconsider e as Instruction-Location of S by A1;
take il.(S,k+locnum e), e;
thus thesis;
end;
consider f being Function such that
A3: dom f = dom F and
A4: for x being set st x in dom F holds P[x,f.x] from NonUniqFuncEx(A2);
take f;
hereby
let x1, x2 be set such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f.x1 = f.x2;
consider i1 being Instruction-Location of S such that
A8: x1 = i1 and
A9: f.x1 = il.(S,k+locnum i1) by A3,A4,A5;
consider i2 being Instruction-Location of S such that
A10: x2 = i2 and
A11: f.x2 = il.(S,k+locnum i2) by A3,A4,A6;
k+locnum i1 = k+locnum i2 by A7,A9,A11,AMISTD_1:25;
then locnum i1 = locnum i2 by XCMPLX_1:2;
hence x1 = x2 by A8,A10,AMISTD_1:27;
end;
thus dom f = dom F by A3;
A12: dom Shift(F,k) = { il.(S,m+k) where m is Nat: il.(S,m) in dom F }
by Def16;
hereby
let y be set;
assume y in rng f;
then consider x being set such that
A13: x in dom f and
A14: f.x = y by FUNCT_1:def 5;
consider il being Instruction-Location of S such that
A15: x = il & f.x = il.(S,k+locnum il) by A3,A4,A13;
consider a being natural number such that
A16: il = il.(S,a) by AMISTD_1:26;
reconsider a as Element of NAT by ORDINAL2:def 21;
a = locnum il by A16,AMISTD_1:def 13;
hence y in dom Shift(F,k) by A3,A12,A13,A14,A15,A16;
end;
let y be set;
assume y in dom Shift(F,k);
then consider m being Nat such that
A17: y = il.(S,m+k) and
A18: il.(S,m) in dom F by A12;
consider il being Instruction-Location of S such that
A19: il.(S,m) = il & f.il.(S,m) = il.(S,k+locnum il) by A4,A18;
m = locnum il by A19,AMISTD_1:def 13;
hence y in rng f by A3,A17,A18,A19,FUNCT_1:def 5;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of S;
attr I is IC-good means :Def17:
for k being natural number,
s1, s2 being State of S
st s2 = s1 +* (IC S .--> (IC s1 + k))
holds IC Exec(I,s1) + k = IC Exec(IncAddr(I,k), s2);
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
attr S is IC-good means :Def18:
for I being Instruction of S holds I is IC-good;
end;
definition
let N be with_non-empty_elements set,
S be non void AMI-Struct over N,
I be Instruction of S;
attr I is Exec-preserving means :Def19:
for s1, s2 being State of S
st s1, s2 equal_outside the Instruction-Locations of S
holds Exec(I,s1), Exec(I,s2)
equal_outside the Instruction-Locations of S;
end;
definition
let N be with_non-empty_elements set,
S be non void AMI-Struct over N;
attr S is Exec-preserving means :Def20:
for I being Instruction of S holds I is Exec-preserving;
end;
theorem Th44:
for S being regular standard without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I being Instruction of S st I is sequential
holds I is IC-good
proof
let S be regular standard without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be Instruction of S such that
A1: I is sequential;
let k be natural number,
s1, s2 be State of S such that
A2: s2 = s1 +* (IC S .--> (IC s1 + k));
A3: I is ins-loc-free by A1,Th24;
dom (IC S .--> (IC s1 + k)) = {IC S} by CQC_LANG:5;
then A4: IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
A5: IC s2 = s2.IC S by AMI_1:def 15
.= (IC S .--> (IC s1 + k)).IC S by A2,A4,FUNCT_4:14
.= IC s1 + k by CQC_LANG:6
.= il.(S,locnum IC s1 + k) by AMISTD_1:def 14;
A6: IC Exec(I, s2) = Exec(I, s2).IC S by AMI_1:def 15
.= NextLoc IC s2 by A1,AMISTD_1:def 16
.= il.(S,locnum IC s1 + k) + 1 by A5,AMISTD_1:def 15
.= il.(S,locnum il.(S,locnum IC s1 + k) + 1) by AMISTD_1:def 14
.= il.(S,locnum IC s1 + k + 1) by AMISTD_1:def 13
.= il.(S,locnum IC s1 + 1 + k) by XCMPLX_1:1;
A7: IC Exec(I,s1) = Exec(I,s1).IC S by AMI_1:def 15
.= NextLoc IC s1 by A1,AMISTD_1:def 16
.= il.(S,locnum IC s1 + 1) by AMISTD_1:34;
thus IC Exec(I,s1) + k = il.(S,locnum IC Exec(I,s1) + k) by AMISTD_1:def 14
.= IC Exec(I,s2) by A6,A7,AMISTD_1:def 13
.= IC Exec(IncAddr(I,k), s2) by A3,Th29;
end;
definition
let N be with_non-empty_elements set,
S be regular standard without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster sequential -> IC-good Instruction of S;
coherence by Th44;
end;
theorem Th45:
for S being regular standard without_implicit_jumps realistic
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I being Instruction of S st I is halting
holds I is IC-good
proof
let S be regular standard without_implicit_jumps realistic
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be Instruction of S such that
A1: I is halting;
let k be natural number,
s1, s2 be State of S such that
A2: s2 = s1 +* (IC S .--> (IC s1 + k));
A3: I is ins-loc-free by A1,Th23;
dom (IC S .--> (IC s1 + k)) = {IC S} by CQC_LANG:5;
then A4: IC S in dom (IC S .--> (IC s1 + k)) by TARSKI:def 1;
thus IC Exec(I,s1) + k = IC s1 + k by A1,AMI_1:def 8
.= (IC S .--> (IC s1 + k)).IC S by CQC_LANG:6
.= s2.IC S by A2,A4,FUNCT_4:14
.= IC s2 by AMI_1:def 15
.= IC Exec(I,s2) by A1,AMI_1:def 8
.= IC Exec(IncAddr(I,k), s2) by A3,Th29;
end;
definition
let N be with_non-empty_elements set,
S be regular standard without_implicit_jumps realistic
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
cluster halting -> IC-good Instruction of S;
coherence by Th45;
end;
theorem Th46:
for S being non void AMI-Struct over N,
I being Instruction of S st I is halting
holds I is Exec-preserving
proof
let S be non void AMI-Struct over N,
I be Instruction of S such that
A1: for s being State of S holds Exec(I,s) = s;
let s1, s2 be State of S such that
A2: s1, s2 equal_outside the Instruction-Locations of S;
Exec(I,s1) = s1 & Exec(I,s2) = s2 by A1;
hence thesis by A2;
end;
definition
let N be with_non-empty_elements set,
S be non void AMI-Struct over N;
cluster halting -> Exec-preserving Instruction of S;
coherence by Th46;
end;
definition
let N be with_non-empty_elements set;
cluster STC N -> IC-good Exec-preserving;
coherence
proof
thus STC N is IC-good
proof
let I be Instruction of STC N,
k be natural number,
s1, s2 be State of STC N such that
A1: s2 = s1 +* (IC STC N .--> (IC s1 + k));
{IC STC N} = dom (IC STC N .--> (IC s1 + k)) by CQC_LANG:5;
then A2: IC STC N in dom (IC STC N .--> (IC s1 + k)) by TARSKI:def 1;
A3: IC Exec(IncAddr(I,k), s2) = Exec(IncAddr(I,k), s2).IC STC N
by AMI_1:def 15;
A4: IC s2 = s2.IC STC N by AMI_1:def 15
.= (IC STC N .--> (IC s1 + k)).IC STC N by A1,A2,FUNCT_4:14
.= IC s1 + k by CQC_LANG:6;
per cases by AMISTD_1:22;
suppose
A5: InsCode I = 1;
then A6: InsCode IncAddr(I,k) = 1 by Def14;
Exec(I,s1).IC STC N = NextLoc IC s1 by A5,AMISTD_1:38
.= il.(STC N,locnum IC s1 + 1) by AMISTD_1:34;
then A7: locnum IC Exec(I,s1) = locnum il.(STC N,locnum IC s1 + 1)
by AMI_1:def 15
.= locnum IC s1 + 1 by AMISTD_1:def 13;
thus IC Exec(I,s1) + k = il.(STC N, locnum IC Exec(I,s1) + k)
by AMISTD_1:def 14
.= locnum IC Exec(I,s1) + k by AMISTD_1:37
.= locnum IC s1 + k + 1 by A7,XCMPLX_1:1
.= locnum (IC s1 + k) + 1 by AMISTD_1:33
.= il.(STC N, locnum IC s2 + 1) by A4,AMISTD_1:37
.= NextLoc IC s2 by AMISTD_1:34
.= IC Exec(IncAddr(I,k), s2) by A3,A6,AMISTD_1:38;
suppose InsCode I = 0;
then A8: I is halting by AMISTD_1:20;
then I is ins-loc-free by Th23;
then A9: IncAddr(I,k) is halting by A8,Th29;
thus IC Exec(I,s1) + k = IC s1 + k by A8,AMI_1:def 8
.= IC Exec(IncAddr(I,k), s2) by A4,A9,AMI_1:def 8;
end;
let I be Instruction of STC N;
per cases by AMISTD_1:22;
suppose InsCode I = 1;
then A10: I`1 = 1 by AMI_5:def 1;
the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
then A11: I = [0,0] or I = [1,0] by TARSKI:def 2;
let s1, s2 be State of STC N such that
A12: s1, s2 equal_outside the Instruction-Locations of STC N;
consider f being Function of product the Object-Kind of STC N,
product the Object-Kind of STC N such that
A13: for s being Element of product the Object-Kind of STC N
holds f.s = s+*({NAT}-->succ(s.NAT)) and
A14: the Execution of STC N
= ({[1,0]} --> f) +* ({[0,0]} --> id product the Object-Kind of STC N)
by AMISTD_1:def 11;
[0,0] <> [1,0] by ZFMISC_1:33;
then not I in {[0,0]} by A10,A11,MCART_1:7,TARSKI:def 1;
then not I in dom ({[0,0]} --> id product the Object-Kind of STC N)
by FUNCOP_1:19;
then A15: (the Execution of STC N).I = ({[1,0]} --> f).I by A14,FUNCT_4:12;
A16: I in {[1,0]} by A10,A11,MCART_1:7,TARSKI:def 1;
A17: Exec(I,s1) = (the Execution of STC N).I.s1 by AMI_1:def 7
.= f.s1 by A15,A16,FUNCOP_1:13
.= s1+*({NAT}-->succ(s1.NAT)) by A13;
A18: Exec(I,s2) = (the Execution of STC N).I.s2 by AMI_1:def 7
.= f.s2 by A15,A16,FUNCOP_1:13
.= s2+*({NAT}-->succ(s2.NAT)) by A13;
dom Exec(I,s1) = dom the Object-Kind of STC N by CARD_3:18;
then A19: dom Exec(I,s1) = dom Exec(I,s2) by CARD_3:18;
A20: dom Exec(I,s1) \ the Instruction-Locations of STC N c= dom Exec(I,s1)
by XBOOLE_1:36;
for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of STC
N
holds Exec(I,s1).x = Exec(I,s2).x
proof
let x be set;
assume
A21: x in dom Exec(I,s1) \ the Instruction-Locations of STC N;
then not x in the Instruction-Locations of STC N by XBOOLE_0:def 4;
then A22: not x in NAT by AMISTD_1:def 11;
A23: IC STC N = the Instruction-Counter of STC N by AMI_1:def 5;
then A24: s1.NAT = s1.IC STC N by AMISTD_1:def 11
.= IC s1 by AMI_1:def 15
.= IC s2 by A12,SCMFSA6A:29
.= s2.IC STC N by AMI_1:def 15
.= s2.NAT by A23,AMISTD_1:def 11;
x in dom Exec(I,s1) by A21,XBOOLE_0:def 4;
then x in the carrier of STC N by AMI_3:36;
then x in NAT \/ {NAT} by AMISTD_1:def 11;
then A25: x in {NAT} by A22,XBOOLE_0:def 2;
then A26: x in dom ({NAT}-->succ(s2.NAT)) by FUNCOP_1:19;
x in dom ({NAT}-->succ(s1.NAT)) by A25,FUNCOP_1:19;
hence Exec(I,s1).x = ({NAT}-->succ(s1.NAT)).x by A17,FUNCT_4:14
.= Exec(I,s2).x by A18,A24,A26,FUNCT_4:14;
end;
hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of STC N) =
Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of STC N)
by A19,A20,SCMFSA6A:9;
suppose InsCode I = 0;
then I is halting by AMISTD_1:20;
hence thesis by Th46;
end;
end;
definition
let N be with_non-empty_elements set;
cluster halting realistic steady-programmed programmable
with_explicit_jumps without_implicit_jumps
IC-good Exec-preserving
(regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)));
existence
proof
take STC N;
thus thesis;
end;
end;
definition
let N be with_non-empty_elements set,
S be IC-good (regular standard
(IC-Ins-separated definite (non empty non void AMI-Struct over N)));
cluster -> IC-good Instruction of S;
coherence by Def18;
end;
definition
let N be with_non-empty_elements set,
S be Exec-preserving (non void AMI-Struct over N);
cluster -> Exec-preserving Instruction of S;
coherence by Def20;
end;
definition
let N be with_non-empty_elements set;
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F be non empty programmed FinPartState of S;
func CutLastLoc F -> FinPartState of S equals :Def21:
F \ ( LastLoc F .--> F.LastLoc F );
coherence by Th11;
end;
Lm8:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being non empty programmed FinPartState of S
holds CutLastLoc F c= F
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be non empty programmed FinPartState of S;
CutLastLoc F = F \ ( LastLoc F .--> F.LastLoc F ) by Def21;
hence thesis by XBOOLE_1:36;
end;
theorem Th47:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being non empty programmed FinPartState of S
holds dom CutLastLoc F = (dom F) \ {LastLoc F}
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be non empty programmed FinPartState of S;
A1: CutLastLoc F = F \ ( LastLoc F .--> F.LastLoc F ) by Def21;
A2: dom (LastLoc F .--> (F.LastLoc F)) = {LastLoc F} by CQC_LANG:5;
reconsider R = {[LastLoc F, F.LastLoc F]} as Relation by RELAT_1:4;
A3: R = LastLoc F .--> (F.LastLoc F) by AMI_1:19;
then A4: dom R = {LastLoc F} by CQC_LANG:5;
thus dom CutLastLoc F c= (dom F) \ {LastLoc F}
proof
let x be set;
assume x in dom CutLastLoc F;
then consider y being set such that
A5: [x,y] in F \ R by A1,A3,RELAT_1:def 4;
A6: [x,y] in F & not [x,y] in R by A5,XBOOLE_0:def 4;
then A7: x in dom F by RELAT_1:def 4;
per cases by A6,TARSKI:def 1;
suppose x <> LastLoc F;
then not x in dom R by A4,TARSKI:def 1;
hence thesis by A2,A3,A7,XBOOLE_0:def 4;
suppose
A8: y <> F.LastLoc F;
now
assume x in dom R;
then x = LastLoc F by A4,TARSKI:def 1;
hence contradiction by A6,A8,FUNCT_1:8;
end;
hence thesis by A2,A3,A7,XBOOLE_0:def 4;
end;
thus thesis by A1,A2,RELAT_1:15;
end;
theorem Th48:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being non empty programmed FinPartState of S
holds dom F = dom CutLastLoc F \/ {LastLoc F}
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be non empty programmed FinPartState of S;
LastLoc F in dom F by AMISTD_1:51;
then A1: {LastLoc F} c= dom F by ZFMISC_1:37;
dom CutLastLoc F = (dom F) \ {LastLoc F} by Th47;
hence thesis by A1,XBOOLE_1:45;
end;
definition
let N be with_non-empty_elements set;
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F be non empty trivial programmed FinPartState of S;
cluster CutLastLoc F -> empty;
coherence
proof
A1: CutLastLoc F = F \ ( LastLoc F .--> F.LastLoc F ) by Def21;
LastLoc F in dom F by AMISTD_1:51;
then A2: [LastLoc F,F.LastLoc F] in F by FUNCT_1:def 4;
assume not thesis;
then consider a being set such that
A3: a in CutLastLoc F by XBOOLE_0:def 1;
a in F by A1,A3,XBOOLE_0:def 4;
then A4: a = [LastLoc F,F.LastLoc F] by A2,YELLOW_8:def 1;
not a in LastLoc F .--> F.LastLoc F by A1,A3,XBOOLE_0:def 4;
then not a in {[LastLoc F,F.LastLoc F]} by AMI_1:19;
hence thesis by A4,TARSKI:def 1;
end;
end;
definition
let N be with_non-empty_elements set;
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F be non empty programmed FinPartState of S;
cluster CutLastLoc F -> programmed;
coherence
proof
CutLastLoc F = F \ ( LastLoc F .--> F.LastLoc F ) by Def21;
hence thesis by Th12;
end;
end;
definition
let N be with_non-empty_elements set;
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F be lower non empty programmed FinPartState of S;
cluster CutLastLoc F -> lower;
coherence
proof
set G = CutLastLoc F;
per cases;
suppose G is empty;
then reconsider H = G as empty FinPartState of S;
H is lower;
hence thesis;
suppose G is non empty;
then reconsider G as non empty FinPartState of S;
G is lower
proof
let l be Instruction-Location of S such that
A1: l in dom G;
let m be Instruction-Location of S such that
A2: m <= l;
consider M being finite non empty natural-membered set such that
A3: M = { locnum w where w is Element of the Instruction-Locations of S
: w in dom F } and
A4: LastLoc F = il.(S, max M) by AMISTD_1:def 21;
reconsider R = {[LastLoc F, F.LastLoc F]} as Relation by RELAT_1:4;
R = LastLoc F .--> (F.LastLoc F) by AMI_1:19;
then A5: dom R = {LastLoc F} by CQC_LANG:5;
then A6: dom F \ dom R = dom G by Th47;
then A7: l in dom F by A1,XBOOLE_0:def 4;
then A8: m in dom F by A2,AMISTD_1:def 20;
locnum l in M by A3,A7;
then A9: locnum l <= max M by PRE_CIRC:def 1;
now
assume m = LastLoc F;
then LastLoc F <= il.(S,locnum l) by A2,AMISTD_1:def 13;
then max M <= locnum l by A4,AMISTD_1:28;
then il.(S,locnum l) = il.(S,max M) by A9,AXIOMS:21;
then LastLoc F in dom G by A1,A4,AMISTD_1:def 13;
then not LastLoc F in {LastLoc F} by A5,A6,XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
then not m in {LastLoc F} by TARSKI:def 1;
hence m in dom G by A5,A6,A8,XBOOLE_0:def 4;
end;
hence thesis;
end;
end;
theorem Th49:
for S being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being non empty programmed FinPartState of S
holds card CutLastLoc F = card F - 1
proof
let S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be non empty programmed FinPartState of S;
A1: LastLoc F .--> F.LastLoc F c= F
proof
let a, b be set;
assume [a,b] in LastLoc F .--> F.LastLoc F;
then [a,b] in {[LastLoc F,F.LastLoc F]} by AMI_1:19;
then A2: [a,b] = [LastLoc F,F.LastLoc F] by TARSKI:def 1;
LastLoc F in dom F by AMISTD_1:51;
hence [a,b] in F by A2,FUNCT_1:def 4;
end;
CutLastLoc F = F \ ( LastLoc F .--> F.LastLoc F ) by Def21;
hence card CutLastLoc F = card F - card (LastLoc F .--> F.LastLoc F)
by A1,CARD_2:63
.= card F - card {[LastLoc F,F.LastLoc F]} by AMI_1:19
.= card F - 1 by CARD_1:79;
end;
theorem Th50:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being lower non empty programmed FinPartState of S,
G being non empty programmed FinPartState of S
holds dom CutLastLoc F misses dom Shift(IncAddr(G,card F -' 1),card F -' 1)
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower non empty programmed FinPartState of S,
G be non empty programmed FinPartState of S;
set k = card F -' 1;
assume not thesis;
then consider il being set such that
A1: il in dom CutLastLoc F /\ dom Shift(IncAddr(G,k),k) by XBOOLE_0:4;
A2: il in dom CutLastLoc F by A1,XBOOLE_0:def 3;
A3: il in dom Shift(IncAddr(G,k),k) by A1,XBOOLE_0:def 3;
dom Shift(IncAddr(G,k),k) = { il.(S,m+k) where m is Nat:
il.(S,m) in dom IncAddr(G,k) } by Def16;
then consider m being Nat such that
A4: il = il.(S,m+k) and
il.(S,m) in dom IncAddr(G,k) by A3;
reconsider f = CutLastLoc F as non empty programmed FinPartState of S
by A2,Lm1;
il.(S,m+k) <= LastLoc f by A2,A4,AMISTD_1:53;
then il.(S,m+k) <= il.(S, card f -' 1) by AMISTD_1:55;
then A5: m+k <= card f -' 1 by AMISTD_1:28;
A6: card f = card F - 1 by Th49
.= card F -' 1 by Th4;
per cases;
suppose k - 1 >= 0;
then m + k <= k - 1 by A5,A6,BINARITH:def 3;
then m + k - k <= k - 1 - k by REAL_1:49;
then m + (k - k) <= k - 1 - k by XCMPLX_1:29;
then m + 0 <= k - 1 - k by XCMPLX_1:14;
then m <= k - k - 1 by XCMPLX_1:21;
then m <= 0-1 by XCMPLX_1:14;
hence thesis by Lm3;
suppose k - 1 < 0;
then m + k = 0 or m + k < 0 by A5,A6,BINARITH:def 3;
then m = 0 & k = 0 by NAT_1:18,23;
hence thesis by A6,CARD_2:59;
end;
theorem Th51:
for S being standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being unique-halt (lower non empty programmed FinPartState of S),
I being Instruction-Location of S st I in dom CutLastLoc F
holds (CutLastLoc F).I <> halt S
proof
let S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be unique-halt (lower non empty programmed FinPartState of S),
I be Instruction-Location of S such that
A1: I in dom CutLastLoc F and
A2: (CutLastLoc F).I = halt S;
A3: CutLastLoc F c= F by Lm8;
then A4: dom CutLastLoc F c= dom F by GRFUNC_1:8;
F.I = halt S by A1,A2,A3,GRFUNC_1:8;
then A5: I = LastLoc F by A1,A4,AMISTD_1:def 23;
dom CutLastLoc F = (dom F) \ {LastLoc F} by Th47;
then not I in {LastLoc F} by A1,XBOOLE_0:def 4;
hence thesis by A5,TARSKI:def 1;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G be non empty programmed FinPartState of S;
func F ';' G -> FinPartState of S equals :Def22:
CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1);
coherence;
end;
Lm9:
now
let N be with_non-empty_elements set;
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F, G be non empty programmed FinPartState of S;
thus dom (F ';' G)
= dom (CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1)) by Def22
.= dom CutLastLoc F \/ dom Shift(IncAddr(G,card F -' 1),card F -' 1)
by FUNCT_4:def 1;
end;
definition
let N be with_non-empty_elements set,
S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G be non empty programmed FinPartState of S;
cluster F ';' G -> non empty programmed;
coherence
proof
F ';' G = CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1)
by Def22;
hence thesis;
end;
end;
theorem Th52:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being lower non empty programmed FinPartState of S,
G being non empty programmed FinPartState of S
holds card (F ';' G) = card F + card G - 1 &
card (F ';' G) = card F + card G -' 1
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be lower non empty programmed FinPartState of S,
G be non empty programmed FinPartState of S;
set k = card F -' 1;
dom IncAddr(G,k),dom Shift(IncAddr(G,k),k) are_equipotent by Th43;
then A1: IncAddr(G,k),Shift(IncAddr(G,k),k) are_equipotent by Th1;
A2: dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
thus
A3: card (F ';' G)
= card (CutLastLoc F +* Shift(IncAddr(G,k),k)) by Def22
.= card CutLastLoc F + card Shift(IncAddr(G,k),k) by A2,Th2
.= card CutLastLoc F + card IncAddr(G,k) by A1,CARD_1:21
.= card CutLastLoc F + card dom IncAddr(G,k) by PRE_CIRC:21
.= card CutLastLoc F + card dom G by Def15
.= card CutLastLoc F + card G by PRE_CIRC:21
.= card F - 1 + card G by Th49
.= card F + card G - 1 by XCMPLX_1:29;
card F <> 0 & card G <> 0 by CARD_2:59;
then card F >= 1 & card G >= 1 by RLVECT_1:99;
then card F + card G >= 1+1 by REAL_1:55;
then card F + card G - 1 >= 2 - 1 by REAL_1:49;
then card F + card G - 1 >= 0 by AXIOMS:22;
hence thesis by A3,BINARITH:def 3;
end;
definition
let N be with_non-empty_elements set;
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F, G be lower non empty programmed FinPartState of S;
cluster F ';' G -> lower;
coherence
proof
set P = F ';' G;
A1: P = CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1) by Def22;
let n be Instruction-Location of S such that
A2: n in dom P;
let f be Instruction-Location of S such that
A3: f <= n;
set k = card F -' 1;
A4: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by A1,FUNCT_4:def 1;
per cases by A2,A4,XBOOLE_0:def 2;
suppose n in dom CutLastLoc F;
then f in dom CutLastLoc F by A3,AMISTD_1:def 20;
hence f in dom P by A4,XBOOLE_0:def 2;
suppose n in dom Shift(IncAddr(G,k),k);
then n in { il.(S,w+k) where w is Nat:
il.(S,w) in dom IncAddr(G,k) } by Def16;
then consider m being Nat such that
A5: n = il.(S,m+k) and
A6: il.(S,m) in dom IncAddr(G,k);
A7: locnum f <= locnum n by A3,AMISTD_1:29;
A8: il.(S,m) in dom G by A6,Def15;
now per cases;
case
A9: locnum f < k;
then locnum f < card F - 1 by Th4;
then 1+locnum f < 1 + (card F - 1) by REAL_1:53;
then 1+locnum f < 1 + card F - 1 by XCMPLX_1:29;
then 1+locnum f < card F + (1 - 1) by XCMPLX_1:29;
then A10: il.(S,1+locnum f) in dom F by AMISTD_1:50;
locnum f <= 1+locnum f by NAT_1:29;
then il.(S,locnum f) <= il.(S,1+locnum f) by AMISTD_1:28;
then il.(S,locnum f) in dom F by A10,AMISTD_1:def 20;
then A11: f in dom F by AMISTD_1:def 13;
now
assume f = LastLoc F;
then f = il.(S,k) by AMISTD_1:55;
hence contradiction by A9,AMISTD_1:def 13;
end;
then not f in {LastLoc F} by TARSKI:def 1;
then f in (dom F) \ {LastLoc F} by A11,XBOOLE_0:def 4;
hence f in dom CutLastLoc F by Th47;
case locnum f >= k;
then consider l1 being Nat such that
A12: locnum f = k + l1 by NAT_1:28;
A13: dom Shift(IncAddr(G,k),k) =
{ il.(S,w+k) where w is Nat: il.(S,w) in dom IncAddr(G,k) } by Def16;
A14: f = il.(S,l1+k) by A12,AMISTD_1:def 13;
locnum f <= k+m by A5,A7,AMISTD_1:def 13;
then l1 <= m by A12,REAL_1:53;
then il.(S,l1) <= il.(S,m) by AMISTD_1:28;
then il.(S,l1) in dom G by A8,AMISTD_1:def 20;
then il.(S,l1) in dom IncAddr(G,k) by Def15;
hence f in dom Shift(IncAddr(G,k),k) by A13,A14;
end;
hence f in dom P by A4,XBOOLE_0:def 2;
end;
end;
theorem Th53:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G being lower non empty programmed FinPartState of S
holds dom F c= dom (F ';' G)
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G be lower non empty programmed FinPartState of S;
set P = F ';' G;
A1: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,card F -' 1),card F -' 1)
by Lm9;
A2: dom F = dom CutLastLoc F \/ {LastLoc F} by Th48;
let x be set;
assume
A3: x in dom F;
per cases by A2,A3,XBOOLE_0:def 2;
suppose x in dom CutLastLoc F;
hence x in dom P by A1,XBOOLE_0:def 2;
suppose
A4: x in {LastLoc F};
then reconsider f = x as Instruction-Location of S by TARSKI:def 1;
x = LastLoc F by A4,TARSKI:def 1;
then A5: locnum f = locnum il.(S,card F -' 1) by AMISTD_1:55
.= card F -' 1 by AMISTD_1:def 13
.= card F - 1 + 0 by Th4;
A6: card P = card F + card G - 1 by Th52
.= card F - 1 + card G by XCMPLX_1:29;
0 <> card G by CARD_2:59;
then 0 < card G by NAT_1:19;
then locnum f < card P by A5,A6,REAL_1:53;
then il.(S,locnum f) in dom P by AMISTD_1:50;
hence x in dom P by AMISTD_1:def 13;
end;
theorem Th54:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G being lower non empty programmed FinPartState of S
holds CutLastLoc F c= CutLastLoc (F ';' G)
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G be lower non empty programmed FinPartState of S;
set k = card F -' 1;
set P = F ';' G;
P = CutLastLoc F +* Shift(IncAddr(G,k),k) by Def22;
then A1: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by FUNCT_4:def 1
;
A2: dom CutLastLoc F = { il.(S,m) where m is Nat: m < card CutLastLoc F }
by Th15;
A3: card CutLastLoc P = card P - 1 by Th49
.= card F + card G - 1 - 1 by Th52
.= card F - 1 + card G - 1 by XCMPLX_1:29
.= card F - 1 + (card G - 1) by XCMPLX_1:29;
A4: for m being Nat st m < card CutLastLoc F holds m < card CutLastLoc P
proof
let m be Nat such that
A5: m < card CutLastLoc F;
A6: card CutLastLoc F = card F - 1 by Th49;
0 <> card G by CARD_2:59;
then 1 <= card G by RLVECT_1:99;
then 1 - 1 <= card G - 1 by REAL_1:49;
then card F - 1 + 0 <= card F - 1 + (card G - 1) by AXIOMS:24;
hence m < card CutLastLoc P by A3,A5,A6,AXIOMS:22;
end;
A7: dom CutLastLoc F c= dom CutLastLoc P
proof
let x be set;
assume x in dom CutLastLoc F;
then consider m being Nat such that
A8: x = il.(S,m) and
A9: m < card CutLastLoc F by A2;
m < card CutLastLoc P by A4,A9;
hence x in dom CutLastLoc P by A8,AMISTD_1:50;
end;
for x being set st x in dom CutLastLoc F holds
(CutLastLoc F).x = (CutLastLoc P).x
proof
let x be set;
assume
A10: x in dom CutLastLoc F;
then consider m being Nat such that
A11: x = il.(S,m) and
A12: m < card CutLastLoc F by A2;
A13: CutLastLoc P = P \ ( LastLoc P .--> P.LastLoc P ) by Def21;
A14: dom Shift(IncAddr(G,k),k) = { il.(S,w+k) where w is Nat:
il.(S,w) in dom IncAddr(G,k) } by Def16;
A15: now
assume x in dom Shift(IncAddr(G,k),k);
then consider w being Nat such that
A16: x = il.(S,w+k) and
il.(S,w) in dom IncAddr(G,k) by A14;
m < card F - 1 by A12,Th49;
then A17: m < k by Th4;
m = w+k by A11,A16,AMISTD_1:25;
hence contradiction by A17,NAT_1:29;
end;
A18: x in dom P by A1,A10,XBOOLE_0:def 2;
now
assume x = LastLoc P;
then il.(S,m) = il.(S,card P -' 1) by A11,AMISTD_1:55;
then A19: m = card P -' 1 by AMISTD_1:25
.= card P - 1 by Th4;
card CutLastLoc P = card P - 1 by Th49;
hence contradiction by A4,A12,A19;
end;
then not x in {LastLoc P} by TARSKI:def 1;
then not x in dom ( LastLoc P .--> P.LastLoc P ) by CQC_LANG:5;
then x in dom P \ dom ( LastLoc P .--> P.LastLoc P ) by A18,XBOOLE_0:def
4;
hence (CutLastLoc P).x = P.x by A13,Th3
.= (CutLastLoc F +* Shift(IncAddr(G,k),k)).x by Def22
.= (CutLastLoc F).x by A15,FUNCT_4:12;
end;
hence CutLastLoc F c= CutLastLoc P by A7,GRFUNC_1:8;
end;
theorem Th55:
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G being lower non empty programmed FinPartState of S
holds (F ';' G).LastLoc F = IncAddr(G,card F -' 1).il.(S,0)
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G be lower non empty programmed FinPartState of S;
set k = card F -' 1;
A1: LastLoc F = il.(S,0+k) by AMISTD_1:55;
A2: il.(S,0) in dom IncAddr(G,k) by AMISTD_1:49;
dom Shift(IncAddr(G,k),k) =
{il.(S,m+k) where m is Nat: il.(S,m) in dom IncAddr(G,k)} by Def16;
then A3: LastLoc F in dom Shift(IncAddr(G,k),k) by A1,A2;
thus (F ';' G).LastLoc F
= (CutLastLoc F +* Shift(IncAddr(G,k),k)).LastLoc F by Def22
.= (Shift(IncAddr(G,k),k)).LastLoc F by A3,FUNCT_4:14
.= IncAddr(G,k).il.(S,0) by A1,A2,Def16;
end;
theorem
for S being regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G being lower non empty programmed FinPartState of S,
f being Instruction-Location of S st locnum f < card F - 1
holds IncAddr(F,card F -' 1).f = IncAddr(F ';' G, card F -' 1).f
proof
let S be regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F, G be lower non empty programmed FinPartState of S,
f be Instruction-Location of S;
set k = card F -' 1,
P = F ';' G;
assume locnum f < card F - 1;
then locnum f < card CutLastLoc F by Th49;
then A1: il.(S,locnum f) in dom CutLastLoc F by AMISTD_1:50;
A2: f = il.(S,locnum f) by AMISTD_1:def 13;
A3: CutLastLoc F c= F by Lm8;
then A4: dom CutLastLoc F c= dom F by GRFUNC_1:8;
CutLastLoc F c= CutLastLoc P & CutLastLoc P c= P by Lm8,Th54;
then CutLastLoc F c= P by XBOOLE_1:1;
then A5: dom CutLastLoc F c= dom P by GRFUNC_1:8;
A6: F.il.(S,locnum f) = pi(F,il.(S,locnum f)) by A1,A4,AMI_5:def 5;
dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
then dom CutLastLoc F /\ dom Shift(IncAddr(G,k),k) = {} by XBOOLE_0:def 7;
then A7: not il.(S,locnum f) in dom Shift(IncAddr(G,k),k) by A1,XBOOLE_0:def 3;
A8: P.il.(S,locnum f)
= (CutLastLoc F +* Shift(IncAddr(G,k),k)).il.(S,locnum f) by Def22
.= (CutLastLoc F).il.(S,locnum f) by A7,FUNCT_4:12
.= F.il.(S,locnum f) by A1,A3,GRFUNC_1:8;
thus IncAddr(F,k).f = IncAddr(pi(F,il.(S,locnum f)),k) by A1,A2,A4,Def15
.= IncAddr(pi(P,il.(S,locnum f)),k) by A1,A5,A6,A8,AMI_5:def 5
.= IncAddr(P,k).f by A1,A2,A5,Def15;
end;
definition
let N be with_non-empty_elements set;
let S be regular standard realistic halting steady-programmed
without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
let F be lower non empty programmed FinPartState of S;
let G be halt-ending (lower non empty programmed FinPartState of S);
cluster F ';' G -> halt-ending;
coherence
proof
set P = F ';' G,
k = card F -' 1;
A1: P = CutLastLoc F +* Shift(IncAddr(G,k),k) by Def22;
A2: dom Shift(IncAddr(G,k),k) = { il.(S,m+k) where m is Nat:
il.(S,m) in dom IncAddr(G,k) } by Def16;
A3: il.(S, card G -' 1) = LastLoc G by AMISTD_1:55;
then A4: il.(S, card G -' 1) in dom G by AMISTD_1:51;
then A5: il.(S, card G -' 1) in dom IncAddr(G,k) by Def15;
then A6: il.(S, k + (card G -' 1)) in dom Shift(IncAddr(G,k),k) by A2;
A7: pi(G,il.(S,card G -' 1)) = G.il.(S,card G -' 1) by A4,AMI_5:def 5
.= halt S by A3,AMISTD_1:def 22;
card F <> 0 by CARD_2:59;
then A8: 1 <= card F by RLVECT_1:99;
card G <> 0 by CARD_2:59;
then card G >= 1 by RLVECT_1:99;
then A9: card G - 1 >= 0 by SQUARE_1:12;
then k + (card G - 1) >= k+0 by AXIOMS:24;
then A10: k + card G - 1 >= k+0 by XCMPLX_1:29;
k+0 >= 0 by NAT_1:18;
then A11: k + card G -' 1 = k + card G - 1 by A10,BINARITH:def 3
.= k + (card G - 1) by XCMPLX_1:29
.= k + (card G -' 1) by A9,BINARITH:def 3;
thus P.(LastLoc P) = P.il.(S,card P -' 1) by AMISTD_1:55
.= P.il.(S, card F + card G -' 1 -' 1) by Th52
.= P.il.(S, k + card G -' 1) by A8,JORDAN4:3
.= Shift(IncAddr(G,k),k).il.(S, k + (card G -' 1))
by A1,A6,A11,FUNCT_4:14
.= IncAddr(G,k).il.(S,card G -' 1) by A5,Def16
.= IncAddr(pi(G,il.(S,card G -' 1)),k) by A4,Def15
.= halt S by A7,Th30;
end;
end;
definition
let N be with_non-empty_elements set;
let S be regular standard realistic halting steady-programmed
without_implicit_jumps
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
let F, G be halt-ending unique-halt
(lower non empty programmed FinPartState of S);
cluster F ';' G -> unique-halt;
coherence
proof
set P = F ';' G,
k = card F -' 1;
A1: P = CutLastLoc F +* Shift(IncAddr(G,k),k) by Def22;
then A2: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by FUNCT_4:def 1
;
A3: dom Shift(IncAddr(G,k),k) = { il.(S,m+k) where m is Nat:
il.(S,m) in dom IncAddr(G,k) } by Def16;
card F <> 0 by CARD_2:59;
then A4: 1 <= card F by RLVECT_1:99;
card G <> 0 by CARD_2:59;
then card G >= 1 by RLVECT_1:99;
then A5: card G - 1 >= 0 by SQUARE_1:12;
then k + (card G - 1) >= k+0 by AXIOMS:24;
then A6: k + card G - 1 >= k+0 by XCMPLX_1:29;
k+0 >= 0 by NAT_1:18;
then A7: k + card G -' 1 = k + card G - 1 by A6,BINARITH:def 3
.= k + (card G - 1) by XCMPLX_1:29
.= k + (card G -' 1) by A5,BINARITH:def 3;
let f be Instruction-Location of S such that
A8: P.f = halt S and
A9: f in dom P;
per cases by A2,A9,XBOOLE_0:def 2;
suppose
A10: f in dom CutLastLoc F;
then A11: (CutLastLoc F).f <> halt S by Th51;
dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
then CutLastLoc F c= P by A1,FUNCT_4:33;
hence f = LastLoc P by A8,A10,A11,GRFUNC_1:8;
suppose
A12: f in dom Shift(IncAddr(G,k),k);
then consider m being Nat such that
A13: f = il.(S,m+k) and
A14: il.(S,m) in dom IncAddr(G,k) by A3;
A15: il.(S,m) in dom G by A14,Def15;
then A16: pi(G,il.(S,m)) = G.il.(S,m) by AMI_5:def 5;
IncAddr(pi(G,il.(S,m)),k)
= IncAddr(G,k).il.(S,m) by A15,Def15
.= Shift(IncAddr(G,k),k).il.(S,m+k) by A14,Def16
.= halt S by A1,A8,A12,A13,FUNCT_4:14;
then G.il.(S,m) = halt S by A16,Th35;
then il.(S,m) = LastLoc G by A15,AMISTD_1:def 23
.= il.(S,card G -' 1) by AMISTD_1:55;
then m = card G -' 1 by AMISTD_1:25;
then m+k = card F + card G -' 1 -' 1 by A4,A7,JORDAN4:3
.= card P -' 1 by Th52;
hence f = LastLoc P by A13,AMISTD_1:55;
end;
end;
definition
let N be with_non-empty_elements set;
let S be regular standard realistic halting steady-programmed
without_implicit_jumps (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
let F, G be pre-Macro of S;
redefine func F ';' G -> pre-Macro of S;
coherence;
end;
definition
let N be with_non-empty_elements set,
S be realistic halting steady-programmed IC-good Exec-preserving
(regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N))),
F, G be closed lower non empty programmed FinPartState of S;
cluster F ';' G -> closed;
coherence
proof
set P = F ';' G,
k = card F -' 1;
let f be Instruction-Location of S such that
A1: f in dom P;
A2: dom P = dom CutLastLoc F \/ dom Shift(IncAddr(G,k),k) by Lm9;
A3: P = CutLastLoc F +* Shift(IncAddr(G,k),k) by Def22;
dom CutLastLoc F misses dom Shift(IncAddr(G,k),k) by Th50;
then A4: dom CutLastLoc F /\ dom Shift(IncAddr(G,k),k) = {} by XBOOLE_0:def 7;
A5: CutLastLoc F c= F by Lm8;
then A6: dom CutLastLoc F c= dom F by GRFUNC_1:8;
A7: dom Shift(IncAddr(G,k),k) =
{il.(S,m+k) where m is Nat: il.(S,m) in dom IncAddr(G,k)} by Def16;
A8: NIC(pi(P,f),f) = { IC Following s where s is State of S:
IC s = f & s.f = pi(P,f) } by AMISTD_1:def 5;
let x be set;
assume x in NIC(pi(P,f),f);
then consider s2 being State of S such that
A9: x = IC Following s2 and
A10: IC s2 = f and
A11: s2.f = pi(P,f) by A8;
A12: pi(P,f) = P.f by A1,AMI_5:def 5;
A13: x = (Following s2).IC S by A9,AMI_1:def 15
.= Exec(CurInstr s2,s2).IC S by AMI_1:def 18
.= Exec(s2.IC s2,s2).IC S by AMI_1:def 17
.= IC Exec(pi(P,f),s2) by A10,A11,AMI_1:def 15;
per cases by A1,A2,XBOOLE_0:def 2;
suppose
A14: f in dom CutLastLoc F;
then A15: NIC(pi(F,f),f) c= dom F by A6,AMISTD_1:def 17;
A16: NIC(pi(F,f),f) = { IC Following s where s is State of S:
IC s = f & s.f = pi(F,f) } by AMISTD_1:def 5;
not f in dom Shift(IncAddr(G,k),k) by A4,A14,XBOOLE_0:def 3;
then s2.f = (CutLastLoc F).f by A3,A11,A12,FUNCT_4:12
.= F.f by A5,A14,GRFUNC_1:8
.= pi(F,f) by A6,A14,AMI_5:def 5;
then IC Following s2 in NIC(pi(F,f),f) by A10,A16;
then A17: x in dom F by A9,A15;
dom F c= dom P by Th53;
hence x in dom P by A17;
suppose
A18: f in dom Shift(IncAddr(G,k),k);
then consider m being Nat such that
A19: f = il.(S,m+k) and
A20: il.(S,m) in dom IncAddr(G,k) by A7;
A21: il.(S,m) in dom G by A20,Def15;
then A22: NIC(pi(G,il.(S,m)),il.(S,m)) c= dom G by AMISTD_1:def 17;
A23: ObjectKind IC S = the Instruction-Locations of S by AMI_1:def 11;
then reconsider v = IC S .--> il.(S,m) as FinPartState of S by AMI_1:59;
set s1 = s2 +* v;
A24: pi(P,f) = Shift(IncAddr(G,k),k).f by A3,A12,A18,FUNCT_4:14
.= IncAddr(G,k).il.(S,m) by A19,A20,Def16;
A25: (IC S .--> il.(S,m)).IC S = il.(S,m) by CQC_LANG:6;
A26: IC S in {IC S} by TARSKI:def 1;
A27: dom (IC S .--> il.(S,m)) = {IC S} by CQC_LANG:5;
A28: IC s1 = s1.IC S by AMI_1:def 15
.= il.(S,m) by A25,A26,A27,FUNCT_4:14;
A29: dom s2 = the carrier of S by AMI_3:36;
reconsider w = IC S .--> (IC s1 + k) as FinPartState of S by A23,AMI_1:59;
s1 +* w is State of S;
then A30: dom (s1 +* (IC S .--> (IC s1 + k))) = the carrier of S by AMI_3:36;
for a being set st a in dom s2 holds
s2.a = (s1 +* (IC S .--> (IC s1 + k))).a
proof
let a be set such that a in dom s2;
A31: dom (IC S .--> (IC s1 + k)) = {IC S} by CQC_LANG:5;
per cases;
suppose
A32: a = IC S;
hence s2.a = il.(S,m+k) by A10,A19,AMI_1:def 15
.= il.(S,locnum IC s1 + k) by A28,AMISTD_1:def 13
.= IC s1 + k by AMISTD_1:def 14
.= (IC S .--> (IC s1 + k)).a by A32,CQC_LANG:6
.= (s1 +* (IC S .--> (IC s1 + k))).a by A26,A31,A32,FUNCT_4:14;
suppose
A33: a <> IC S;
then A34: not a in dom (IC S .--> (IC s1 + k)) by A31,TARSKI:def 1;
not a in dom (IC S .--> il.(S,m)) by A27,A33,TARSKI:def 1;
then s1.a = s2.a by FUNCT_4:12;
hence s2.a = (s1 +* (IC S .--> (IC s1 + k))).a by A34,FUNCT_4:12;
end;
then A35: s2 = s1 +* (IC S .--> (IC s1 + k)) by A29,A30,FUNCT_1:9;
set s3 = s1 +* (il.(S,m) .--> pi(G,il.(S,m)));
A36: dom (il.(S,m) .--> pi(G,il.(S,m))) = {il.(S,m)} by CQC_LANG:5;
then A37: il.(S,m) in dom (il.(S,m) .--> pi(G,il.(S,m))) by TARSKI:def 1;
IC S <> il.(S,m) by AMI_1:48;
then A38: not IC S in dom (il.(S,m) .--> pi(G,il.(S,m))) by A36,TARSKI:def 1;
A39: IC s3 = s3.IC S by AMI_1:def 15
.= s1.IC S by A38,FUNCT_4:12
.= il.(S,m) by A25,A26,A27,FUNCT_4:14;
A40: s3.il.(S,m) = (il.(S,m) .--> pi(G,il.(S,m))).il.(S,m) by A37,FUNCT_4:14
.= pi(G,il.(S,m)) by CQC_LANG:6;
s1, s3 equal_outside the Instruction-Locations of S
proof
A41: dom s1 = the carrier of S & dom s3 = the carrier of S by AMI_3:36;
then A42: dom s1 \ the Instruction-Locations of S c= dom s3 by XBOOLE_1:36;
for x being set st x in dom s1 \ the Instruction-Locations of S holds
s1.x = s3.x
proof
let x be set;
assume A43: x in dom s1 \ the Instruction-Locations of S;
now
assume x in dom (il.(S,m) .--> pi(G,il.(S,m)));
then x = il.(S,m) by A36,TARSKI:def 1;
hence contradiction by A43,XBOOLE_0:def 4;
end;
hence s1.x = s3.x by FUNCT_4:12;
end;
hence s1|(dom s1 \ the Instruction-Locations of S) =
s3|(dom s3 \ the Instruction-Locations of S) by A41,A42,SCMFSA6A:9;
end;
then A44: Exec(pi(G,il.(S,m)),s1), Exec(pi(G,il.(S,m)),s3)
equal_outside the Instruction-Locations of S by Def19;
reconsider k,m as Element of NAT;
A45: x = IC Exec(IncAddr(pi(G,il.(S,m)),k),s2) by A13,A21,A24,Def15
.= IC Exec(pi(G,il.(S,m)), s1) + k by A35,Def17
.= IC Exec(pi(G,il.(S,m)), s3) + k by A44,SCMFSA6A:29
.= il.(S,locnum IC Exec(pi(G,il.(S,m)), s3) + k) by AMISTD_1:def 14;
A46: NIC(pi(G,il.(S,m)),il.(S,m)) =
{ IC Following t where t is State of S:
IC t = il.(S,m) & t.il.(S,m) = pi(G,il.(S,m)) } by AMISTD_1:def 5;
IC Following s3 = IC Exec(CurInstr s3,s3) by AMI_1:def 18
.= IC Exec(s3.IC s3,s3) by AMI_1:def 17
.= il.(S,locnum IC Exec(pi(G,il.(S,m)), s3))
by A39,A40,AMISTD_1:def 13;
then il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in NIC(pi(G,il.(S,m)),il.(S
,m))
by A39,A40,A46;
then il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in dom G by A22;
then
A47: il.(S,locnum IC Exec(pi(G,il.(S,m)), s3)) in dom IncAddr(G,k)
by Def15;
reconsider nn = locnum IC Exec(pi(G,il.(S,m)), s3) as Element of NAT;
A48: x = il.(S,nn + k) by A45;
x in dom Shift(IncAddr(G,k),k) by A7,A47,A48;
hence x in dom P by A2,XBOOLE_0:def 2;
end;
end;
theorem Th57:
for S being regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N))
holds IncAddr(Stop S, k) = Stop S
proof
let S be regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
A1: dom IncAddr(Stop S, k) = dom Stop S by Def15
.= {il.(S,0)} by Lm5;
A2: dom Stop S = {il.(S,0)} by Lm5;
A3: Stop S = il.(S,0) .--> halt S by Def13;
for x being set st x in {il.(S,0)} holds IncAddr(Stop S, k).x = (Stop S).
x
proof
let x be set;
assume
A4: x in {il.(S,0)};
then A5: x = il.(S,0) by TARSKI:def 1;
then A6: pi(Stop S,il.(S,0)) = (Stop S).il.(S,0) by A2,A4,AMI_5:def 5
.= halt S by A3,CQC_LANG:6;
thus IncAddr(Stop S, k).x
= IncAddr(pi(Stop S,il.(S,0)),k) by A2,A4,A5,Def15
.= halt S by A6,Th30
.= (Stop S).x by A3,A5,CQC_LANG:6;
end;
hence IncAddr(Stop S, k) = Stop S by A1,A2,FUNCT_1:9;
end;
theorem Th58:
for S being standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N))
holds Shift(Stop S, k) = il.(S,k) .--> halt S
proof
let S be standard halting (IC-Ins-separated definite
(non empty non void AMI-Struct over N));
A1: dom Shift(Stop S,k) = {il.(S,m+k) where m is Nat: il.(S,m) in dom Stop S}
by Def16;
A2: il.(S,0) in dom Stop S by Lm5;
A3: dom Shift(Stop S,k) = {il.(S,k)}
proof
hereby
let x be set;
assume x in dom Shift(Stop S,k);
then consider m being Nat such that
A4: x = il.(S,m+k) and
A5: il.(S,m) in dom Stop S by A1;
il.(S,m) in {il.(S,0)} by A5,Lm5;
then il.(S,m) = il.(S,0) by TARSKI:def 1;
then m = 0 by AMISTD_1:25;
hence x in {il.(S,k)} by A4,TARSKI:def 1;
end;
let x be set;
assume x in {il.(S,k)};
then x = il.(S,0+k) by TARSKI:def 1;
hence thesis by A1,A2;
end;
A6: dom (il.(S,k) .--> halt S) = {il.(S,k)} by CQC_LANG:5;
for x being set st x in {il.(S,k)} holds
(Shift(Stop S, k)).x = (il.(S,k) .--> halt S).x
proof
let x be set;
assume x in {il.(S,k)};
then A7: x = il.(S,0+k) by TARSKI:def 1;
il.(S,0) in dom Stop S by Lm5;
hence (Shift(Stop S, k)).x = (Stop S).il.(S,0) by A7,Def16
.= halt S by Lm6
.= (il.(S,k) .--> halt S).x by A7,CQC_LANG:6;
end;
hence thesis by A3,A6,FUNCT_1:9;
end;
theorem Th59:
for S being regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F being pre-Macro of S
holds F ';' Stop S = F
proof
let S be regular standard halting without_implicit_jumps
realistic (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
F be pre-Macro of S;
set k = card F -' 1;
A1: F ';' Stop S = CutLastLoc F +* Shift(IncAddr(Stop S,k),k) by Def22;
then A2: F ';' Stop S = CutLastLoc F +* Shift(Stop S,k) by Th57;
A3: dom F = dom CutLastLoc F \/ {LastLoc F} by Th48;
dom Shift(Stop S,k) = dom (il.(S,k) .--> halt S) by Th58
.= {il.(S,k)} by CQC_LANG:5
.= {LastLoc F} by AMISTD_1:55;
then A4: dom (F ';' Stop S) = dom F by A2,A3,FUNCT_4:def 1;
for x being set st x in dom F holds (F ';' Stop S).x = F.x
proof
let x be set such that
A5: x in dom F;
dom CutLastLoc F misses dom Shift(IncAddr(Stop S,k),k) by Th50;
then A6: {} = dom CutLastLoc F /\ dom Shift(IncAddr(Stop S,k),k) by XBOOLE_0:
def 7
;
A7: CutLastLoc F c= F by Lm8;
per cases by A3,A5,XBOOLE_0:def 2;
suppose
A8: x in dom CutLastLoc F;
then not x in dom Shift(IncAddr(Stop S,k),k) by A6,XBOOLE_0:def 3;
hence (F ';' Stop S).x = (CutLastLoc F).x by A1,FUNCT_4:12
.= F.x by A7,A8,GRFUNC_1:8;
suppose x in {LastLoc F};
then A9: x = LastLoc F by TARSKI:def 1;
then A10: x = il.(S,k) by AMISTD_1:55;
A11: il.(S,0) in dom Stop S by Lm5;
dom Shift(Stop S,k)
= { il.(S,m+k) where m is Nat: il.(S,m) in dom Stop S } by Def16;
then il.(S,0+k) in dom Shift(Stop S,k) by A11;
hence (F ';' Stop S).x = Shift(Stop S,0+k).x by A2,A10,FUNCT_4:14
.= (Stop S).il.(S,0) by A10,A11,Def16
.= halt S by Lm6
.= F.x by A9,AMISTD_1:def 22;
end;
hence F ';' Stop S = F by A4,FUNCT_1:9;
end;
theorem Th60:
for S being regular standard halting
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
F being pre-Macro of S
holds Stop S ';' F = F
proof
let S be regular standard halting
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
F be pre-Macro of S;
set k = card Stop S -' 1;
A1: k = 0 by Lm7;
thus Stop S ';' F = CutLastLoc Stop S +* Shift(IncAddr(F,k),k) by Def22
.= CutLastLoc Stop S +* Shift(F,k) by A1,Th38
.= CutLastLoc Stop S +* F by A1,Th40
.= F by FUNCT_4:21;
end;
theorem
for S being regular standard realistic halting steady-programmed
without_implicit_jumps (IC-Ins-separated
definite (non empty non void AMI-Struct over N)),
F, G, H being pre-Macro of S
holds F ';' G ';' H = F ';' (G ';' H)
proof
let S be regular standard realistic halting steady-programmed
without_implicit_jumps (IC-Ins-separated
definite (non empty non void AMI-Struct over N)),
F, G, H be pre-Macro of S;
per cases;
suppose
A1: F = Stop S;
hence F ';' G ';' H = G ';' H by Th60
.= F ';' (G ';' H) by A1,Th60;
suppose
A2: G = Stop S;
hence F ';' G ';' H = F ';' H by Th59
.= F ';' (G ';' H) by A2,Th60;
suppose that
A3: F <> Stop S and
A4: G <> Stop S;
set X = {il.(S,k) where k is Nat: k < card F + card G + card H - 1 - 1};
A5: card (F ';' G ';' H) = card (F ';' G) + card H - 1 by Th52
.= card F + card G - 1 + card H - 1 by Th52
.= card F + card G + card H - 1 - 1 by XCMPLX_1:29;
A6: card (F ';' (G ';' H)) = card F + card (G ';' H) - 1 by Th52
.= card F + (card G + card H - 1) - 1 by Th52
.= card F + (card G + card H) - 1 - 1 by XCMPLX_1:29
.= card F + card G + card H - 1 - 1 by XCMPLX_1:1;
A7: dom (F ';' G ';' H) = X by A5,Th15;
A8: dom (F ';' (G ';' H)) = X by A6,Th15;
for x being set st x in X holds (F ';' G ';' H).x = (F ';' (G ';' H)).x
proof
let x be set;
assume x in X;
then consider k being Nat such that
A9: x = il.(S,k) and
A10: k < card F + card G + card H - 1 - 1;
A11: F ';' G ';' H =
CutLastLoc (F ';' G) +*
Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1) by Def22;
A12: F ';' (G ';' H) =
CutLastLoc F +*
Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by Def22;
A13: dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) =
{ il.(S,m+(card F -' 1)) where m is Nat:
il.(S,m) in dom IncAddr(G ';' H,card F -' 1) } by Def16;
A14: dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1) =
{ il.(S,m+(card (F ';' G) -' 1)) where m is Nat:
il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) } by Def16;
A15: dom Shift(IncAddr(H,card G -' 1),card G -' 1) =
{ il.(S,m+(card G -' 1)) where m is Nat:
il.(S,m) in dom IncAddr(H,card G -' 1) } by Def16;
A16: card (F ';' G) -' 1
= card (F ';' G) - 1 by Th4
.= card F + card G - 1 - 1 by Th52;
then A17: card (F ';' G) -' 1
= card F - 1 + card G - 1 by XCMPLX_1:29
.= card F - 1 + (card G - 1) by XCMPLX_1:29;
then A18: card (F ';' G) -' 1
= (card G -' 1) + (card F - 1) by Th4
.= (card G -' 1) + (card F -' 1) by Th4;
A19: dom Shift(IncAddr(G,card F -' 1),card F -' 1) =
{ il.(S,m+(card F -' 1)) where m is Nat:
il.(S,m) in dom IncAddr(G,card F -' 1) } by Def16;
A20: CutLastLoc G c= G by Lm8;
A21: card F -' 1 = card F - 1 by Th4;
A22: card G -' 1 = card G - 1 by Th4;
A23: for W being pre-Macro of S st W <> Stop S holds 2 <= card W
proof
let W be pre-Macro of S;
assume W <> Stop S;
then A24: card W <> 1 by Th26;
A25: card W <> 0 by CARD_2:59;
assume 2 > card W;
then 1 + 1 > card W;
then card W <= 1 by NAT_1:38;
hence contradiction by A24,A25,CQC_THE1:2;
end;
then 2 <= card F by A3;
then A26: 1 <= card F by AXIOMS:22;
A27: 2 <= card G by A4,A23;
per cases by A26,A27,Lm4;
suppose
A28: k < card F - 1;
A29: CutLastLoc F c= CutLastLoc (F ';' G) by Th54;
A30: now
assume x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1);
then consider m being Nat such that
A31: x = il.(S,m+(card F -' 1)) and
il.(S,m) in dom IncAddr(G ';' H,card F -' 1) by A13;
k = m + (card F -' 1) by A9,A31,AMISTD_1:25
.= m + (card F - 1) by Th4;
then m + (card F - 1) < card F -' 1 by A28,Th4;
then m + (card F -' 1) < card F -' 1 by Th4;
hence contradiction by NAT_1:29;
end;
A32: now
assume x in dom
Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1);
then consider m being Nat such that
A33: x = il.(S,m+(card (F ';' G) -' 1)) and
il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) by A14;
k = m + (card (F ';' G) -' 1) by A9,A33,AMISTD_1:25
.= m + (card G -' 1) + (card F -' 1) by A18,XCMPLX_1:1;
then m + (card G -' 1) + (card F -' 1) < card F -' 1 by A28,Th4;
hence contradiction by NAT_1:29;
end;
k < card CutLastLoc F by A28,Th49;
then A34: x in dom CutLastLoc F by A9,AMISTD_1:50;
thus (F ';' G ';' H).x
= (CutLastLoc (F ';' G)).x by A11,A32,FUNCT_4:12
.= (CutLastLoc F).x by A29,A34,GRFUNC_1:8
.= (F ';' (G ';' H)).x by A12,A30,FUNCT_4:12;
suppose
A35: k = card F - 1;
A36: now
assume x in dom
Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1);
then consider m being Nat such that
A37: x = il.(S,m+(card (F ';' G) -' 1)) and
il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) by A14;
k = m + (card (F ';' G) -' 1) by A9,A37,AMISTD_1:25
.= m + (card G -' 1) + (card F -' 1) by A18,XCMPLX_1:1;
then m + (card G -' 1) + (card F -' 1) = card F -' 1 by A35,Th4;
then m + (card G -' 1) = (card F -' 1) - (card F -' 1) by XCMPLX_1:26;
then m + (card G -' 1) = 0 by XCMPLX_1:14;
then card G -' 1 = 0 by NAT_1:23;
then card G - 1 = 0 by Th4;
then card G = 1 by XCMPLX_1:15;
hence contradiction by A4,Th26;
end;
A38: il.(S,0) in dom IncAddr(G ';' H,card F -' 1) by AMISTD_1:49;
A39: il.(S,0) in dom IncAddr(G,card F -' 1) by AMISTD_1:49;
A40: il.(S,0) in dom G by AMISTD_1:49;
A41: il.(S,0) in dom (G ';' H) by AMISTD_1:49;
k = 0 + (card F -' 1) by A35,Th4;
then A42: x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A9,A13,
A38;
A43: k = card F -' 1 by A35,Th4;
A44: x = il.(S,0+k) by A9;
il.(S,0) in dom IncAddr(G,card F -' 1) by AMISTD_1:49;
then A45: x in dom Shift(IncAddr(G,card F -' 1),card F -' 1) by A19,A43,A44;
then x in dom CutLastLoc F \/ dom Shift(IncAddr(G,card F -' 1),card F -'
1)
by XBOOLE_0:def 2;
then A46: x in dom (F ';' G) by Lm9;
now
A47: dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
= {LastLoc (F ';' G)} by CQC_LANG:5
.= {il.(S,card (F ';' G) -' 1)} by AMISTD_1:55;
assume x in dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ));
then x = il.(S,card (F ';' G) -' 1) by A47,TARSKI:def 1;
then k = (card G -' 1) + (card F -' 1) by A9,A18,AMISTD_1:25;
then card G -' 1 = (card F -' 1) - (card F -' 1) by A43,XCMPLX_1:26
.= 0 by XCMPLX_1:14;
then card G - 1 = 0 by Th4;
then card G = 1 by XCMPLX_1:15;
hence contradiction by A4,Th26;
end;
then A48: x in dom (F ';' G) \
dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
by A46,XBOOLE_0:def 4;
card G > 1
proof
card G <> 0 by CARD_2:59;
hence 1 <= card G & 1 <> card G by A4,Th26,RLVECT_1:99;
end;
then A49: card G - 1 > 1 - 1 by REAL_1:54;
then card G -' 1 > 1 - 1 by Th4;
then A50: not il.(S,0) in dom Shift(IncAddr(H,card G -' 1), card G -' 1) by
Th41;
card CutLastLoc G <> {} by A49,Th49,CARD_1:51;
then A51: il.(S,0) in dom CutLastLoc G by AMISTD_1:49,CARD_1:78;
A52: pi(G,il.(S,0)) = G.il.(S,0) by A40,AMI_5:def 5
.= (CutLastLoc G).il.(S,0) by A20,A51,GRFUNC_1:8
.= ((CutLastLoc G) +* Shift(IncAddr(H,card G -' 1), card G -' 1)).
il.(S,0) by A50,FUNCT_4:12
.= (G ';' H).il.(S,0) by Def22
.= pi(G ';' H,il.(S,0)) by A41,AMI_5:def 5;
thus (F ';' G ';' H).x
= (CutLastLoc (F ';' G)).x by A11,A36,FUNCT_4:12
.= ((F ';' G) \
( LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))).x by Def21
.= (F ';' G).x by A48,Th3
.= (CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1)).x
by Def22
.= Shift(IncAddr(G,card F -' 1),card F -' 1).x by A45,FUNCT_4:14
.= IncAddr(G,card F -' 1).il.(S,0) by A39,A43,A44,Def16
.= IncAddr(pi(G ';' H,il.(S,0)),card F -' 1) by A40,A52,Def15
.= IncAddr(G ';' H,card F -' 1).il.(S,0) by A41,Def15
.= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x
by A38,A43,A44,Def16
.= (F ';' (G ';' H)).x by A12,A42,FUNCT_4:14;
suppose that
A53: card F <= k and
A54: k <= card F + card G - 3;
A55: now
assume
x in dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1);
then consider m being Nat such that
A56: x = il.(S,m+(card (F ';' G) -' 1)) and
il.(S,m) in dom IncAddr(H,card (F ';' G) -' 1) by A14;
m + ((card G -' 1) + (card F -' 1)) <= card F + card G - (1+2)
by A9,A18,A54,A56,AMISTD_1:25;
then m + ((card G -' 1) + (card F -' 1)) <= card F + card G - 1 - 2
by XCMPLX_1:36;
then m + ((card G -' 1) + (card F -' 1)) <= card F - 1 + card G - (1+1
)
by XCMPLX_1:29;
then m + ((card G -' 1) + (card F -' 1)) <= card F - 1 + card G - 1 -
1
by XCMPLX_1:36;
then m + ((card G -' 1) + (card F -' 1))
<= (card G -' 1) + (card F -' 1) - 1 by A21,A22,XCMPLX_1:29;
then m + ((card G -' 1) + (card F -' 1))
<= - 1 + ((card G -' 1) + (card F -' 1)) by XCMPLX_0:def 8;
then m <= -1 by REAL_1:53;
hence contradiction by Lm3;
end;
card F -' 1 <= card F by GOBOARD9:2;
then k >= card F -' 1 by A53,AXIOMS:22;
then A57: x = il.(S, k -' (card F -' 1) + (card F -' 1)) by A9,AMI_5:4;
card F - card F <= k - card F by A53,REAL_1:49;
then A58: 0 <= k - card F by XCMPLX_1:14;
card F - 1 < card F - 0 by REAL_1:92;
then k - (card F - 1) >= 0 by A58,REAL_1:92;
then A59: k - (card F -' 1) >= 0 by Th4;
card F + card G - 3 < card F + card G - 3 + 1 by REAL_1:69;
then A60: card F + card G - 3 < card F + card G - (3 - 1) by XCMPLX_1:37;
then A61: k < card F + card G - 2 by A54,AXIOMS:22;
then A62: k < (card G - 1) + (card F - 1) by Lm2;
k - 0 < (card G - 1) + (card F - 1) by A61,Lm2;
then k - ((card F - 1) - (card F - 1)) < (card G - 1) + (card F - 1)
by XCMPLX_1:14;
then k - (card F - 1) + (card F - 1) < (card G - 1) + (card F - 1)
by XCMPLX_1:37;
then k - (card F - 1) < card G - 1 by REAL_1:55;
then k - (card F -' 1) < card G - 1 by Th4;
then k -' (card F -' 1) < card G - 1 by A59,BINARITH:def 3;
then k -' (card F -' 1) < card CutLastLoc G by Th49;
then A63: il.(S,k -' (card F -' 1)) in dom CutLastLoc G by AMISTD_1:50;
then il.(S,k -' (card F -' 1)) in
dom CutLastLoc G \/ dom Shift(IncAddr(H,card G -' 1),card G -' 1)
by XBOOLE_0:def 2;
then A64: il.(S,k -' (card F -' 1)) in dom (G ';' H) by Lm9;
then A65: il.(S,k -' (card F -' 1)) in dom IncAddr(G ';' H,card F -' 1)
by Def15;
then A66: x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A13,A57
;
card G + card F - 2 < card F + card G - 1 by REAL_1:92;
then (card G - 1) + (card F - 1) < card F + card G - 1 by Lm2;
then k < card F + card G - 1 by A62,AXIOMS:22;
then k < card (F ';' G) by Th52;
then A67: x in dom (F ';' G) by A9,AMISTD_1:50;
now
assume x in dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G));
then x in {LastLoc (F ';' G)} by CQC_LANG:5;
then x = LastLoc (F ';' G) by TARSKI:def 1
.= il.(S,card (F ';' G) -' 1) by AMISTD_1:55;
then k = card (F ';' G) -' 1 by A9,AMISTD_1:25
.= (card G - 1) + (card F - 1) by A18,A22,Th4;
hence contradiction by A54,A60,Lm2;
end;
then A68: x in dom (F ';' G) \
dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G))
by A67,XBOOLE_0:def 4;
A69: dom CutLastLoc G c= dom G by A20,GRFUNC_1:8;
then il.(S,k -' (card F -' 1)) in dom G by A63;
then A70: il.(S,k -' (card F -' 1)) in dom IncAddr(G,card F -' 1) by Def15;
then A71: x in dom Shift(IncAddr(G,card F -' 1),card F -' 1) by A19,A57;
A72: now
assume il.(S,k -' (card F -' 1)) in
dom Shift(IncAddr(H,card G -' 1),card G -' 1);
then consider m being Nat such that
A73: il.(S,k -' (card F -' 1)) = il.(S,m+(card G -' 1)) and
il.(S,m) in dom IncAddr(H,card G -' 1) by A15;
k -' (card F -' 1) = m + (card G -' 1) by A73,AMISTD_1:25;
then A74: m = k -' (card F -' 1) - (card G -' 1) by XCMPLX_1:26
.= k - (card F -' 1) - (card G -' 1) by A59,BINARITH:def 3
.= k - (card F - 1) - (card G -' 1) by Th4
.= k - (card F - 1) - (card G - 1) by Th4
.= k - ((card F - 1) + (card G - 1)) by XCMPLX_1:36
.= k - (card F + card G - 2) by Lm2;
k - (card F + card G - 2)
<= card F + card G - 3 - (card F + card G - 2) by A54,REAL_1:49;
then k - (card F + card G - 2)
<= card F + card G - (card F + card G - 2 + 3) by XCMPLX_1:36;
then k - (card F + card G - 2)
<= card F + card G - (card F + card G - (2 - 3)) by XCMPLX_1:37;
then k - (card F + card G - 2)
<= card F + card G - (card F + card G) + (2 - 3) by XCMPLX_1:37;
then k - (card F + card G - 2) <= 0 + (2 - 3) by XCMPLX_1:14;
hence contradiction by A74,Lm3;
end;
A75: pi(G ';' H,il.(S,k -' (card F -' 1)))
= (G ';' H).il.(S,k -' (card F -' 1)) by A64,AMI_5:def 5
.= (CutLastLoc G +* Shift(IncAddr(H,card G -' 1),card G -' 1))
.il.(S,k -' (card F -' 1)) by Def22
.= (CutLastLoc G).il.(S,k -' (card F -' 1)) by A72,FUNCT_4:12
.= G.il.(S,k -' (card F -' 1)) by A20,A63,GRFUNC_1:8;
thus (F ';' G ';' H).x
= (CutLastLoc (F ';' G)).x by A11,A55,FUNCT_4:12
.= ((F ';' G) \ (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G))).x
by Def21
.= (F ';' G).x by A68,Th3
.= (CutLastLoc F +* Shift(IncAddr(G,card F -' 1),card F -' 1)).x
by Def22
.= Shift(IncAddr(G,card F -' 1),card F -' 1).x by A71,FUNCT_4:14
.= IncAddr(G,card F -' 1).il.(S,k -' (card F -' 1)) by A57,A70,Def16
.= IncAddr(pi(G,il.(S,k -' (card F -' 1))),card F -' 1)
by A63,A69,Def15
.= IncAddr(pi(G ';' H,il.(S,k -' (card F -' 1))),card F -' 1)
by A63,A69,A75,AMI_5:def 5
.= IncAddr(G ';' H,card F -' 1).il.(S,k -' (card F -' 1))
by A64,Def15
.= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x by A57,A65,Def16
.= (F ';' (G ';' H)).x by A12,A66,FUNCT_4:14;
suppose
A76: k = card F + card G - 2;
then A77: card (F ';' G) -' 1 = k by A17,Lm2;
then A78: x = il.(S,k -' (card (F ';' G) -' 1) + (card (F ';' G) -' 1))
by A9,AMI_5:4;
k - (card (F ';' G) -' 1) = 0 by A77,XCMPLX_1:14;
then A79: k -' (card (F ';' G) -' 1) = 0 by BINARITH:def 3;
then A80: il.(S,k -' (card (F ';' G) -' 1)) in dom IncAddr(H,card (F ';' G)
-' 1)
by AMISTD_1:49;
then A81: x in dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1)
by A14,A78;
A82: x = il.(S, (card G -' 1) + (card F -' 1)) by A9,A21,A22,A76,Lm2;
0 <> card H by CARD_2:59;
then 0 < card H by NAT_1:19;
then card G - 1 + 0 < card G - 1 + card H by REAL_1:53;
then card G -' 1 < card G + card H - 1 by A22,XCMPLX_1:29;
then card G -' 1 < card (G ';' H) by Th52;
then A83: il.(S,card G -' 1) in dom (G ';' H) by AMISTD_1:50;
then A84: il.(S,card G -' 1) in dom IncAddr(G ';' H,card F -' 1) by Def15;
then A85: x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A13,A82
;
A86: il.(S,0) in dom H by AMISTD_1:49;
A87: pi(G ';' H,il.(S,card G -' 1)) = (G ';' H).il.(S,card G -' 1)
by A83,AMI_5:def 5;
A88: il.(S,0) in dom IncAddr(H,card G -' 1) by AMISTD_1:49;
then A89: pi(IncAddr(H,card G -' 1),il.(S,0))
= IncAddr(H,card G -' 1).il.(S,0) by AMI_5:def 5
.= IncAddr(pi(H,il.(S,0)),(card G -' 1)) by A86,Def15;
pi(G ';' H,il.(S,card G -' 1))
= (G ';' H).LastLoc G by A87,AMISTD_1:55
.= IncAddr(H,card G -' 1).il.(S,0) by Th55
.= pi(IncAddr(H,card G -' 1),il.(S,0)) by A88,AMI_5:def 5;
then A90: IncAddr(pi(G ';' H,il.(S,card G -' 1)),card F -' 1)
= IncAddr(pi(H,il.(S,0)),card (F ';' G) -' 1) by A18,A89,Th37;
thus (F ';' G ';' H).x
= Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1).x
by A11,A81,FUNCT_4:14
.= IncAddr(H,card (F ';' G) -' 1).il.(S,k -' (card (F ';' G) -' 1))
by A78,A80,Def16
.= IncAddr(pi(H,il.(S,0)),card (F ';' G) -' 1) by A79,A86,Def15
.= IncAddr(G ';' H,card F -' 1).il.(S,card G -' 1) by A83,A90,Def15
.= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x by A82,A84,Def16
.= (F ';' (G ';' H)).x by A12,A85,FUNCT_4:14;
suppose card F + card G - 2 < k;
then card F + card G - (1 + 1) < k;
then A91: k >= card (F ';' G) -' 1 by A16,XCMPLX_1:36;
then A92: x = il.(S,k -' (card (F ';' G) -' 1) + (card (F ';' G) -' 1))
by A9,AMI_5:4;
A93: k - (card (F ';' G) -' 1) >= 0 by A91,SQUARE_1:12;
k < card F + card G + card H - (1 + 1) by A10,XCMPLX_1:36;
then k + 0 < card F + card G - (1 + 1) + card H by XCMPLX_1:29;
then k - (card F + card G - (1 + 1)) < card H - 0 by REAL_2:168;
then k - (card (F ';' G) -' 1) < card H by A16,XCMPLX_1:36;
then k -' (card (F ';' G) -' 1) < card H by A93,BINARITH:def 3;
then A94: il.(S,k -' (card (F ';' G) -' 1)) in dom H by AMISTD_1:50;
then A95: il.(S,k -' (card (F ';' G) -' 1)) in dom IncAddr(H,card (F ';' G)
-' 1)
by Def15;
then A96: x in dom Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1)
by A14,A92;
card F -' 1 <= (card G -' 1) + (card F -' 1) by NAT_1:29;
then A97: k >= card F -' 1 by A18,A91,AXIOMS:22;
then A98: x = il.(S,k -' (card F -' 1) + (card F -' 1)) by A9,AMI_5:4;
A99: k - (card F -' 1) >= 0 by A97,SQUARE_1:12;
k - (card F -' 1) < card F + card G + card H - 1 - 1 - (card F -' 1)
by A10,REAL_1:54;
then k -' (card F -' 1) < card F + card G + card H - 1 - 1 - (card F - 1
)
by A21,A99,BINARITH:def 3;
then k -' (card F -' 1) < card F + card G + card H - 1 - (1 + (card F -
1))
by XCMPLX_1:36;
then k -' (card F -' 1) < card F + card G + card H - 1 - (card F - (1 -
1))
by XCMPLX_1:37;
then k -' (card F -' 1) < card F + card G + card H - card F - 1
by XCMPLX_1:21;
then k -' (card F -' 1) < card F + card G - card F + card H - 1
by XCMPLX_1:29;
then k -' (card F -' 1) < card F - card F + card G + card H - 1
by XCMPLX_1:29;
then A100: k -' (card F -' 1) < 0 + card G + card H - 1 by XCMPLX_1:14;
then k -' (card F -' 1) < card (G ';' H) by Th52;
then A101: il.(S,k -' (card F -' 1)) in dom (G ';' H) by AMISTD_1:50;
then il.(S,k -' (card F -' 1)) in dom IncAddr(G ';' H,card F -' 1)
by Def15;
then A102: x in dom Shift(IncAddr(G ';' H,card F -' 1),card F -' 1) by A13,
A98;
A103: il.(S,k -' (card F -' 1)) in dom IncAddr(G ';' H,card F -' 1)
by A101,Def15;
k - (card F -' 1) >= card (F ';' G) -' 1 - (card F -' 1)
by A91,REAL_1:49;
then k -' (card F -' 1) >= (card F -' 1) + (card G -' 1) - (card F -' 1)
by A18,A97,SCMFSA_7:3;
then A104: k -' (card F -' 1) >= card G -' 1 by XCMPLX_1:26;
then A105: il.(S,k -' (card F -' 1)) =
il.(S, k -' (card F -' 1) -' (card G -' 1) + (card G -' 1))
by AMI_5:4;
k -' (card F -' 1) - (card G -' 1) < card G + card H - 1 - (card G - 1)
by A22,A100,REAL_1:54;
then k -' (card F -' 1) - (card G -' 1) <
card H + (card G - 1) - (card G - 1) by XCMPLX_1:29;
then k -' (card F -' 1) -' (card G -' 1) <
card H + (card G - 1) - (card G - 1) by A104,SCMFSA_7:3;
then k -' (card F -' 1) -' (card G -' 1) < card H by XCMPLX_1:26;
then il.(S,k -' (card F -' 1) -' (card G -' 1)) in dom H by AMISTD_1:50;
then A106: il.(S,k -' (card F -' 1) -' (card G -' 1)) in
dom IncAddr(H,card G -' 1) by Def15;
then A107: il.(S,k -' (card F -' 1)) in
dom Shift(IncAddr(H,card G -' 1),card G -' 1) by A15,A105;
A108: k -' (card F -' 1) -' (card G -' 1)
= k -' (card F -' 1) - (card G -' 1) by A104,SCMFSA_7:3
.= k - (card F -' 1) - (card G -' 1) by A97,SCMFSA_7:3
.= k - ((card F -' 1) + (card G -' 1)) by XCMPLX_1:36
.= k -' (card (F ';' G) -' 1) by A18,A91,SCMFSA_7:3;
A109: pi(G ';' H,il.(S,k -' (card F -' 1)))
= (G ';' H).il.(S,k -' (card F -' 1)) by A101,AMI_5:def 5
.= ((CutLastLoc G) +* Shift(IncAddr(H,card G -' 1),card G -' 1)).
il.(S,k -' (card F -' 1)) by Def22
.= Shift(IncAddr(H,card G -' 1),card G -' 1).il.(S,k -' (card F -' 1))
by A107,FUNCT_4:14
.= IncAddr(H,card G -' 1).il.(S,k -' (card (F ';' G) -' 1)) by A105,A106
,A108,Def16
.= IncAddr(pi(H,il.(S,k -' (card (F ';' G) -' 1))),card G -' 1)
by A94,Def15;
thus (F ';' G ';' H).x
= Shift(IncAddr(H,card (F ';' G) -' 1),card (F ';' G) -' 1).x
by A11,A96,FUNCT_4:14
.= IncAddr(H,card (F ';' G) -' 1).il.(S,k -' (card (F ';' G) -' 1))
by A92,A95,Def16
.= IncAddr(pi(H,il.(S,k -' (card (F ';' G) -' 1))),card (F ';' G) -' 1)
by A94,Def15
.= IncAddr(pi(G ';' H,il.(S,k -' (card F -' 1))),card F -' 1)
by A18,A109,Th37
.= IncAddr(G ';' H,card F -' 1).il.(S,k -' (card F -' 1))
by A101,Def15
.= Shift(IncAddr(G ';' H,card F -' 1),card F -' 1).x by A98,A103,Def16
.= (F ';' (G ';' H)).x by A12,A102,FUNCT_4:14;
end;
hence thesis by A7,A8,FUNCT_1:9;
end;