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;