Copyright (c) 2003 Association of Mizar Users
environ
vocabulary AMISTD_3, AMI_1, TREES_2, GOBOARD5, AMI_3, RELAT_1, FINSET_1,
FUNCT_1, AMISTD_1, SQUARE_1, WAYBEL_0, BOOLE, ORDINAL1, FINSEQ_1, CARD_1,
CARD_3, ORDINAL2, ARYTM, PARTFUN1, TREES_1, TARSKI, WELLORD1, WELLORD2,
AMISTD_2, FRECHET, FINSEQ_2, CAT_1, FUNCOP_1, MEMBERED;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1, NUMBERS,
ORDINAL1, ORDINAL2, MEMBERED, XREAL_0, CQC_SIM1, NAT_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, WELLORD1, WELLORD2, FUNCOP_1, CQC_LANG, FINSEQ_1,
FINSEQ_2, TREES_1, TREES_2, STRUCT_0, AMI_1, AMI_3, AMI_5, AMISTD_1,
AMISTD_2;
constructors AMISTD_2, CQC_SIM1, WELLORD1, ORDERS_2, AMI_5, PRE_CIRC,
POLYNOM1, WELLORD2;
clusters AMI_1, AMISTD_1, FINSET_1, RELSET_1, TREES_2, ARYTM_3, FINSEQ_6,
FUNCT_7, HEYTING2, NECKLACE, CARD_5, WAYBEL12, RELAT_1, FUNCOP_1,
FINSEQ_5, SCMFSA_4, XREAL_0, CARD_1, ORDINAL1, MEMBERED, FINSEQ_1,
PRELAMB;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, ORDINAL1, WELLORD1, WELLORD2, FUNCT_1, TREES_1;
theorems ORDINAL2, AMI_3, CQC_SIM1, AMISTD_1, GRFUNC_1, NAT_1, ORDINAL1,
CARD_1, TREES_2, SUBSET_1, FUNCT_2, TREES_1, FINSEQ_1, FUNCT_1, PARTFUN1,
XBOOLE_1, RELAT_1, FINSEQ_3, FINSEQ_5, AXIOMS, TARSKI, QC_LANG4, CARD_5,
FINSEQ_2, XBOOLE_0, AMI_5, AMISTD_2, CQC_LANG, CARD_2, WELLORD2,
ENUMSET1, WELLORD1, ZFMISC_1, AMI_1, TOLER_1, ORDERS_2, CARD_4, FINSET_1,
FUNCOP_1, RELSET_1, MEMBERED;
schemes FRAENKEL, TREES_2, FUNCT_2, NAT_1, HILBERT2, ORDINAL2;
begin
:: Preliminaries
reserve x, y, X for set,
m, n for natural number,
O for Ordinal,
R, S for Relation;
definition
let D be set, f be PartFunc of D,NAT, n be set;
cluster f.n -> natural;
coherence
proof
per cases;
suppose n in dom f;
then reconsider a = f.n as Nat by PARTFUN1:27;
a is natural;
hence thesis;
suppose not n in dom f;
hence thesis by FUNCT_1:def 4;
end;
end;
definition
let R be empty Relation, X be set;
cluster R|X -> empty;
coherence
proof
dom R misses X by XBOOLE_1:65;
hence thesis by RELAT_1:95;
end;
end;
theorem Th1:
dom R = {x} & rng R = {y} implies R = x .--> y
proof
assume that
A1: dom R = {x} and
A2: rng R = {y};
set g = x .--> y;
A3: g = {[x,y]} by AMI_1:19;
for a, b being set holds [a,b] in R iff [a,b] in g
proof
let a, b be set;
hereby
assume [a,b] in R;
then a in dom R & b in rng R by RELAT_1:20;
then a = x & b = y by A1,A2,TARSKI:def 1;
hence [a,b] in g by A3,TARSKI:def 1;
end;
assume [a,b] in g;
then [a,b] = [x,y] by A3,TARSKI:def 1;
then
A4: a = x & b = y by ZFMISC_1:33;
then a in dom R by A1,TARSKI:def 1;
then consider z being set such that
A5: [a,z] in R by RELAT_1:def 4;
z in rng R by A5,RELAT_1:20;
hence [a,b] in R by A5,A2,A4,TARSKI:def 1;
end;
hence thesis by RELAT_1:def 2;
end;
theorem Th2:
field {[x,x]} = {x}
proof
thus field {[x,x]} = {x,x} by RELAT_1:32
.= {x} by ENUMSET1:69;
end;
definition
let X be infinite set, a be set;
cluster X --> a -> infinite;
coherence
proof
assume X --> a is finite;
then reconsider f = X --> a as finite Relation;
dom f is finite;
hence thesis by FUNCOP_1:19;
end;
end;
definition
cluster infinite Function;
existence
proof
take NAT --> 0;
thus thesis;
end;
end;
definition
let R be finite Relation;
cluster field R -> finite;
coherence
proof
field R = dom R \/ rng R by RELAT_1:def 6;
hence thesis;
end;
end;
theorem Th3:
field R is finite implies R is finite
proof
assume field R is finite;
then reconsider A = field R as finite set;
R c= [:A,A:] by ORDERS_2:82;
hence thesis by FINSET_1:13;
end;
definition
let R be infinite Relation;
cluster field R -> infinite;
coherence by Th3;
end;
theorem
dom R is finite & rng R is finite implies R is finite
proof
assume dom R is finite & rng R is finite;
then dom R \/ rng R is finite by FINSET_1:14;
then field R is finite by RELAT_1:def 6;
hence thesis by Th3;
end;
definition
cluster RelIncl {} -> empty;
coherence
proof
for Y,Z being set st Y in {} & Z in {} holds [Y,Z] in {} iff Y c= Z;
hence thesis by TOLER_1:1,WELLORD2:def 1;
end;
end;
definition
let X be non empty set;
cluster RelIncl X -> non empty;
coherence
proof
consider a being Element of X;
[a,a] in RelIncl X by WELLORD2:def 1;
hence thesis;
end;
end;
theorem Th5:
RelIncl {x} = {[x,x]}
proof
A1: field {[x,x]} = {x} by Th2;
for Y,Z being set st Y in {x} & Z in {x} holds [Y,Z] in {[x,x]} iff Y c= Z
proof
let Y,Z be set;
assume Y in {x} & Z in {x};
then
A2: Y = x & Z = x by TARSKI:def 1;
hence [Y,Z] in {[x,x]} implies Y c= Z;
thus thesis by A2,TARSKI:def 1;
end;
hence thesis by A1,WELLORD2:def 1;
end;
theorem Th6:
RelIncl X c= [:X,X:]
proof
set R = RelIncl X;
let x be set;
assume
A1: x in R;
then consider a, b being set such that
A2: x = [a,b] by RELAT_1:def 1;
a in field R & b in field R by A1,A2,RELAT_1:30;
then a in X & b in X by WELLORD2:def 1;
hence thesis by A2,ZFMISC_1:106;
end;
definition
let X be finite set;
cluster RelIncl X -> finite;
coherence
proof
RelIncl X c= [:X,X:] by Th6;
hence thesis by FINSET_1:13;
end;
end;
theorem Th7:
RelIncl X is finite implies X is finite
proof
set R = RelIncl X;
assume R is finite;
then reconsider A = R as finite Relation;
field A is finite;
hence thesis by WELLORD2:def 1;
end;
definition
let X be infinite set;
cluster RelIncl X -> infinite;
coherence by Th7;
end;
theorem
R,S are_isomorphic & R is well-ordering implies S is well-ordering
proof
assume R,S are_isomorphic;
then ex F being Function st F is_isomorphism_of R,S by WELLORD1:def 8;
hence thesis by WELLORD1:54;
end;
theorem Th9:
R,S are_isomorphic & R is finite implies S is finite
proof
given F being Function such that
A1: F is_isomorphism_of R,S;
assume R is finite;
then reconsider R as finite Relation;
field R is finite;
then dom F is finite by A1,WELLORD1:def 7;
then rng F is finite by FINSET_1:26;
then field S is finite by A1,WELLORD1:def 7;
hence S is finite by Th3;
end;
theorem Th10:
x .--> y is_isomorphism_of {[x,x]},{[y,y]}
proof
set F = x .--> y;
set R = {[x,x]};
set S = {[y,y]};
A1: field R = {x} by Th2;
hence dom F = field R by CQC_LANG:5;
field S = {y} by Th2;
hence rng F = field S by CQC_LANG:5;
thus F is one-to-one;
let a,b be set;
hereby
assume [a,b] in R;
then [a,b] = [x,x] by TARSKI:def 1;
then
A2: a = x & b = x by ZFMISC_1:33;
hence a in field R & b in field R by A1,TARSKI:def 1;
F.x = y by CQC_LANG:6;
hence [F.a,F.b] in S by A2,TARSKI:def 1;
end;
assume a in field R & b in field R;
then a = x & b = x by A1,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem
{[x,x]}, {[y,y]} are_isomorphic
proof
take f = x .--> y;
thus f is_isomorphism_of {[x,x]},{[y,y]} by Th10;
end;
definition
cluster order_type_of {} -> empty;
coherence
proof
{},RelIncl {} are_isomorphic by WELLORD1:48;
hence thesis by ORDERS_2:21,WELLORD2:def 2;
end;
end;
theorem
order_type_of RelIncl O = O
proof
A1: RelIncl O is well-ordering by WELLORD2:7;
RelIncl O,RelIncl O are_isomorphic by WELLORD1:48;
hence thesis by A1,WELLORD2:def 2;
end;
Lm1:
for X being finite set st X c= O holds order_type_of RelIncl X is finite
proof
let X be finite set;
assume X c= O;
then RelIncl X is well-ordering by WELLORD2:9;
then
RelIncl X,RelIncl order_type_of RelIncl X are_isomorphic by WELLORD2:def 2;
then RelIncl order_type_of RelIncl X is finite by Th9;
hence thesis by Th7;
end;
theorem Th13:
for X being finite set st X c= O holds order_type_of RelIncl X = card X
proof
let X be finite set;
assume
A1: X c= O;
then
A2: card X = Card order_type_of RelIncl X by CARD_5:16;
order_type_of RelIncl X is finite by A1,Lm1;
then order_type_of RelIncl X in omega by CARD_4:7;
hence thesis by A2,CARD_1:66;
end;
theorem Th14:
{x} c= O implies order_type_of RelIncl {x} = 1
proof
card {x} = 1 by CARD_2:60;
hence thesis by Th13;
end;
theorem Th15:
{x} c= O implies
canonical_isomorphism_of (RelIncl order_type_of RelIncl {x}, RelIncl {x})
= 0 .--> x
proof
set X = {x};
set R = RelIncl X;
set C = canonical_isomorphism_of (RelIncl order_type_of R,R);
assume
A1: X c= O;
then R is well-ordering by WELLORD2:9;
then R, RelIncl order_type_of R are_isomorphic by WELLORD2:def 2;
then
A2:RelIncl order_type_of R, R are_isomorphic by WELLORD1:50;
RelIncl order_type_of R is well-ordering by WELLORD2:9;
then
A3:C is_isomorphism_of RelIncl order_type_of R, R by A2,WELLORD1:def 9;
A4:RelIncl {0} = {[0,0]} by Th5;
A5:order_type_of R = {0} by A1,Th14,CARD_5:1;
then
A6:dom canonical_isomorphism_of(RelIncl {0}, R) = field RelIncl {0}
by A3,WELLORD1:def 7
.= {0} by A4,Th2;
rng canonical_isomorphism_of(RelIncl {0}, R) = field R
by A5,A3,WELLORD1:def 7
.= X by WELLORD2:def 1;
hence thesis by A5,A6,Th1;
end;
definition
let O be Ordinal,
X be Subset of O,
n be set;
cluster canonical_isomorphism_of
(RelIncl order_type_of RelIncl X,RelIncl X).n
-> ordinal;
coherence
proof
consider phi being Ordinal-Sequence such that
A1:phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X, RelIncl X) &
phi is increasing & dom phi = order_type_of RelIncl X and
A2:rng phi = X by CARD_5:14;
per cases;
suppose n in dom phi;
then phi.n in rng phi by FUNCT_1:def 5;
hence thesis by A1,A2,ORDINAL1:23;
suppose not n in dom phi;
hence thesis by A1,FUNCT_1:def 4;
end;
end;
definition
let X be natural-membered set,
n be set;
cluster canonical_isomorphism_of
(RelIncl order_type_of RelIncl X,RelIncl X).n
-> natural;
coherence
proof
X c= NAT
proof
let x be set;
assume x in X;
then x is natural by MEMBERED:def 5;
hence thesis by ORDINAL2:def 21;
end;
then reconsider X as Subset of NAT;
consider phi being Ordinal-Sequence such that
A1:phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X, RelIncl X) &
phi is increasing & dom phi = order_type_of RelIncl X and
A2:rng phi = X by CARD_5:14;
per cases;
suppose
A3: n in dom phi;
then
A4:phi.n in rng phi by FUNCT_1:def 5;
reconsider a = phi.n as Element of X by A2,A3,FUNCT_1:def 5;
a is Nat by A2,A4;
hence thesis by A1;
suppose not n in dom phi;
hence thesis by A1,FUNCT_1:def 4;
end;
end;
:: Trees
theorem Th16:
n |-> x = m |-> x implies n = m
proof
len(n |-> x) = n & len(m |-> x) = m by FINSEQ_2:69;
hence thesis;
end;
theorem Th17:
for T being Tree, t being Element of T holds t|Seg n in T
proof
let T be Tree,
t be Element of T;
t|Seg n is_a_prefix_of t by RELAT_1:88;
hence thesis by TREES_1:45;
end;
theorem Th18:
for T1, T2 being Tree st
for n being Nat holds T1-level n = T2-level n holds
T1 = T2
proof
let T1, T2 be Tree such that
A1: for n being Nat holds T1-level n = T2-level n;
for p being FinSequence of NAT holds p in T1 iff p in T2
proof
let p be FinSequence of NAT;
A2: T1 = union { T1-level n where n is Nat: not contradiction } by TREES_2:16;
A3: T2 = union { T2-level n where n is Nat: not contradiction } by TREES_2:16;
hereby
assume p in T1;
then consider Y being set such that
A4: p in Y and
A5: Y in { T1-level n where n is Nat: not contradiction }
by A2,TARSKI:def 4;
consider n being Nat such that
A6: Y = T1-level n by A5;
Y = T2-level n by A1,A6;
hence p in T2 by A4;
end;
assume p in T2;
then consider Y being set such that
A7: p in Y and
A8: Y in { T2-level n where n is Nat: not contradiction }
by A3,TARSKI:def 4;
consider n being Nat such that
A9: Y = T2-level n by A8;
Y = T1-level n by A1,A9;
hence p in T1 by A7;
end;
hence T1 = T2 by TREES_2:7;
end;
definition
func TrivialInfiniteTree equals :Def1:
{ k |-> 0 where k is Nat: not contradiction };
coherence;
end;
definition
cluster TrivialInfiniteTree -> non empty Tree-like;
coherence
proof
set X = TrivialInfiniteTree;
0 |-> 0 in X by Def1;
hence X is non empty;
thus X c= NAT*
proof
let x be set;
assume x in X;
then ex k being Nat st x = k |-> 0 by Def1;
then x is FinSequence of NAT by FINSEQ_2:77;
hence thesis by FINSEQ_1:def 11;
end;
thus for p being FinSequence of NAT st p in X holds ProperPrefixes p c= X
proof
let p be FinSequence of NAT;
assume p in X;
then consider m being Nat such that
A1: p = m |-> 0 by Def1;
let x be set;
assume
A2: x in ProperPrefixes p;
then reconsider x as FinSequence by TREES_1:35;
A3: len x = len (len x |-> 0) by FINSEQ_2:69;
for k being Nat st 1 <= k & k <= len x holds x.k = (len x |-> 0).k
proof
let k be Nat;
assume 1 <= k & k <= len x;
then
A4: k in dom x by FINSEQ_3:27;
then
A5: k in Seg len x by FINSEQ_1:def 3;
len x < len p by A2,TREES_1:37;
then Seg len x c= Seg len p by FINSEQ_1:7;
then k in Seg len p by A5;
then
A6: k in Seg m by A1,FINSEQ_2:69;
x is_a_proper_prefix_of p by A2,TREES_1:36;
then
A7: x c= p by XBOOLE_0:def 8;
thus (len x |-> 0).k = 0 by A5,FINSEQ_2:70
.= p.k by A1,A6,FINSEQ_2:70
.= x.k by A4,A7,GRFUNC_1:8;
end;
then x = len x |-> 0 by A3,FINSEQ_1:18;
hence thesis by Def1;
end;
let p be FinSequence of NAT,
m, n be Nat;
assume p^<*m*> in X;
then consider k being Nat such that
A8: p^<*m*> = k |-> 0 by Def1;
assume
A9: n <= m;
A10: len (p^<*m*>) = len p + 1 by FINSEQ_2:19;
A11: len (p^<*m*>) = k by A8,FINSEQ_2:69;
A12: (p^<*m*>).len (p^<*m*>) = m by A10,FINSEQ_1:59;
0 = k or 0 < k by NAT_1:18;
then 0+1 <= k by A8,NAT_1:38,FINSEQ_2:72;
then k in Seg k by FINSEQ_1:3;
then
A13: m = 0 by A12,A8,A11,FINSEQ_2:70;
A14: len (p^<*n*>) = len (len (p^<*n*>) |-> 0) by FINSEQ_2:69;
for z being Nat st 1 <= z & z <= len (p^<*n*>) holds
(len (p^<*n*>) |-> 0).z = (p^<*n*>).z
proof
let z be Nat;
assume that
A15: 1 <= z and
A16: z <= len (p^<*n*>);
z in dom (p^<*n*>) by A15,A16,FINSEQ_3:27;
then
A17: z in Seg len (p^<*n*>) by FINSEQ_1:def 3;
len (p^<*n*>) = len p + 1 by FINSEQ_2:19;
then
A18: z in Seg k by A15,A16,A11,A10,FINSEQ_1:3;
thus (len (p^<*n*>) |-> 0).z = 0 by A17,FINSEQ_2:70
.= (p^<*m*>).z by A8,A18,FINSEQ_2:70
.= (p^<*n*>).z by A13,A9,NAT_1:19;
end;
then len (p^<*n*>) |-> 0 = p^<*n*> by A14,FINSEQ_1:18;
hence p^<*n*> in X by Def1;
end;
end;
theorem Th19:
NAT,TrivialInfiniteTree are_equipotent
proof
defpred P[Nat,set] means $2 = $1 |-> 0;
A1: for x being Element of NAT
ex y being Element of TrivialInfiniteTree st P[x,y]
proof
let x be Element of NAT;
x |-> 0 in TrivialInfiniteTree by Def1;
then reconsider y = x |-> 0 as Element of TrivialInfiniteTree;
take y;
thus thesis;
end;
consider f being Function of NAT,TrivialInfiniteTree such that
A2: for x being Element of NAT holds P[x,f.x] from FuncExD(A1);
take f;
thus f is one-to-one
proof
let x,y be set;
assume
A3: x in dom f & y in dom f;
assume
A4: f.x = f.y;
reconsider x, y as Nat by A3,FUNCT_2:def 1;
P[x,f.x] & P[y,f.y] by A2;
hence thesis by A4,Th16;
end;
thus
A5: dom f = NAT by FUNCT_2:def 1;
thus rng f c= TrivialInfiniteTree by RELSET_1:12;
let a be set;
assume a in TrivialInfiniteTree;
then consider k being Nat such that
A6: a = k |-> 0 by Def1;
k in dom f & f.k = a by A2,A6,A5;
hence thesis by FUNCT_1:def 5;
end;
definition
cluster TrivialInfiniteTree -> infinite;
coherence by Th19,CARD_1:68;
end;
theorem Th20:
for n being Nat holds TrivialInfiniteTree-level n = { n |-> 0 }
proof
let n be Nat;
set T = TrivialInfiniteTree;
set L = { w where w is Element of T: len w = n };
set f = n |-> 0;
{f} = L
proof
hereby
let a be set;
assume a in {f};
then
A1: a = f by TARSKI:def 1;
A2: f in T by Def1;
len f = n by FINSEQ_2:69;
hence a in L by A1,A2;
end;
let a be set;
assume a in L;
then consider w being Element of T such that
A3: a = w & len w = n;
w in T;
then ex k being Nat st w = k |-> 0 by Def1;
then a = f by A3,FINSEQ_2:69;
hence a in {f} by TARSKI:def 1;
end;
hence thesis by TREES_2:def 6;
end;
:: First Location
reserve
N for with_non-empty_elements set,
S for standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
L, l1 for Instruction-Location of S,
J for Instruction of S,
F for Subset of the Instruction-Locations of S;
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 FinPartState of S such that
A1: F is non empty and
A2: F is programmed;
func FirstLoc F -> Instruction-Location of S means :Def2:
ex M being non empty Subset of NAT st
M = { locnum l where l is Element of the Instruction-Locations of S
: l in dom F } &
it = il.(S, min M);
existence
proof
deffunc G(Element of the Instruction-Locations of S) = locnum $1;
reconsider F as non empty programmed FinPartState of S by A1,A2;
set M = { G(l) where l is Element of the Instruction-Locations of S
: l in dom F };
A3: dom F is finite;
A4: M is finite from FraenkelFin(A3);
consider l being Element of dom F;
l in dom F & dom F c= the Instruction-Locations of S by AMI_3:def 13;
then reconsider l as Element of the Instruction-Locations of S;
A5: locnum l in M;
M c= NAT
proof
let k be set;
assume k in M;
then ex l being Element of the Instruction-Locations of S st
k = locnum l & l in dom F;
hence k in NAT;
end;
then reconsider M as finite non empty Subset of NAT by A4,A5;
take il.(S, min M), M;
thus thesis;
end;
uniqueness;
end;
theorem Th21:
for F being non empty programmed FinPartState of S holds
FirstLoc F in dom F
proof
let F be non empty programmed FinPartState of S;
consider M being non empty Subset of NAT such that
A1: M = { locnum l where l is Element of the Instruction-Locations of S
: l in dom F } and
A2: FirstLoc F = il.(S,min M) by Def2;
min M in M by CQC_SIM1:def 8;
then ex l being Element of the Instruction-Locations of S st
min M = locnum l & l in dom F by A1;
hence FirstLoc F in dom F by A2,AMISTD_1:def 13;
end;
theorem
for F, G being non empty programmed FinPartState of S st F c= G holds
FirstLoc G <= FirstLoc F
proof
let F, G be non empty programmed FinPartState of S such that
A1: F c= G;
consider M being non empty Subset of NAT such that
A2: M = { locnum l where l is Element of the Instruction-Locations of S
: l in dom F } and
A3: FirstLoc F = il.(S,min M) by Def2;
consider N being non empty Subset of NAT such that
A4: N = { locnum l where l is Element of the Instruction-Locations of S
: l in dom G } and
A5: FirstLoc G = il.(S,min N) by Def2;
M c= N
proof
let a be set;
assume a in M;
then
A6: ex l being Element of the Instruction-Locations of S st
a = locnum l & l in dom F by A2;
dom F c= dom G by A1,GRFUNC_1:8;
hence a in N by A4,A6;
end;
then min N <= min M by CQC_SIM1:19;
hence thesis by A3,A5,AMISTD_1:28;
end;
theorem Th23:
for F being non empty programmed FinPartState of S st l1 in dom F holds
FirstLoc F <= l1
proof
let F be non empty programmed FinPartState of S such that
A1: l1 in dom F;
consider M being non empty Subset of NAT such that
A2: M = { locnum w where w is Element of the Instruction-Locations of S
: w in dom F } and
A3: FirstLoc F = il.(S,min M) by Def2;
A4: locnum FirstLoc F = min M by A3,AMISTD_1:def 13;
locnum l1 in M by A1,A2;
then min M <= locnum l1 by CQC_SIM1:def 8;
hence FirstLoc F <= l1 by A4,AMISTD_1:29;
end;
theorem
for F being lower non empty programmed FinPartState of S holds
FirstLoc F = il.(S,0)
proof
let F be lower non empty programmed FinPartState of S;
consider M being non empty Subset of NAT such that
M = { locnum l where l is Element of the Instruction-Locations of S
: l in dom F } and
A1: FirstLoc F = il.(S,min M) by Def2;
A2: FirstLoc F in dom F by Th21;
0 <= min M by NAT_1:18;
then
A3:il.(S,0) <= il.(S,min M) by AMISTD_1:28;
then il.(S,0) in dom F by A2,A1,AMISTD_1:def 20;
then FirstLoc F <= il.(S,0) by Th23;
hence thesis by A3,A1,AMISTD_1:def 9;
end;
:: LocNums
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 Subset of the Instruction-Locations of S;
func LocNums F -> Subset of NAT equals :Def3:
{locnum l where l is Instruction-Location of S : l in F};
coherence
proof
set A = {locnum l where l is Instruction-Location of S : l in F};
A c= NAT
proof
let a be set;
assume a in A;
then ex l being Instruction-Location of S st a = locnum l & l in F;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th25:
locnum l1 in LocNums F iff l1 in F
proof
A1:LocNums F =
{locnum l where l is Instruction-Location of S : l in F} by Def3;
hereby
assume locnum l1 in LocNums F;
then ex l being Instruction-Location of S st locnum l1 = locnum l &
l in F by A1;
hence l1 in F by AMISTD_1:27;
end;
thus thesis by A1;
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 Subset of the Instruction-Locations of S;
cluster LocNums F -> empty;
coherence
proof
A1:LocNums F =
{locnum l where l is Instruction-Location of S : l in F} by Def3;
assume LocNums F is non empty;
then consider x being set such that
A2: x in LocNums F by XBOOLE_0:def 1;
ex l being Instruction-Location of S st x = locnum l & l in 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 Subset of the Instruction-Locations of S;
cluster LocNums F -> non empty;
coherence
proof
ex l being Instruction-Location of S st l in F by SUBSET_1:10;
hence thesis by Th25;
end;
end;
theorem Th26:
F = {il.(S,n)} implies LocNums F = {n}
proof
assume
A1: F = {il.(S,n)};
A2: il.(S,n) in {il.(S,n)} by TARSKI:def 1;
A3: locnum il.(S,n) = n by AMISTD_1:def 13;
A4: LocNums F = {locnum l where l is Instruction-Location of S : l in F}
by Def3;
hereby
let x be set;
assume x in LocNums F;
then consider l being Instruction-Location of S such that
A5: x = locnum l and
A6: l in F by A4;
l = il.(S,n) by A1,A6,TARSKI:def 1;
then x = n by A5,AMISTD_1:def 13;
hence x in {n} by TARSKI:def 1;
end;
let x be set;
assume x in {n};
then x = n by TARSKI:def 1;
hence thesis by A1,A2,A3,Th25;
end;
theorem Th27:
F, LocNums F are_equipotent
proof
A1:LocNums F = {locnum l where l is Instruction-Location of S : l in F}
by Def3;
per cases;
suppose F is empty;
then reconsider F as empty Subset of the Instruction-Locations of S;
LocNums F is empty;
hence thesis;
suppose
A2: F is non empty;
LocNums F,F are_equipotent
proof
defpred P[Nat,set] means $2 = il.(S,$1);
A3: for x being set st x in LocNums F ex y being set st y in F & P[x,y]
proof
let x be set;
assume x in LocNums F;
then consider l being Instruction-Location of S such that
A4: x = locnum l & l in F by A1;
take l;
thus thesis by A4,AMISTD_1:def 13;
end;
consider f being Function of LocNums F,F such that
A5: for x being set st x in LocNums F holds P[x,f.x] from FuncEx1(A3);
take f;
thus f is one-to-one
proof
let x,y be set;
assume that
A6: x in dom f and
A7: y in dom f and
A8: f.x = f.y;
A9: dom f = LocNums F by A2,FUNCT_2:def 1;
then
A10: ex l1 being Instruction-Location of S st x = locnum l1 & l1 in F by A6,A1;
A11: ex l2 being Instruction-Location of S st y = locnum l2 & l2 in F
by A7,A1,A9;
P[x,f.x] & P[y,f.y] by A5,A6,A7,A9;
hence thesis by A8,A10,A11,AMISTD_1:25;
end;
thus
A12: dom f = LocNums F by A2,FUNCT_2:def 1;
thus rng f c= F by RELSET_1:12;
let a be set;
assume
A13: a in F;
then reconsider l = a as Instruction-Location of S;
A14:locnum l in dom f by A12,A13,A1;
then P[locnum l,f.locnum l] by A5,A12;
then f.locnum l = a by AMISTD_1:def 13;
hence thesis by A14,FUNCT_1:def 5;
end;
hence thesis;
end;
theorem Th28:
Card F c= order_type_of RelIncl LocNums F
proof
set X = LocNums F;
A1: Card X = Card order_type_of RelIncl X by CARD_5:16;
F,X are_equipotent by Th27;
then Card F = Card X by CARD_1:21;
hence thesis by A1,CARD_1:24;
end;
theorem Th29:
S is realistic & J is halting implies LocNums NIC(J,L) = {locnum L}
proof
assume S is realistic & J is halting;
then NIC(J,L) = {L} by AMISTD_1:15
.= {il.(S,locnum L)} by AMISTD_1:def 13;
hence thesis by Th26;
end;
theorem
S is realistic & J is sequential implies
LocNums NIC(J,L) = {locnum NextLoc L}
proof
assume S is realistic & J is sequential;
then NIC(J,L) = {NextLoc L} by AMISTD_1:41
.= {il.(S,locnum NextLoc L)} by AMISTD_1:def 13;
hence thesis by Th26;
end;
:: LocSeq
definition
let N be with_non-empty_elements set,
S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
M be Subset of the Instruction-Locations of S;
deffunc F(set) = il.(S, canonical_isomorphism_of
(RelIncl order_type_of RelIncl LocNums M,RelIncl LocNums M).$1);
set Z = the Instruction-Locations of S;
func LocSeq M -> T-Sequence of the Instruction-Locations of S means :Def4:
dom it = Card M &
for m being set st m in Card M holds
it.m = il.(S, canonical_isomorphism_of
(RelIncl order_type_of RelIncl LocNums M,
RelIncl LocNums M).m);
existence
proof
consider f being T-Sequence such that
A1: dom f = Card M and
A2: for A being Ordinal st A in Card M holds f.A = F(A) from TS_Lambda;
take f;
thus f is T-Sequence of Z
proof
let y be set;
assume y in rng f;
then consider x being set such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 5;
x is Ordinal by A3,ORDINAL1:23;
then f.x = F(x) by A1,A2,A3;
hence y in Z by A4;
end;
thus dom f = Card M by A1;
let m be set;
assume
A5: m in Card M;
then m is Ordinal by ORDINAL1:23;
hence thesis by A2,A5;
end;
uniqueness
proof
let f, g be T-Sequence of Z such that
A6: dom f = Card M and
A7: for m being set st m in Card M holds f.m = F(m) and
A8: dom g = Card M and
A9: for m being set st m in Card M holds g.m = F(m);
for x being set st x in dom f holds f.x = g.x
proof
let x be set such that
A10: x in dom f;
thus f.x = F(x) by A6,A7,A10
.= g.x by A6,A9,A10;
end;
hence thesis by A6,A8,FUNCT_1:9;
end;
end;
theorem
F = {il.(S,n)} implies LocSeq F = 0 .--> il.(S,n)
proof
assume
A1: F = {il.(S,n)};
then
A2:LocNums F = {n} by Th26;
{n} c= omega
proof
let a be set;
assume a in {n};
then a = n by TARSKI:def 1;
hence thesis by ORDINAL2:def 21;
end;
then
A3:canonical_isomorphism_of(RelIncl order_type_of RelIncl {n}, RelIncl {n}).0
= (0 .--> n).0 by Th15
.= n by CQC_LANG:6;
A4: dom LocSeq F = Card F by Def4;
A5: Card F = {0} by A1,CARD_1:50,CARD_2:20,CARD_5:1;
A6: dom (0 .--> il.(S,n)) = {0} by CQC_LANG:5;
for a being set st a in dom LocSeq F holds (LocSeq F).a = (0 .--> il.(S,n)).a
proof
let a be set;
assume
A7: a in dom LocSeq F;
then
A8: a = 0 by A4,A5,TARSKI:def 1;
thus (LocSeq F).a = il.(S, canonical_isomorphism_of
(RelIncl order_type_of RelIncl LocNums F,
RelIncl LocNums F).a) by A4,A7,Def4
.= (0 .--> il.(S,n)).a by A8,CQC_LANG:6,A3,A2;
end;
hence LocSeq F = 0 .--> il.(S,n) by A4,A5,A6,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)),
M be Subset of the Instruction-Locations of S;
cluster LocSeq M -> one-to-one;
coherence
proof
set f = LocSeq M;
set X = LocNums M;
set C = canonical_isomorphism_of (RelIncl order_type_of RelIncl X,RelIncl X);
let x1,x2 be set such that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f.x1 = f.x2;
A4: dom f = Card M by Def4;
then
A5: f.x1 = il.(S,C.x1) by A1,Def4;
f.x2 = il.(S,C.x2) by A2,A4,Def4;
then
A6:C.x1 = C.x2 by A3,A5,AMISTD_1:25;
consider phi being Ordinal-Sequence such that
A7:phi = C
and
A8: phi is increasing and
A9: dom phi = order_type_of RelIncl X and rng phi = X by CARD_5:14;
A10:phi is one-to-one by A8,CARD_5:20;
Card M c= order_type_of RelIncl X by Th28;
hence x1 = x2 by A7,A6,A10,A1,A2,A4,A9,FUNCT_1:def 8;
end;
end;
:: Tree of Execution
definition
let N be with_non-empty_elements set,
S be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
M be FinPartState of S;
func ExecTree(M) -> DecoratedTree of the Instruction-Locations of S means
:Def5:
it.{} = FirstLoc(M) &
for t being Element of dom it holds
succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,it.t),it.t) } &
for m being Nat st m in Card NIC(pi(M,it.t),it.t) holds
it.(t^<*m*>) = (LocSeq NIC(pi(M,it.t),it.t)).m;
existence
proof
set D = the Instruction-Locations of S;
defpred P[Instruction-Location of S,Nat,set] means
($2 in dom LocSeq NIC(pi(M,$1),$1) implies
$3 = (LocSeq NIC(pi(M,$1),$1)).$2) &
(not $2 in dom LocSeq NIC(pi(M,$1),$1) implies $3 = il.(S,0));
A1: for x being Element of D, y being Element of NAT
ex z being Element of D st P[x,y,z]
proof
let x be Element of D, y be Element of NAT;
set z = (LocSeq NIC(pi(M,x),x)).y;
per cases;
suppose
A2: y in dom LocSeq NIC(pi(M,x),x);
then
A3: z in rng LocSeq NIC(pi(M,x),x) by FUNCT_1:def 5;
take z;
rng LocSeq NIC(pi(M,x),x) c= D by ORDINAL1:def 8;
then z in D by A3;
hence thesis by A2;
suppose
A4: not y in dom LocSeq NIC(pi(M,x),x);
take il.(S,0);
thus thesis by A4;
end;
consider f be Function of [:D,NAT:],D such that
A5: for l being Instruction-Location of S, n being Nat holds
P[l,n,f.[l,n]] from FuncEx2D(A1);
deffunc F(Instruction-Location of S) = Card NIC(pi(M,$1),$1);
A6: for d being Element of D,
k1, k2 being Nat st k1 <= k2 & k2 in F(d) holds k1 in F(d)
proof
let d be Element of D,
k1, k2 be Nat such that
A7: k1 <= k2 and
A8: k2 in F(d);
k1 c= k2 by A7,CARD_1:56;
hence thesis by A8,ORDINAL1:22;
end;
consider T being DecoratedTree of D such that
A9:T.{} = FirstLoc(M) and
A10:for t being Element of dom T holds
succ t = { t^<*k*> where k is Nat: k in F(T.t)} &
for n being Nat, x being set st x = T.t & n in F(x) holds
T.(t^<*n*>) = f.[x,n] from DTreeStructEx(A6);
take T;
thus T.{} = FirstLoc(M) by A9;
let t be Element of dom T;
thus succ t = { t^<*k*> where k is Nat: k in F(T.t)} by A10;
let m be Nat;
assume
A11: m in Card NIC(pi(M,T.t),T.t);
A12: dom LocSeq NIC(pi(M,T.t),T.t) = Card NIC(pi(M,T.t),T.t) by Def4;
thus T.(t^<*m*>) = f.[T.t,m] by A10,A11
.= (LocSeq NIC(pi(M,T.t),T.t)).m by A5,A11,A12;
end;
uniqueness
proof
let T1,T2 be DecoratedTree of the Instruction-Locations of S such that
A13: T1.{} = FirstLoc(M) and
A14: for t being Element of dom T1 holds
succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t),T1.t)} &
for m being Nat st m in Card NIC(pi(M,T1.t),T1.t) holds
T1.(t^<*m*>) = (LocSeq NIC(pi(M,T1.t),T1.t)).m and
A15: T2.{} = FirstLoc(M) and
A16: for t being Element of dom T2 holds
succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,T2.t),T2.t)} &
for m being Nat st m in Card NIC(pi(M,T2.t),T2.t) holds
T2.(t^<*m*>) = (LocSeq NIC(pi(M,T2.t),T2.t)).m;
defpred P[Nat] means dom T1-level $1 = dom T2-level $1;
A17:P[0]
proof
thus dom T1-level 0 = {{}} by QC_LANG4:17
.= dom T2-level 0 by QC_LANG4:17;
end;
A18:for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A19: P[n];
set U1 = { succ w where w is Element of dom T1 : len w = n };
set U2 = { succ w where w is Element of dom T2 : len w = n };
A20: dom T1-level (n+1) = union U1 by QC_LANG4:18;
A21: dom T1-level n = {v where v is Element of dom T1: len v = n}
by TREES_2:def 6;
A22: dom T2-level n = {v where v is Element of dom T2: len v = n}
by TREES_2:def 6;
union U1 = union U2
proof
hereby
let a be set;
assume a in union U1;
then consider A being set such that
A23: a in A and
A24: A in U1 by TARSKI:def 4;
consider w being Element of dom T1 such that
A25: A = succ w and
A26: len w = n by A24;
w in dom T1-level n by A26,A21;
then consider v being Element of dom T2 such that
A27: w = v and
A28: len v = n by A22,A19;
A29: succ v = {v^<*k*> where k is Nat: k in Card NIC(pi(M,T2.v),T2.v)}
by A16;
A30: succ w = {w^<*k*> where k is Nat: k in Card NIC(pi(M,T1.w),T1.w)}
by A14;
defpred R[Nat] means
$1 <= len w & w|Seg $1 in dom T1 & v|Seg $1 in dom T2 implies
T1.(w|Seg $1) = T2.(w|Seg $1);
A31: R[0]
proof
assume 0 <= len w;
assume w|Seg 0 in dom T1;
assume v|Seg 0 in dom T2;
w|{} = {} by RELAT_1:110;
hence T1.(w|Seg 0) = T2.(w|Seg 0) by A15,A13,FINSEQ_1:4;
end;
A32: for n being Nat st R[n] holds R[n+1]
proof
let n be Nat;
assume that
A33: R[n] and
A34: n+1 <= len w and
A35: w|Seg (n+1) in dom T1 and
A36: v|Seg (n+1) in dom T2;
set t1 = w|Seg n;
A37: n <= n+1 by NAT_1:29;
then
A38: Seg n c= Seg(n+1) by FINSEQ_1:7;
then
w|Seg n = w|Seg(n+1)|Seg n by RELAT_1:103;
then
A39: w|Seg n is_a_prefix_of w|Seg(n+1) by TREES_1:def 1;
v|Seg n = v|Seg(n+1)|Seg n by A38,RELAT_1:103;
then
A40: v|Seg n is_a_prefix_of v|Seg(n+1) by TREES_1:def 1;
A41: (w|Seg(n+1)).len(w|Seg(n+1)) is Nat by ORDINAL2:def 21;
A42: 1 <= n+1 by NAT_1:29;
then
A43: n+1 in dom w by A34,FINSEQ_3:27;
A44: len(w|Seg(n+1)) = n+1 by A34,FINSEQ_1:21;
then len(w|Seg(n+1)) in Seg(n+1) by A42,FINSEQ_1:3;
then w.(n+1) = (w|Seg(n+1)).len(w|Seg(n+1)) by A44,FUNCT_1:72;
then
A45: w|Seg(n+1) = t1^<*(w|Seg(n+1)).len (w|Seg(n+1))*> by A43,FINSEQ_5:11;
reconsider t1 as Element of dom T1 by A39,A35,TREES_1:45;
reconsider t2 = t1 as Element of dom T2 by A27,A40,A36,TREES_1:45;
A46: succ t1 = { t1^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t1),T1.t1)}
by A14;
t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> in succ t1 by A45,A41,A35,TREES_2:14;
then consider k being Nat such that
A47: t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> = t1^<*k*> and
A48: k in Card NIC(pi(M,T1.t1),T1.t1) by A46;
A49: k = (w|Seg(n+1)).len(w|Seg(n+1)) by A47,FINSEQ_2:20;
A50: (w|Seg(n+1)).len(w|Seg(n+1)) in Card NIC(pi(M,T2.t2),T2.t2)
by A48,A47,A40,A33,A36,A37,A34,AXIOMS:22,TREES_1:45,FINSEQ_2:20;
thus T1.(w|Seg(n+1)) =
(LocSeq NIC(pi(M,T1.t1),T1.t1)).((w|Seg(n+1)).len (w|Seg(n+1)))
by A14,A48,A49,A45
.= T2.(w|Seg(n+1))
by A16,A45,A50,A41,A40,A33,A36,A37,A34,AXIOMS:22,TREES_1:45;
end;
A51: for n being Nat holds R[n] from Ind(A31,A32);
w = w|Seg len w by FINSEQ_3:55;
then
A52: T1.w = T2.w by A51,A27;
succ v in U2 by A28;
hence a in union U2 by A52,A27,A29,A30,A23,A25,TARSKI:def 4;
end;
let a be set;
assume a in union U2;
then consider A being set such that
A53: a in A and
A54: A in U2 by TARSKI:def 4;
consider w being Element of dom T2 such that
A55: A = succ w and
A56: len w = n by A54;
w in dom T2-level n by A56,A22;
then consider v being Element of dom T1 such that
A57: w = v and
A58: len v = n by A21,A19;
A59: succ v = {v^<*k*> where k is Nat: k in Card NIC(pi(M,T1.v),T1.v)}
by A14;
A60: succ w = {w^<*k*> where k is Nat: k in Card NIC(pi(M,T2.w),T2.w)}
by A16;
defpred R[Nat] means
$1 <= len w & w|Seg $1 in dom T1 & v|Seg $1 in dom T2 implies
T1.(w|Seg $1) = T2.(w|Seg $1);
A61: R[0]
proof
assume 0 <= len w;
assume w|Seg 0 in dom T1;
assume v|Seg 0 in dom T2;
w|{} = {} by RELAT_1:110;
hence T1.(w|Seg 0) = T2.(w|Seg 0) by A15,A13,FINSEQ_1:4;
end;
A62: for n being Nat st R[n] holds R[n+1]
proof
let n be Nat;
assume that
A63: R[n] and
A64: n+1 <= len w and
A65: w|Seg (n+1) in dom T1 and
A66: v|Seg (n+1) in dom T2;
set t1 = w|Seg n;
A67: n <= n+1 by NAT_1:29;
then
A68: Seg n c= Seg(n+1) by FINSEQ_1:7;
then
w|Seg n = w|Seg(n+1)|Seg n by RELAT_1:103;
then
A69: w|Seg n is_a_prefix_of w|Seg(n+1) by TREES_1:def 1;
v|Seg n = v|Seg(n+1)|Seg n by A68,RELAT_1:103;
then
A70: v|Seg n is_a_prefix_of v|Seg(n+1) by TREES_1:def 1;
A71: (w|Seg(n+1)).len(w|Seg(n+1)) is Nat by ORDINAL2:def 21;
A72: 1 <= n+1 by NAT_1:29;
then
A73: n+1 in dom w by A64,FINSEQ_3:27;
A74: len(w|Seg(n+1)) = n+1 by A64,FINSEQ_1:21;
then len(w|Seg(n+1)) in Seg(n+1) by A72,FINSEQ_1:3;
then w.(n+1) = (w|Seg(n+1)).len(w|Seg(n+1)) by A74,FUNCT_1:72;
then
A75: w|Seg(n+1) = t1^<*(w|Seg(n+1)).len (w|Seg(n+1))*> by A73,FINSEQ_5:11;
reconsider t1 as Element of dom T1 by A69,A65,TREES_1:45;
reconsider t2 = t1 as Element of dom T2 by A57,A70,A66,TREES_1:45;
A76: succ t1 = { t1^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t1),T1.t1)}
by A14;
t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> in succ t1 by A75,A71,A65,TREES_2:14;
then consider k being Nat such that
A77: t1^<*(w|Seg(n+1)).len(w|Seg(n+1))*> = t1^<*k*> and
A78: k in Card NIC(pi(M,T1.t1),T1.t1) by A76;
A79: k = (w|Seg(n+1)).len(w|Seg(n+1)) by A77,FINSEQ_2:20;
A80: (w|Seg(n+1)).len(w|Seg(n+1)) in Card NIC(pi(M,T2.t2),T2.t2)
by A78,A77,A70,A63,A66,A67,A64,AXIOMS:22,TREES_1:45,FINSEQ_2:20;
thus T1.(w|Seg(n+1)) =
(LocSeq NIC(pi(M,T1.t1),T1.t1)).((w|Seg(n+1)).len(w|Seg(n+1)))
by A14,A78,A79,A75
.= T2.(w|Seg(n+1))
by A75,A16,A80,A71,A70,A63,A66,A67,A64,AXIOMS:22,TREES_1:45;
end;
A81: for n being Nat holds R[n] from Ind(A61,A62);
w = w|Seg len w by FINSEQ_3:55;
then
A82: T1.w = T2.w by A81,A57;
succ v in U1 by A58;
hence a in union U1 by A82,A57,A59,A60,A53,A55,TARSKI:def 4;
end;
hence thesis by A20,QC_LANG4:18;
end;
A83: for n being Nat holds P[n] from Ind(A17,A18);
then
A84:dom T1 = dom T2 by Th18;
for p being FinSequence of NAT st p in dom T1 holds T1.p = T2.p
proof
let p be FinSequence of NAT;
assume
A85: p in dom T1;
defpred P[Nat] means
$1 <= len p & p|Seg $1 in dom T1 implies T1.(p|Seg $1) = T2.(p|Seg $1);
A86: P[0]
proof
assume 0 <= len p;
assume p|Seg 0 in dom T1;
p|{} = {} by RELAT_1:110;
hence T1.(p|Seg 0) = T2.(p|Seg 0) by A15,A13,FINSEQ_1:4;
end;
A87: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume that
A88: P[n] and
A89: n+1 <= len p and
A90: p|Seg (n+1) in dom T1;
set t1 = p|Seg n;
A91: n <= n+1 by NAT_1:29;
then Seg n c= Seg(n+1) by FINSEQ_1:7;
then p|Seg n = p|Seg(n+1)|Seg n by RELAT_1:103;
then
A92: p|Seg n is_a_prefix_of p|Seg(n+1) by TREES_1:def 1;
A93: (p|Seg(n+1)).len(p|Seg(n+1)) is Nat by ORDINAL2:def 21;
A94: 1 <= n+1 by NAT_1:29;
then
A95: n+1 in dom p by A89,FINSEQ_3:27;
A96: len(p|Seg(n+1)) = n+1 by A89,FINSEQ_1:21;
then len(p|Seg(n+1)) in Seg(n+1) by A94,FINSEQ_1:3;
then p.(n+1) = (p|Seg(n+1)).len(p|Seg(n+1)) by A96,FUNCT_1:72;
then
A97: p|Seg(n+1) = t1^<*(p|Seg(n+1)).len (p|Seg(n+1))*> by A95,FINSEQ_5:11;
reconsider t1 as Element of dom T1 by A92,A90,TREES_1:45;
reconsider t2 = t1 as Element of dom T2 by A83,Th18;
A98: succ t1 = { t1^<*k*> where k is Nat: k in Card NIC(pi(M,T1.t1),T1.t1)}
by A14;
t1^<*(p|Seg(n+1)).len (p|Seg(n+1))*> in succ t1 by A97,A93,A90,TREES_2:14;
then consider k being Nat such that
A99: t1^<*(p|Seg(n+1)).len (p|Seg(n+1))*> = t1^<*k*> and
A100: k in Card NIC(pi(M,T1.t1),T1.t1) by A98;
A101: k = (p|Seg(n+1)).len (p|Seg(n+1)) by A99,FINSEQ_2:20;
A102: (p|Seg(n+1)).len (p|Seg(n+1)) in Card NIC(pi(M,T2.t2),T2.t2)
by A100,A99,A88,A91,A89,AXIOMS:22,FINSEQ_2:20;
thus T1.(p|Seg (n+1)) =
(LocSeq NIC(pi(M,T1.t1),T1.t1)).((p|Seg(n+1)).len (p|Seg(n+1)))
by A14,A100,A101,A97
.= T2.(p|Seg (n+1)) by A97,A16,A102,A93,A88,A91,A89,AXIOMS:22;
end;
A103: for n being Nat holds P[n] from Ind(A86,A87);
p|Seg len p = p by FINSEQ_3:55;
hence thesis by A103,A85;
end;
hence T1 = T2 by A84,TREES_2:33;
end;
end;
theorem
for S being standard halting realistic
(IC-Ins-separated definite (non empty non void AMI-Struct over N))
holds
ExecTree Stop S = TrivialInfiniteTree --> il.(S,0)
proof
let S be standard halting realistic
(IC-Ins-separated definite (non empty non void AMI-Struct over N));
set D = TrivialInfiniteTree;
set M = Stop S;
set E = ExecTree M;
A1: M = il.(S,0) .--> halt S by AMISTD_2:def 13;
then
A2: dom M = {il.(S,0)} by CQC_LANG:5;
A3: M.il.(S,0) = halt S by A1,CQC_LANG:6;
A4: E.{} = FirstLoc(M) by Def5;
A5: for t being Element of dom E holds Card NIC(halt S,E.t) = {0}
proof
let t be Element of dom E;
NIC(halt S,E.t) = {E.t} by AMISTD_1:15;
hence thesis by CARD_1:50,CARD_2:20,CARD_5:1;
end;
defpred R[set] means E.$1 in dom M;
A6: R[<*>NAT] by A4,Th21;
A7: for f being Element of dom E st R[f]
for a being Nat st f^<*a*> in dom E holds R[f^<*a*>]
proof
let f be Element of dom E such that
A8: R[f];
let a be Nat such that
A9: f^<*a*> in dom E;
A10: Card NIC(halt S,E.f) = {0} by A5;
A11: succ f = { f^<*k*> where k is Nat: k in Card NIC(pi(M,E.f),E.f) }
by Def5;
A12: E.f = il.(S,0) by A8,A2,TARSKI:def 1;
then
A13: locnum (E.f) = 0 by AMISTD_1:def 13;
A14: pi(M,E.f) = M.(E.f) by A8,AMI_5:def 5;
then
A15: 0 in Card NIC(pi(M,E.f),E.f) by A10,A12,A3,TARSKI:def 1;
A16: succ f = { f^<*0*> }
proof
hereby
let s be set;
assume s in succ f;
then consider k being Nat such that
A17: s = f^<*k*> and
A18: k in Card NIC(pi(M,E.f),E.f) by A11;
k = 0 by A3,A18,A12,A10,A14,TARSKI:def 1;
hence s in { f^<*0*> } by A17,TARSKI:def 1;
end;
let s be set;
assume s in { f^<*0*> };
then s = f^<*0*> by TARSKI:def 1;
hence s in succ f by A11,A15;
end;
f^<*a*> in succ f by A9,TREES_2:14;
then
A19: f^<*a*> = f^<*0*> by A16,TARSKI:def 1;
LocNums NIC(halt S,E.f) = {0} by A13,Th29;
then canonical_isomorphism_of
(RelIncl order_type_of RelIncl LocNums NIC(pi(M,E.f),E.f),
RelIncl LocNums NIC(pi(M,E.f),E.f)) = 0 .--> locnum (E.f)
by A12,A3,A14,A13,Th15;
then
A20: canonical_isomorphism_of
(RelIncl order_type_of RelIncl LocNums NIC(pi(M,E.f),E.f),
RelIncl LocNums NIC(pi(M,E.f),E.f)).0 = locnum (E.f) by CQC_LANG:6
.= 0 by A12,AMISTD_1:def 13;
E.(f^<*a*>) = (LocSeq NIC(pi(M,E.f),E.f)).0 by A15,A19,Def5
.= il.(S,0) by A20,A15,Def4;
hence R[f^<*a*>] by A2,TARSKI:def 1;
end;
A21: for f being Element of dom E holds R[f] from InTreeInd(A6,A7);
defpred X[Nat] means dom E-level $1 = D-level $1;
A22: X[0]
proof
thus dom E-level 0 = {{}} by QC_LANG4:17
.= D-level 0 by QC_LANG4:17;
end;
A23: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat;
assume
A24: X[n];
set f0 = n |-> 0;
set f1 = (n+1) |-> 0;
A25: dom E-level (n+1) = {w where w is Element of dom E: len w = n+1}
by TREES_2:def 6;
A26: len f1 = n+1 by FINSEQ_2:69;
dom E-level (n+1) = {f1}
proof
hereby
let a be set;
assume a in dom E-level (n+1);
then consider t1 being Element of dom E such that
A27: a = t1 and
A28: len t1 = n+1 by A25;
reconsider t0 = t1|Seg n as Element of dom E by Th17;
A29: dom E-level n = {w where w is Element of dom E: len w = n}
by TREES_2:def 6;
A30: succ t0 = { t0^<*k*> where k is Nat: k in Card NIC(pi(M,E.t0),E.t0) }
by Def5;
A31: Card NIC(halt S,E.t0) = {0} by A5;
A32: E.t0 in dom M by A21;
then
A33: E.t0 = il.(S,0) by A2,TARSKI:def 1;
A34: pi(M,E.t0) = M.(E.t0) by A32,AMI_5:def 5;
then
A35: 0 in Card NIC(pi(M,E.t0),E.t0) by A31,A33,A3,TARSKI:def 1;
A36: t1.(n+1) is Nat by ORDINAL2:def 21;
A37: dom E-level n = {f0} by A24,Th20;
n <= n+1 by NAT_1:29;
then Seg n c= Seg(n+1) by FINSEQ_1:7;
then Seg n c= dom t1 by A28,FINSEQ_1:def 3;
then dom t0 = Seg n by RELAT_1:91;
then len t0 = n by FINSEQ_1:def 3;
then
A38: t0 in dom E-level n by A29;
t1 = t0^<*t1.(n+1)*> by A28,FINSEQ_3:61;
then
A39: t0^<*t1.(n+1)*> in succ t0 by A36,TREES_2:14;
succ t0 = { t0^<*0*> }
proof
hereby
let s be set;
assume s in succ t0;
then consider k being Nat such that
A40: s = t0^<*k*> and
A41: k in Card NIC(pi(M,E.t0),E.t0) by A30;
k = 0 by A34,A3,A41,A33,A31,TARSKI:def 1;
hence s in { t0^<*0*> } by A40,TARSKI:def 1;
end;
let s be set;
assume s in { t0^<*0*> };
then s = t0^<*0*> by TARSKI:def 1;
hence s in succ t0 by A30,A35;
end;
then
A42: t0^<*t1.(n+1)*> = t0^<*0*> by A39,TARSKI:def 1;
for k being Nat st 1 <= k & k <= len t1 holds t1.k = f1.k
proof
let k be Nat such that
A43: 1 <= k & k <= len t1;
A44: k in Seg(n+1) by A28,A43,FINSEQ_1:3;
now
per cases by A44,FINSEQ_2:8;
suppose
A45: k in Seg n;
hence t1.k = t0.k by FUNCT_1:72
.= f0.k by A38,A37,TARSKI:def 1
.= 0 by A45,FINSEQ_2:70;
suppose k = n+1;
hence t1.k = 0 by A42,FINSEQ_2:20;
end;
hence t1.k = f1.k by A44,FINSEQ_2:70;
end;
then t1 = f1 by A28,A26,FINSEQ_1:18;
hence a in {f1} by A27,TARSKI:def 1;
end;
let a be set;
assume a in {f1};
then
A46: a = f1 by TARSKI:def 1;
defpred P[Nat] means $1 |-> 0 in dom E;
0 |-> 0 = {} by FINSEQ_2:72;
then
A47: P[0] by TREES_1:47;
A48: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then reconsider t = n |-> 0 as Element of dom E;
A49: succ t = { t^<*k*> where k is Nat: k in Card NIC(pi(M,E.t),E.t) }
by Def5;
A50: Card NIC(halt S,E.t) = {0} by A5;
A51: E.t in dom M by A21;
then
A52: E.t = il.(S,0) by A2,TARSKI:def 1;
pi(M,E.t) = M.(E.t) by A51,AMI_5:def 5;
then 0 in Card NIC(pi(M,E.t),E.t) by A50,A52,A3,TARSKI:def 1;
then t^<*0*> in succ t by A49;
then t^<*0*> in dom E;
hence thesis by FINSEQ_2:74;
end;
for n being Nat holds P[n] from Ind(A47,A48);
then f1 is Element of dom E;
hence a in dom E-level (n+1) by A25,A26,A46;
end;
hence thesis by Th20;
end;
for x being Nat holds X[x] from Ind(A22,A23);
then
A53: dom E = D by Th18;
for x being set st x in dom E holds E.x = il.(S,0)
proof
let x be set;
assume x in dom E;
then reconsider x as Element of dom E;
E.x in dom M by A21;
then E.x in {il.(S,0)} by A1,CQC_LANG:5;
hence thesis by TARSKI:def 1;
end;
hence thesis by A53,FUNCOP_1:17;
end;