:: On Defining Functions on Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 12, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, XBOOLE_0, FINSEQ_1, TREES_3, SUBSET_1, RELAT_1,
FUNCT_1, TARSKI, TREES_2, TREES_4, ZFMISC_1, MCART_1, LANG1, STRUCT_0,
TDGROUP, CARD_3, ARYTM_3, NAT_1, XXREAL_0, FINSET_1, TREES_1, TREES_A,
FUNCT_6, PRE_POLY, ORDINAL4, FINSEQ_2, DTCONSTR;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
FINSET_1, XTUPLE_0, MCART_1, CARD_3, DOMAIN_1, LANG1, TREES_1, TREES_2,
FINSEQ_4, TREES_3, TREES_4, FINSEQOP, XXREAL_0, NAT_1, PRE_POLY;
constructors PARTFUN1, BINOP_1, DOMAIN_1, SETWISEO, XXREAL_0, XREAL_0, NAT_1,
CARD_3, FINSEQOP, FINSEQ_4, FINSOP_1, TREES_4, LANG1, RELSET_1, PRE_POLY,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1,
FINSEQ_1, TREES_1, TREES_2, TREES_3, STRUCT_0, LANG1, FINSET_1, CARD_1,
FINSEQ_2, TREES_4, VALUED_0, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FINSEQ_1, XBOOLE_0;
equalities FINSEQ_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_6, MCART_1,
LANG1, FINSEQ_1, FINSEQ_2, CARD_5, TREES_1, TREES_3, TREES_4, CARD_3,
RELSET_1, XBOOLE_0, XBOOLE_1, MEASURE2, XXREAL_0, ORDINAL1, PRE_POLY,
CARD_1;
schemes NAT_1, CQC_SIM1, FINSEQ_1, RELSET_1, FRAENKEL, FUNCT_2, FUNCT_1;
begin :: Preliminaries
deffunc T(set) = 0;
deffunc A(set,set,set) = 0;
theorem Th1: :: This really belongs elsewhere
for D being non empty set, p being FinSequence of FinTrees D holds
p is FinSequence of Trees D
proof
let D be non empty set;
FinTrees D is non empty Subset of Trees D by TREES_3:21;
hence thesis by FINSEQ_2:24;
end;
theorem Th2:
for x,y being set, p being FinSequence of x st y in dom p holds p.y in x
proof
let x,y be set;
let p be FinSequence of x;
assume y in dom p;
then
A1: p.y in rng p by FUNCT_1:def 3;
rng p c= x by FINSEQ_1:def 4;
hence thesis by A1;
end;
registration
let D be non empty set, T be DTree-set of D;
cluster -> DTree-yielding for FinSequence of T;
coherence;
end;
definition
let D be non empty set;
let F be non empty DTree-set of D;
let Tset be non empty Subset of F;
redefine mode Element of Tset -> Element of F; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of Tset;
thus thesis;
end;
end;
definition
let D be non empty set, T be DTree-set of D;
let p be FinSequence of T;
redefine func roots p -> FinSequence of D; :: redefines roots (TREES_3, definition)
coherence
proof
let x be object;
assume x in rng roots p;
then consider k being object such that
A1: k in dom roots p and
A2: x = (roots p).k by FUNCT_1:def 3;
reconsider k as Element of NAT by A1;
A3: dom roots p = dom p by TREES_3:def 18;
then consider t being DecoratedTree such that
A4: t = p.k and
A5: (roots p).k = t.{} by A1,TREES_3:def 18;
reconsider t as DecoratedTree of D by A1,A3,A4,Th2,TREES_3:def 6;
reconsider r = {} as Node of t by TREES_1:22;
t.r in D;
hence thesis by A2,A5;
end;
end;
Lm1: dom roots {} = dom {} by TREES_3:def 18
.= {};
theorem Th3:
roots {} = {} by Lm1;
theorem Th4:
for T being DecoratedTree holds roots <*T*> = <*T.{}*>
proof
let T be DecoratedTree;
A1: dom <*T*> = Seg 1 by FINSEQ_1:def 8;
A2: dom <*T.{}*> = Seg 1 by FINSEQ_1:def 8;
A3: <*T*>.1 = T;
A4: <*T.{}*>.1 = T.{};
now
let i be Element of NAT;
assume
A5: i in dom <*T*>;
take t = T;
thus t = <*T*>.i & <*T.{}*>.i = t.{} by A1,A3,A4,A5,FINSEQ_1:2,TARSKI:def 1
;
end;
hence thesis by A1,A2,TREES_3:def 18;
end;
theorem Th5:
for D being non empty set, F being (Subset of FinTrees D),
p being FinSequence of F st len roots p = 1
ex x being Element of FinTrees D st p = <*x*> & x in F
proof
let D be non empty set, F be (Subset of FinTrees D), p be FinSequence of F;
assume len roots p = 1;
then
A1: dom roots p = Seg 1 by FINSEQ_1:def 3;
A2: dom p = dom roots p by TREES_3:def 18;
then
A3: 1 in dom p by A1;
then reconsider x = p.1 as Element of FinTrees D by Th2;
take x;
thus thesis by A1,A2,A3,Th2,FINSEQ_1:def 8;
end;
theorem
for T1, T2 being DecoratedTree holds roots <*T1, T2*> = <*T1.{}, T2.{}*>
proof
let T1, T2 be DecoratedTree;
A1: len <*T1, T2*> = 2 by FINSEQ_1:44;
A2: len <*T1.{}, T2.{}*> = 2 by FINSEQ_1:44;
A7: dom <*T1, T2*> = Seg 2 by A1,FINSEQ_1:def 3;
A8: dom <*T1.{}, T2.{}*> = Seg 2 by A2,FINSEQ_1:def 3;
now
let i be Element of NAT;
assume i in dom <*T1, T2*>;
then i in Seg 2 by A1,FINSEQ_1:def 3;
then i = 1 or i = 2 by FINSEQ_1:2,TARSKI:def 2;
hence ex t being DecoratedTree st
t = <*T1, T2*>.i & <*T1.{}, T2.{}*>.i = t.{};
end;
hence thesis by A7,A8,TREES_3:def 18;
end;
definition
let X, Y be set, f be FinSequence of [:X, Y:];
redefine func pr1 f -> FinSequence of X; :: redefines pr1 (MCART_1, definition)
coherence
proof
A1: dom pr1 f = dom f by MCART_1:def 12;
dom f = Seg len f by FINSEQ_1:def 3;
then reconsider p = pr1 f as FinSequence by A1,FINSEQ_1:def 2;
rng p c= X
proof
let x be object;
assume x in rng p;
then consider i being object such that
A2: i in dom p and
A3: x = p.i by FUNCT_1:def 3;
A4: f.i in [:X, Y:] by A1,A2,Th2;
x = (f.i)`1 by A1,A2,A3,MCART_1:def 12;
hence thesis by A4,MCART_1:10;
end;
hence thesis by FINSEQ_1:def 4;
end;
redefine func pr2 f -> FinSequence of Y; :: redefines pr2 (MCART_1, definition)
coherence
proof
A5: dom pr2 f = dom f by MCART_1:def 13;
dom f = Seg len f by FINSEQ_1:def 3;
then reconsider p = pr2 f as FinSequence by A5,FINSEQ_1:def 2;
rng p c= Y
proof
let x be object;
assume x in rng p;
then consider i being object such that
A6: i in dom p and
A7: x = p.i by FUNCT_1:def 3;
A8: f.i in [:X, Y:] by A5,A6,Th2;
x = (f.i)`2 by A5,A6,A7,MCART_1:def 13;
hence thesis by A8,MCART_1:10;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th7:
pr1 {} = {} & pr2 {} = {}
proof
set r = <*>[:{}, {}:];
dom pr1 r = dom {}
.= {};
hence pr1 {} = {};
dom pr2 r = dom {}
.= {};
hence thesis;
end;
begin
registration
let A be non empty set, R be Relation of A,A*;
cluster DTConstrStr(#A,R#) -> non empty;
coherence;
end;
scheme DTConstrStrEx { S() -> non empty set, P[object,object] }:
ex G be strict non empty DTConstrStr st the carrier of G = S() &
for x being Symbol of G, p being FinSequence of the carrier of G
holds x ==> p iff P[x, p]
proof
consider PR being Relation of S(), S()* such that
A1: for x, y being object
holds [x,y] in PR iff x in S() & y in S()* & P[x, y] from RELSET_1:sch 1;
take DT = DTConstrStr (# S(), PR #);
thus the carrier of DT = S();
let x be Symbol of DT, p be FinSequence of the carrier of DT;
hereby
assume x ==> p;
then [x, p] in the Rules of DT by LANG1:def 1;
hence P[x, p] by A1;
end;
assume
A2: P[x, p];
p in (the carrier of DT)* by FINSEQ_1:def 11;
then [x, p] in PR by A1,A2;
hence thesis by LANG1:def 1;
end;
scheme DTConstrStrUniq { S() -> non empty set, P[set, set] }:
for G1, G2 being strict non empty DTConstrStr st (the carrier of G1 = S() &
for x being Symbol of G1, p being FinSequence of the carrier of G1
holds x ==> p iff P[x, p]) & (the carrier of G2 = S() &
for x being Symbol of G2, p being FinSequence of the carrier of G2
holds x ==> p iff P[x, p]) holds G1 = G2
proof
let G1, G2 be strict non empty DTConstrStr such that
A1: the carrier of G1 = S() and
A2: for x being Symbol of G1, p being FinSequence of the carrier of G1
holds x ==> p iff P[x, p] and
A3: the carrier of G2 = S() and
A4: for x being Symbol of G2, p being FinSequence of the carrier of G2
holds x ==> p iff P[x, p];
now
let x, y be object;
hereby
assume
A5: [x, y] in the Rules of G1;
then
A6: y in (the carrier of G1)* by ZFMISC_1:87;
reconsider x1 = x as Symbol of G1 by A5,ZFMISC_1:87;
reconsider y1 = y as FinSequence of the carrier of G1 by A6,FINSEQ_2:def 3;
A7: x1 ==> y1 iff P[x1, y1] by A2;
reconsider x2 = x as Symbol of G2 by A1,A3,A5,ZFMISC_1:87;
reconsider y2 = y as FinSequence of the carrier of G2 by A1,A3,A6,
FINSEQ_2:def 3;
x2 ==> y2 by A4,A5,A7,LANG1:def 1;
hence [x, y] in the Rules of G2 by LANG1:def 1;
end;
assume
A8: [x, y] in the Rules of G2;
then
A9: y in (the carrier of G2)* by ZFMISC_1:87;
reconsider x2 = x as Symbol of G2 by A8,ZFMISC_1:87;
reconsider y2 = y as FinSequence of the carrier of G2 by A9,FINSEQ_2:def 3;
A10: x2 ==> y2 iff P[x2, y2] by A4;
reconsider x1 = x as Symbol of G1 by A1,A3,A8,ZFMISC_1:87;
reconsider y1 = y as FinSequence of the carrier of G1 by A1,A3,A9,
FINSEQ_2:def 3;
x1 ==> y1 by A2,A8,A10,LANG1:def 1;
hence [x, y] in the Rules of G1 by LANG1:def 1;
end;
hence thesis by A1,A3,RELAT_1:def 2;
end;
theorem
for G being non empty DTConstrStr holds Terminals G misses NonTerminals G
proof
let G be non empty DTConstrStr;
A1: Terminals G = { t where t is Symbol of G :
not ex tnt being FinSequence st t ==> tnt } by LANG1:def 2;
A2: NonTerminals G = { t where t is Symbol of G :
ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
assume not thesis;
then consider x being object such that
A3: x in Terminals G and
A4: x in NonTerminals G by XBOOLE_0:3;
A5: ex t being Symbol of G st x = t & not ex tnt being FinSequence st t ==>
tnt by A1,A3;
ex t being Symbol of G st x = t & ex tnt being FinSequence st t ==> tnt
by A2,A4;
hence contradiction by A5;
end;
scheme DTCMin { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
ex X being Subset of FinTrees [:the carrier of G(), D():] st X = Union f() &
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G(),
p being FinSequence of X st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
for F being Subset of FinTrees [:the carrier of G(), D():] st
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G(),
p being FinSequence of F st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F) holds X c= F
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
set f = f();
set G = G();
set D = D();
deffunc
NTV(Symbol of G, FinSequence) = NTermVal($1, pr1 roots $2, pr2 roots $2);
Union f c= FinTrees [:the carrier of G, D:]
proof
let u be object;
assume u in Union f;
then
A4: ex k being object st ( k in NAT)&( u in f.k) by A1,CARD_5:2;
defpred P[Nat] means for u being set st u in f.$1 holds
u in FinTrees [:the carrier of G, D:];
A5: P[0]
proof
let u be set;
assume u in f.0;
then ex t being Symbol of G, d being Element of D st u = root-tree [t,d]
& (t in Terminals G() & d = TermVal(t) or
t ==> {} & d = NTermVal(t, {}, {})) by A2;
hence thesis;
end;
A6: now
let n be Nat such that
A7: P[n];
thus P[n+1]
proof
let u be set;
assume u in f.(n+1);
then u in f.n \/ { [o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.n)*:
ex q being FinSequence of FinTrees[:the carrier of G, D:] st
p = q & o ==> pr1 roots q } by A3;
then
A8: u in f.n or u in { [o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.n)*:
ex q being FinSequence of FinTrees[:the carrier of G, D:] st
p = q & o ==> pr1 roots q } by XBOOLE_0:def 3;
assume
A9: not u in FinTrees [:the carrier of G, D:];
then consider o being Symbol of G, p being Element of (f.n)* such that
A10: u = [o, NTV(o, p)]-tree p and
A11: ex q being FinSequence of FinTrees [:the carrier of G, D:] st p = q
& o ==> pr1 roots q
by A7,A8;
reconsider p as FinSequence of FinTrees [:the carrier of G, D:] by A11;
u = [o, NTV(o, p)]-tree p by A10;
hence contradiction by A9;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A5,A6);
hence thesis by A4;
end;
then reconsider X = Union f as Subset of FinTrees [:the carrier of G, D:];
take X;
thus X = Union f;
hereby
let d be Symbol of G;
assume d in Terminals G;
then root-tree [d, TermVal(d)] in f.0 by A2;
hence root-tree [d, TermVal(d)] in X by A1,CARD_5:2;
end;
hereby
let o be Symbol of G, p be FinSequence of X such that
A12: o ==> pr1 roots p;
set s = pr1 roots p, v = pr2 roots p;
A13: dom p = Seg len p by FINSEQ_1:def 3;
defpred P[set,set] means p.$1 in f.($2);
A14: for x being Nat st x in Seg len p ex n being Element of NAT st P[x,n]
proof
let x be Nat;
assume x in Seg len p;
then
A15: p.x in rng p by A13,FUNCT_1:def 3;
rng p c= X by FINSEQ_1:def 4;
then ex n being object st n in NAT & p.x in f.n by A1,A15,CARD_5:2;
hence thesis;
end;
consider pn being FinSequence of NAT such that
A16: dom pn = Seg len p & for k being Nat st k in Seg len p holds P[k,pn.k]
from FINSEQ_1:sch 5(A14);
A17: now
defpred P[Element of NAT,Element of NAT] means $1 >= $2;
assume rng pn <> {};
then
A18: rng pn is finite & rng pn <> {} & rng pn c= NAT by FINSEQ_1:def 4;
A19: for x, y being Element of NAT holds P[x,y] or P[y,x];
A20: for x, y, z being Element of NAT st P[x,y] & P[y,z] holds P[x,z]
by XXREAL_0:2;
consider n being Element of NAT such that
A21: n in rng pn & for y being Element of NAT st y in rng pn holds P[n,y]
from CQC_SIM1:sch 4 ( A18, A19, A20 );
take n;
thus rng p c= f.n
proof
let t be object;
assume t in rng p;
then consider k being object such that
A22: k in dom p and
A23: t = p.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A22;
A24: pn.k in rng pn by A13,A16,A22,FUNCT_1:def 3;
then reconsider pnk = pn.k as Element of NAT by A18;
consider s being Nat such that
A25: n = pnk + s by A21,A24,NAT_1:10;
deffunc H(set,set) =
{ [o1, NTermVal(o1, pr1 roots p1, pr2 roots p1)]-tree p1
where o1 is Symbol of G(), p1 is Element of (f.$1)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p1 = q & o1 ==> pr1 roots q };
for n being Nat holds f.n c= f.(n+1)
proof
let n be Nat;
f.(n+1) = f.n \/ H(n, f.n) by A3;
hence thesis by XBOOLE_1:7;
end;
then
A26: f.pnk c= f.n by A25,MEASURE2:18,NAT_1:11;
t in f.(pn.k) by A13,A16,A22,A23;
hence thesis by A26;
end;
end;
now
assume rng pn = {};
then pn = {};
then p = {} by A16;
then rng p = {};
hence rng p c= f.0;
end;
then consider n being Element of NAT such that
A27: rng p c= f.n by A17;
A28: X = union rng f by CARD_3:def 4;
f.n in rng f by A1,FUNCT_1:def 3;
then f.n c= X by A28,ZFMISC_1:74;
then reconsider fn = f.n as Subset of FinTrees [:the carrier of G, D:] by
XBOOLE_1:1;
reconsider q = p as FinSequence of fn by A27,FINSEQ_1:def 4;
reconsider q9 = q as Element of (fn)* by FINSEQ_1:def 11;
[o, NTermVal(o, s, v)]-tree q9 in { [oo, NTV(oo, pp)]-tree pp
where oo is Symbol of G, pp is Element of (fn)* :
ex q being FinSequence of FinTrees [:the carrier of G, D:] st
pp = q & oo ==> pr1 roots q } by A12;
then [o, NTermVal(o, s, v)]-tree q9 in f.n \/ { [oo, NTV(oo, pp)]-tree pp
where oo is Symbol of G, pp is Element of (fn)* :
ex q being FinSequence of FinTrees [:the carrier of G, D:] st
pp = q & oo ==> pr1 roots q } by XBOOLE_0:def 3;
then [o, NTermVal(o, s, v)]-tree q9 in f.(n+1) by A3;
hence [o, NTermVal(o, s, v)]-tree p in X by A1,CARD_5:2;
end;
let F be Subset of FinTrees [:the carrier of G, D:] such that
A29: for d being Symbol of G st d in Terminals G holds root-tree [d,
TermVal(d)] in F and
A30: for o being Symbol of G, p being FinSequence of F st o ==> pr1
roots p holds [o, NTV(o, p)]-tree p in F;
defpred P[Nat] means f.$1 c= F;
A31: P[0]
proof
let x be object;
reconsider p = <*>F as FinSequence of F;
assume x in f.0;
then consider t being Symbol of G, d being Element of D such that
A32: x = root-tree [t, d] and
A33: t in Terminals G() & d = TermVal(t) or t ==> pr1 roots p & d = NTV (t, p)
by A2,Th3,Th7;
[t, d]-tree p = root-tree [t, d] by TREES_4:20;
hence thesis by A29,A30,A32,A33;
end;
A34: now
let n be Nat such that
A35: P[n];
thus P[n+1]
proof
let x be object;
assume that
A36: x in f.(n+1) and
A37: not x in F;
x in f.n \/ {[oo, NTV(oo, pp)]-tree pp
where oo is Symbol of G, pp is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G, D:] st
pp = q & oo ==> pr1 roots q } by A3,A36;
then x in f.n or x in {[oo, NTV(oo, pp)]-tree pp
where oo is Symbol of G, pp is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G, D:] st
pp = q & oo ==> pr1 roots q } by XBOOLE_0:def 3;
then consider o being Symbol of G, p being Element of (f.n)* such that
A38: x = [o, NTV(o, p)]-tree p and
A39: ex q being FinSequence of FinTrees [:the carrier of G, D:] st p = q
& o ==> pr1 roots q
by A35,A37;
rng p c= f.n by FINSEQ_1:def 4;
then rng p c= F by A35,XBOOLE_1:1;
then reconsider p as FinSequence of F by FINSEQ_1:def 4;
o ==> pr1 roots p by A39;
hence contradiction by A30,A37,A38;
end;
end;
A40: for n being Nat holds P[n] from NAT_1:sch 2(A31, A34);
thus X c= F
proof
let x be object;
assume x in X;
then consider n being object such that
A41: n in NAT and
A42: x in f.n by A1,CARD_5:2;
f.n c= F by A40,A41;
hence thesis by A42;
end;
end;
scheme DTCSymbols { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
ex X1 being Subset of FinTrees(the carrier of G()) st
X1 = { t`1 where t is Element of FinTrees [:(the carrier of G()), D():] :
t in Union f() } &
(for d being Symbol of G() st d in Terminals G() holds root-tree d in X1) &
(for o being Symbol of G(), p being FinSequence of X1 st o ==> roots p
holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G() st
(for d being Symbol of G() st d in Terminals G() holds root-tree d in F) &
(for o being Symbol of G(), p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds X1 c= F
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
set f = f();
set G = G();
set D = D();
set S = the carrier of G;
set SxD = [:S, D:];
deffunc
NTV(Symbol of G, FinSequence) =NTermVal($1, pr1 roots $2, pr2 roots $2);
A4: f
().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or
t ==> {} & d = NTermVal(t, {}, {}) } by A2;
A5: for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q } by A3;
consider X being Subset of FinTrees [:the carrier of G, D:] such that
A6: X = Union f & (for d being Symbol of G st d in Terminals G
holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G,
p being FinSequence of X st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
for F being Subset of FinTrees [:the carrier of G, D:] st
(for d being Symbol of G st d in Terminals G
holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G,
p being FinSequence of F st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
holds X c= F from DTCMin (A1, A4, A5);
set X9 = { t`1 where t is Element of FinTrees [:the carrier of G,D:]:
t in Union f };
X9 c= FinTrees(the carrier of G)
proof
let x be object;
assume x in X9;
then consider tt being Element of FinTrees [:the carrier of G,D:] such that
A7: x = tt`1 and tt in Union f;
A8: tt`1 = pr1(the carrier of G, D) * tt by TREES_3:def 12;
A9: rng tt c= [:the carrier of G, D:] by RELAT_1:def 19;
dom pr1(the carrier of G, D) = [:the carrier of G, D:] by FUNCT_2:def 1;
then dom tt`1 = dom tt by A8,A9,RELAT_1:27;
hence thesis by A7,TREES_3:def 8;
end;
then reconsider X9 as Subset of FinTrees(the carrier of G());
take X1= X9;
thus X1 = { t`1 where t is Element of FinTrees [:the carrier of G,D:]:
t in Union f };
hereby
let t be Symbol of G();
assume
A10: t in Terminals G();
A11: (root-tree [t, TermVal(t)])`1 = root-tree t by TREES_4:25;
root-tree [t, TermVal(t)] in Union f by A6,A10;
hence root-tree t in X1 by A11;
end;
hereby
let nt be Symbol of G(), ts be FinSequence of X1;
assume
A12: nt ==> roots ts;
A13: dom ts = Seg len ts by FINSEQ_1:def 3;
defpred P[set,set] means
ex dt being DecoratedTree of [:the carrier of G(), D():] st
dt = $2 & dt`1 = ts.$1 & dt in Union f;
A14: for k being Nat st k in Seg len ts
ex x being Element of FinTrees [:the carrier of G, D:] st P[k,x]
proof
let k be Nat;
assume k in Seg len ts;
then
A15: ts.k in rng ts by A13,FUNCT_1:def 3;
rng ts c= X1 by FINSEQ_1:def 4;
then ts.k in X1 by A15;
then ex x being Element of FinTrees [:the carrier of G, D:] st
ts.k = x`1 & x in Union f;
hence thesis;
end;
consider dts being FinSequence of FinTrees [:the carrier of G, D:]
such that
A16: dom dts = Seg len ts and
A17: for k being Nat st k in Seg len ts holds P[k,dts.k]
from FINSEQ_1:sch 5(A14);
rng dts c= Union f
proof
let x be object;
assume x in rng dts;
then consider k being object such that
A18: k in dom ts and
A19: x = dts.k by A13,A16,FUNCT_1:def 3;
reconsider k as Element of NAT by A18;
ex dt being DecoratedTree of [:the carrier of G(), D():]
st dt = x & dt`1 = ts.k & dt in Union f by A13,A17,A18,A19;
hence thesis;
end;
then reconsider dts as FinSequence of X by A6,FINSEQ_1:def 4;
A20: dom roots ts = dom ts by TREES_3:def 18;
A21: dom pr1 roots dts = dom roots dts by MCART_1:def 12;
then
A22: dom pr1 roots dts = dom ts by A13,A16,TREES_3:def 18;
now
let k be Nat;
assume
A23: k in dom ts;
then consider dt being DecoratedTree of [:the carrier of G(), D():]
such that
A24: dt = dts.k and
A25: dt`1 = ts.k and dt in Union f by A13,A17;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st T = ts.k & (roots ts).k = T.{}
by A23,TREES_3:def 18;
then
A26: (roots ts).k = (dt.r)`1 by A25,TREES_3:39;
ex T being DecoratedTree st T = dts.k & (roots dts).k = T.{}
by A13,A16,A23,TREES_3:def 18;
hence (roots ts).k = (pr1 roots dts).k
by A21,A22,A23,A24,A26,MCART_1:def 12;
end;
then roots ts = pr1 roots dts by A20,A22,FINSEQ_1:13;
then
A27: [nt, NTV(nt, dts)]-tree dts in X by A6,A12;
A28: rng dts c= FinTrees [:the carrier of G(), D():] by FINSEQ_1:def 4;
FinTrees [:the carrier of G(),D():] c= Trees [:the carrier of G(), D() :]
by TREES_3:21;
then rng dts c= Trees [:the carrier of G(), D():] by A28;
then reconsider dts9 = dts as FinSequence of Trees [:the carrier of G(),D()
:] by FINSEQ_1:def 4;
A29: rng ts c= FinTrees the carrier of G() by FINSEQ_1:def 4;
FinTrees the carrier of G() c= Trees the carrier of G() by TREES_3:21;
then rng ts c= Trees the carrier of G() by A29;
then reconsider ts9 = ts as FinSequence of Trees the carrier of G()
by FINSEQ_1:def 4;
now
let i be Nat;
assume i in dom dts;
then
A30: ex dt being DecoratedTree of [:the carrier of G, D:] st ( dt
= dts.i)&( dt`1 = ts.i)&( dt in Union f) by A16,A17;
let T be DecoratedTree of [:the carrier of G(), D():];
assume T = dts.i;
hence ts.i = T`1 by A30;
end;
then ([nt, NTV(nt, dts)]-tree dts9)`1 = nt-tree ts9 by A13,A16,TREES_4:27;
hence nt-tree ts in X1 by A6,A27;
end;
let F be Subset of FinTrees the carrier of G;
assume that
A31: for d being Symbol of G st d in Terminals G holds root-tree d in F and
A32: for o being Symbol of G, p being FinSequence of F st o ==> roots p
holds o-tree p in F;
thus X1 c= F
proof
let x be object;
assume x in X1;
then consider tt being Element of FinTrees [:the carrier of G, D:] such that
A33: x = tt`1 and
A34: tt in Union f;
set FF = { dt where dt is Element of FinTrees SxD : dt`1 in F };
FF c= FinTrees SxD
proof
let x be object;
assume x in FF;
then ex dt being Element of FinTrees SxD st x = dt & dt`1 in F;
hence thesis;
end;
then reconsider FF as Subset of FinTrees SxD;
A35: now
let d be Symbol of G;
assume d in Terminals G;
then
A36: root-tree d in F by A31;
(root-tree [d, TermVal(d)])`1 = root-tree d by TREES_4:25;
hence root-tree [d, TermVal(d)] in FF by A36;
end;
now
let o be Symbol of G, p be FinSequence of FF;
assume
A37: o ==> pr1 roots p;
consider p1 being FinSequence of FinTrees S such that
A38: dom p1 = dom p and
A39: for i being Nat st i in dom p
ex T being Element of FinTrees SxD st T = p.i & p1.i = T`1 and
A40: ([o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p)`1 = o-tree p1
by TREES_4:31;
rng p1 c= F
proof
let x be object;
assume x in rng p1;
then consider k being object such that
A41: k in dom p1 and
A42: x = p1.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A41;
A43: p.k in rng p by A38,A41,FUNCT_1:def 3;
A44: ex dt being Element of FinTrees SxD st ( dt = p.k)&( x = dt
`1) by A38,A39,A41,A42;
rng p c= FF by FINSEQ_1:def 4;
then p.k in FF by A43;
then ex dt being Element of FinTrees SxD st p.k = dt & dt`1 in F;
hence thesis by A44;
end;
then reconsider p1 as FinSequence of F by FINSEQ_1:def 4;
A45: dom roots p1 = dom p1 by TREES_3:def 18;
A46: dom pr1 roots p = dom roots p by MCART_1:def 12;
then
A47: dom pr1 roots p = dom p1 by A38,TREES_3:def 18;
now
let k be Nat;
assume
A48: k in dom p1;
then
A49: p.k in rng p by A38,FUNCT_1:def 3;
A50: ex dt being Element of FinTrees SxD st ( dt = p.k)&( p1.k =
dt`1) by A38,A39,A48;
rng p c= FF by FINSEQ_1:def 4;
then p.k in FF by A49;
then consider dt being Element of FinTrees SxD such that
A51: p.k = dt and dt`1 in F;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st T = p1.k & (roots p1).k = T.{}
by A48,TREES_3:def 18;
then
A52: (roots p1).k = (dt.r)`1 by A50,A51,TREES_3:39;
ex T being DecoratedTree st T = p.k & (roots p).k = T.{}
by A38,A48,TREES_3:def 18;
hence (roots p1).k = (pr1 roots p).k
by A46,A47,A48,A51,A52,MCART_1:def 12;
end;
then pr1 roots p = roots p1 by A45,A47,FINSEQ_1:13;
then ([o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p)`1 in F
by A32,A37,A40;
hence [o, NTV(o, p)]-tree p in FF;
end;
then X c= FF by A6,A35;
then tt in FF by A6,A34;
then ex dt being Element of FinTrees SxD st tt = dt & dt`1 in F;
hence thesis by A33;
end;
end;
scheme DTCHeight { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
for n being Nat, dt being Element of FinTrees [:the carrier of G(), D():]
st dt in Union f() holds dt in f().n iff height dom dt <= n
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
set f = f();
set G = G();
set D = D();
set SxD = [:the carrier of G, D:];
deffunc
NTV(Symbol of G, FinSequence) =NTermVal($1, pr1 roots $2, pr2 roots $2);
defpred R[Nat] means
for dt being Element of FinTrees SxD st dt in Union f
holds dt in f.$1 iff height dom dt <= $1;
A4: R[0]
proof
let dt be Element of FinTrees SxD;
assume
A5: dt in Union f;
hereby
assume dt in f.0;
then ex t being Symbol of G, d being Element of D st dt= root-tree [t,d]
& (t in Terminals G() & d = TermVal(t) or
t ==> {} & d = NTermVal(t, {}, {})) by A2;
hence height dom dt <= 0 by TREES_1:42,TREES_4:3;
end;
assume height dom dt <= 0;
then
A6: height dom dt = 0;
defpred P[Nat] means not dt in f.$1;
assume
A7: P[0];
A8: now
let n be Nat;
assume
A9: P[n];
thus P[n+1]
proof
assume dt in f.(n+1);
then dt in f.n \/ { [o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st p=q & o ==> pr1 roots q}
by A3;
then dt in f.n or dt in {[o,NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st p=q & o ==> pr1 roots q}
by XBOOLE_0:def 3;
then consider o being Symbol of G, p being Element of (f.n)* such that
A10: dt = [o, NTV(o, p)]-tree p and
A11: ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q
by A9;
A12: dt = root-tree (dt.{}) by A6,TREES_1:43,TREES_4:5;
then
A13: p = {} by A10,A11,TREES_4:17;
then dt = root-tree [o, NTermVal(o,{},{})]
by A10,A12,Th3,Th7,TREES_4:def 4;
hence contradiction by A2,A7,A11,A13,Th3,Th7;
end;
end;
A14: for n being Nat holds P[n] from NAT_1:sch 2(A7, A8);
ex n being object st n in NAT & dt in f.n by A1,A5,CARD_5:2;
hence contradiction by A14;
end;
A15: now
let n be Nat;
assume
A16: R[n];
thus R[n+1]
proof
let dt be Element of FinTrees SxD;
assume
A17: dt in Union f;
hereby
assume dt in f.(n+1);
then dt in f.n \/ {[o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st
p = q & o ==> pr1 roots q } by A3;
then
A18: dt in f.n or dt in {[o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st
p = q & o ==> pr1 roots q } by XBOOLE_0:def 3;
per cases;
suppose dt in f.n;
then
A19: height dom dt <= n by A16,A17;
n <= n+1 by NAT_1:11;
hence height dom dt <= n+1 by A19,XXREAL_0:2;
end;
suppose not dt in f.n;
then consider o being Symbol of G, p being Element of (f.n)* such that
A20: dt = [o, NTV(o, p)]-tree p and
A21: ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q
by A18;
reconsider p as FinSequence of FinTrees SxD by A21;
A22: dom dt = tree(doms p) by A20,TREES_4:10;
now
let t be finite Tree;
assume t in rng doms p;
then consider k being object such that
A23: k in dom doms p and
A24: t = (doms p).k by FUNCT_1:def 3;
A25: k in dom p by A23,TREES_3:37;
then
A26: p.k in rng p by FUNCT_1:def 3;
rng p c=FinTrees SxD by FINSEQ_1:def 4;
then reconsider pk = p.k as Element of FinTrees SxD by A26;
A27: n in NAT by ORDINAL1:def 12;
A28: rng p c= f.n by FINSEQ_1:def 4;
A29: t = dom pk by A24,A25,FUNCT_6:22;
pk in Union f by A1,A26,A28,CARD_5:2,A27;
hence height t <= n by A16,A26,A28,A29;
end;
hence height dom dt <= n+1 by A22,TREES_3:77;
end;
end;
assume
A30: height dom dt <= n+1;
defpred P[Nat] means dt in f.$1;
ex k being object st k in NAT & dt in f.k by A1,A17,CARD_5:2;
then
A31: ex k being Nat st P[k];
consider mk being Nat such that
A32: P[mk] & for kk being Nat st P[kk] holds mk <= kk from NAT_1:sch 5(A31);
deffunc F(set,set) = { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f.$1)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q };
A33: for n being Nat holds f.n c= f.(n+1)
proof
let n be Nat;
f.(n+1) = f.n \/ F(n, f.n) by A3;
hence thesis by XBOOLE_1:7;
end;
per cases by NAT_1:6;
suppose mk = 0;
then f.mk c= f.(0+(n+1)) by A33,MEASURE2:18;
hence thesis by A32;
end;
suppose ex k being Nat st mk = k+1;
then consider k being Nat such that
A34: mk = k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
A35: k < k+1 by NAT_1:13;
f.mk = f.k \/ {[o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.k)* :
ex q being FinSequence of FinTrees SxD st
p = q & o ==> pr1 roots q } by A3,A34;
then dt in f.k or dt in {[o, NTV(o, p)]-tree p
where o is Symbol of G, p is Element of (f.k)* :
ex q being FinSequence of FinTrees SxD st p = q & o ==>
pr1 roots q } by A32,XBOOLE_0:def 3;
then consider o being Symbol of G, p being Element of (f.k)* such that
A36: dt = [o, NTV(o, p)]-tree p and
A37: ex q being FinSequence of FinTrees SxD st p = q & o ==> pr1 roots q
by A32,A34,A35;
reconsider p as FinSequence of FinTrees SxD by A37;
A38: dom dt = tree(doms p) by A36,TREES_4:10;
rng p c= f.n
proof
let x be object;
assume x in rng p;
then consider k9 being object such that
A39: k9 in dom p and
A40: x = p.k9 by FUNCT_1:def 3;
A41: x in rng p by A39,A40,FUNCT_1:def 3;
rng p c= FinTrees SxD by FINSEQ_1:def 4;
then reconsider t = x as Element of FinTrees SxD by A41;
A42: k9 in dom doms p by A39,A40,FUNCT_6:22;
dom t = (doms p).k9 by A39,A40,FUNCT_6:22;
then dom t in rng doms p by A42,FUNCT_1:def 3;
then height dom t < n+1 by A30,A38,TREES_3:78,XXREAL_0:2;
then
A43: height dom t <= n by NAT_1:13;
A44: rng p c= f.k by FINSEQ_1:def 4;
t in rng p by A39,A40,FUNCT_1:def 3;
then t in Union f by A1,A44,CARD_5:2;
hence thesis by A16,A43;
end;
then p is FinSequence of f.n by FINSEQ_1:def 4;
then reconsider p as Element of (f.n)* by FINSEQ_1:def 11;
[o, NTV(o, p)]-tree p in {[oo, NTV(oo, pp)]-tree pp
where oo is Symbol of G, pp is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st
pp = q & oo ==> pr1 roots q } by A37;
then dt in f.n \/ {[oo, NTV(oo, pp)]-tree pp
where oo is Symbol of G, pp is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st
pp = q & oo ==> pr1 roots q } by A36,XBOOLE_0:def 3;
hence thesis by A3;
end;
end;
end;
thus for n being Nat holds R[n] from NAT_1:sch 2(A4, A15);
end;
scheme DTCUniq { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
for dt1, dt2 being DecoratedTree of [:(the carrier of G()), D():]
st dt1 in Union f() & dt2 in Union f() & dt1`1 = dt2`1 holds dt1 = dt2
provided
A1: dom f() = NAT and
A2: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q }
proof
set f = f();
set G = G();
set D = D();
set S = the carrier of G;
set SxD = [:S, D:];
deffunc
NTV(Symbol of G, FinSequence) =NTermVal($1, pr1 roots $2, pr2 roots $2);
A4: f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or
t ==> {} & d = NTermVal(t, {}, {}) } by A2;
A5: for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q } by A3;
defpred R[Nat] means for dt1, dt2 being DecoratedTree of SxD
st dt1 in f.$1 & dt2 in f.$1 & dt1`1 = dt2`1 holds dt1 = dt2;
A6: R[0]
proof
let dt1,dt2 be DecoratedTree of SxD;
assume that
A7: dt1 in f.0 and
A8: dt2 in f.0 and
A9: dt1`1 = dt2`1;
consider t1 being Symbol of G, d1 being Element of D such that
A10: dt1= root-tree [t1, d1] and
A11: t1 in Terminals G & d1 = TermVal(t1) or t1 ==> {} & d1 = NTermVal(
t1, {}, {})
by A2,A7;
consider t2 being Symbol of G, d2 being Element of D such that
A12: dt2= root-tree [t2, d2] and
A13: t2 in Terminals G & d2 = TermVal(t2) or t2 ==> {} & d2 = NTermVal(
t2, {}, {})
by A2,A8;
A14: root-tree t1 = dt1`1 by A10,TREES_4:25;
root-tree t2 = dt2`1 by A12,TREES_4:25;
then
A15: t1 = t2 by A9,A14,TREES_4:4;
now
let t be Symbol of G;
assume t ==> {};
then not ex t9 being Symbol of G st t=t9 &
not ex tnt being FinSequence st t9 ==> tnt;
then not t in {t9 where t9 is Symbol of G:
not ex tnt being FinSequence st t9 ==> tnt };
hence not t in Terminals G by LANG1:def 2;
end;
hence thesis by A10,A11,A12,A13,A15;
end;
A16: now
let n be Nat such that
A17: R[n];
thus R[n+1]
proof
let dt1, dt2 be DecoratedTree of SxD;
assume that
A18: dt1 in f.(n+1) and
A19: dt2 in f.(n+1) and
A20: dt1`1 = dt2`1;
A21: dom dt1 = dom dt1`1 by TREES_4:24;
A22: dom dt2 = dom dt1`1 by A20,TREES_4:24;
A23: dt1 in Union f by A1,A18,CARD_5:2;
A24: dt2 in Union f by A1,A19,CARD_5:2;
ex X being Subset of FinTrees [:the carrier of G(), D():]
st X = Union f() & (for d being Symbol of G() st d in Terminals G()
holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G(),
p being FinSequence of X st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
for F being Subset of FinTrees [:the carrier of G(), D():] st
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G(),
p being FinSequence of F st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
holds X c= F from DTCMin(A1, A4, A5);
then reconsider dt19 = dt1, dt29 = dt2 as Element of FinTrees SxD
by A23,A24;
A25: for n being Nat,
dt being Element of FinTrees [:the carrier of G(), D():]
st dt in Union f() holds dt in f().n iff height dom dt <= n
from DTCHeight (A1, A4, A5);
per cases;
suppose
A26: dt1 in f.n;
then height dom dt19 <= n by A23,A25;
then dt29 in f.n by A21,A22,A24,A25;
hence thesis by A17,A20,A26;
end;
suppose
A27: not dt1 in f.n;
A28: f.(n+1) = f.n \/ {[o1, NTV(o1, p1)]-tree p1
where o1 is Symbol of G, p1 is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st
p1 = q & o1 ==> pr1 roots q } by A3;
then dt1 in f.n or dt1 in {[o1, NTV(o1, p1)]-tree p1
where o1 is Symbol of G, p1 is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st p1 = q & o1 ==>
pr1 roots q } by A18,XBOOLE_0:def 3;
then consider o1 being Symbol of G, p1 being Element of (f.n)* such that
A29: dt1 = [o1, NTV(o1, p1)]-tree p1 and
A30: ex q being FinSequence of FinTrees SxD st p1 = q & o1 ==> pr1 roots q
by A27;
height dom dt19 > n by A23,A25,A27;
then
A31: not dt29 in f.n by A21,A22,A24,A25;
dt2 in f.n or dt2 in {[o2, NTV(o2, p2)]-tree p2
where o2 is Symbol of G, p2 is Element of (f.n)* :
ex q being FinSequence of FinTrees SxD st
p2 = q & o2 ==> pr1 roots q } by A19,A28,XBOOLE_0:def 3;
then consider o2 being Symbol of G, p2 being Element of (f.n)* such that
A32: dt2 = [o2, NTV(o2, p2)]-tree p2 and
A33: ex q being FinSequence of FinTrees SxD st p2 = q & o2 ==> pr1 roots q
by A31;
reconsider p1 as FinSequence of FinTrees SxD by A30;
consider p11 being FinSequence of FinTrees S such that
A34: dom p11 = dom p1 and
A35: for i being Nat st i in dom p1 holds ex T being Element
of FinTrees SxD st T = p1.i & p11.i = T`1 and
A36: ([o1, NTV(o1,p1)]-tree p1)`1 = o1-tree p11 by TREES_4:31;
reconsider p2 as FinSequence of FinTrees SxD by A33;
consider p21 being FinSequence of FinTrees S such that
A37: dom p21 = dom p2 and
A38: for i being Nat st i in dom p2 holds ex T being Element
of FinTrees SxD st T = p2.i & p21.i = T`1 and
A39: ([o2, NTV(o2,p2)]-tree p2)`1 = o2-tree p21 by TREES_4:31;
A40: o1 = o2 by A20,A29,A32,A36,A39,TREES_4:15;
A41: p11 = p21 by A20,A29,A32,A36,A39,TREES_4:15;
now
let k be Nat;
assume
A42: k in dom p11;
then consider p1k being Element of FinTrees SxD such that
A43: p1k = p1.k and
A44: p11.k = p1k`1 by A34,A35;
consider p2k being Element of FinTrees SxD such that
A45: p2k = p2.k and
A46: p21.k = p2k`1 by A37,A38,A41,A42;
A47: p1k in f.n by A34,A42,A43,Th2;
p2k in f.n by A37,A41,A42,A45,Th2;
hence p1.k = p2.k by A17,A41,A43,A44,A45,A46,A47;
end;
then p1 = p2 by A34,A37,A41,FINSEQ_1:13;
hence thesis by A29,A32,A40;
end;
end;
end;
A48: for n be Nat holds R[n] from NAT_1:sch 2(A6, A16);
let dt1, dt2 be DecoratedTree of SxD;
assume that
A49: dt1 in Union f and
A50: dt2 in Union f and
A51: dt1`1 = dt2`1;
consider n1 being object such that
A52: n1 in NAT and
A53: dt1 in f.n1 by A1,A49,CARD_5:2;
consider n2 being object such that
A54: n2 in NAT and
A55: dt2 in f.n2 by A1,A50,CARD_5:2;
reconsider n1, n2 as Element of NAT by A52,A54;
deffunc F(set,set) = { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f.$1)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q };
A56: for n being Nat holds f.n c= f.(n+1)
proof
let n be Nat;
f.(n+1) = f.n \/ F(n, f.n) by A3;
hence thesis by XBOOLE_1:7;
end;
A57: for k, s being Nat holds f.k c= f.(k+s)
by NAT_1:11,A56,MEASURE2:18;
n1 <= n2 or n1 >= n2;
then (ex s being Nat st n2 = n1 + s) or
ex s being Nat st n1 = n2 + s by NAT_1:10;
then f.n1 c= f.n2 or f.n2 c= f.n1 by A57;
hence thesis by A48,A51,A53,A55;
end;
definition
let G be non empty DTConstrStr;
func TS(G) -> Subset of FinTrees(the carrier of G) means
:Def1:
(for d being Symbol of G st d in Terminals G holds root-tree d in it) &
(for o being Symbol of G, p being FinSequence of it st o ==> roots p
holds o-tree p in it) & for F being Subset of FinTrees the carrier of G st
(for d being Symbol of G st d in Terminals G holds root-tree d in F) &
(for o being Symbol of G, p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds it c= F;
existence
proof
deffunc F(set,set) = $2 \/ { [o, A(o,pr1 roots p,pr2 roots p)]-tree p
where o is Symbol of G, p is Element of $2* :
ex q being FinSequence of FinTrees [:the carrier of G, NAT:] st
p = q & o ==> pr1 roots q };
consider f being Function such that
A1: dom f = NAT and
A2: f.0 = { root-tree [t, d] where t is Symbol of G, d is Element of NAT :
t in Terminals G & d = T(t) or t ==> {} & d = A(t,{},{}) } and
A3: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A4: for n being Nat holds f.(n+1) =
f.n \/ { [o, A(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G, p is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G, NAT:] st
p = q & o ==> pr1 roots q } by A3;
ex X1 being Subset of FinTrees(the carrier of G) st
X1 = { t`1 where t is Element of FinTrees [:(the carrier of G), NAT:] :
t in Union f }
& (for d being Symbol of G st d in Terminals G holds root-tree d in X1)
& (for o being Symbol of G, p being FinSequence of X1 st o ==> roots p
holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G st
(for d being Symbol of G st d in Terminals G holds root-tree d in F)
& (for o being Symbol of G, p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds X1 c= F from DTCSymbols (A1, A2, A4);
hence thesis;
end;
uniqueness;
end;
scheme DTConstrInd{ G()->non empty DTConstrStr, P[set] }:
for t being DecoratedTree of the carrier of G() st t in TS(G()) holds P[t]
provided
A1: for s being Symbol of G() st s in Terminals G() holds P[root-tree s] and
A2: for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts &
for t being DecoratedTree of the carrier of G() st t in rng ts holds P[t]
holds P[nt-tree ts]
proof
deffunc F(set,set) =
$2 \/ { [o, 0]-tree p where o is Symbol of G(), p is Element of $2* :
ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
p = q & o ==> pr1 roots q };
consider f being Function such that
A3: dom f = NAT and
A4: f.0 = { root-tree [t, d] where t is Symbol of G(), d is Element of NAT :
t in Terminals G() & d = T(t) or t ==> {} & d = A(t,{},{}) } and
A5: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A6: for n being Nat holds f.(n+1) =
f.n \/ { [o, A(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
p = q & o ==> pr1 roots q } by A5;
A7: ex
X being Subset of FinTrees [:the carrier of G(), NAT:] st X = Union f &
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, T(d)] in X) & (for o being Symbol of G(),
p being FinSequence of X st o ==> pr1 roots p
holds [o, A(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
for F being Subset of FinTrees [:the carrier of G(), NAT:] st
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, T(d)] in F ) & (for o being Symbol of G(),
p being FinSequence of F st o ==> pr1 roots p
holds [o, A(o, pr1 roots p, pr2 roots p)]-tree p in F)
holds X c= F from DTCMin (A3,A4,A6);
consider TSG being Subset of FinTrees(the carrier of G()) such that
A8: TSG = { t`1 where t is Element of FinTrees [:(the carrier of G()), NAT:]
: t in Union f } and
A9: for d being Symbol of G() st d in Terminals G()
holds root-tree d in TSG and
A10: for o being Symbol of G(), p being FinSequence of TSG st o ==> roots p
holds o-tree p in TSG and
A11: for F being Subset of FinTrees the carrier of G() st
(for d being Symbol of G() st d in Terminals G() holds root-tree d in F)
& (for o being Symbol of G(), p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds TSG c= F from DTCSymbols (A3, A4, A6);
A12: TSG = TS(G()) by A9,A10,A11,Def1;
defpred R[Nat] means
for t being DecoratedTree of [:the carrier of G(), NAT:]
st t in f.$1 holds P[t`1];
A13: R[0]
proof
let tt be DecoratedTree of [:the carrier of G(),NAT:];
set p = <*>TS G();
assume tt in f.0;
then consider t being Symbol of G(), d being Element of NAT such that
A14: tt = root-tree [t, d] and
A15: t in Terminals G() & d = 0 or t ==> roots p & d = 0 by A4,Th3;
A16: tt`1 = root-tree t by A14,TREES_4:25;
A17: t-tree p = root-tree t by TREES_4:20;
for T being DecoratedTree of the carrier of G() st T in rng p holds P[T];
hence thesis by A1,A2,A15,A16,A17;
end;
A18: now
let n be Nat;
assume
A19: R[n];
thus R[n+1]
proof
let x be DecoratedTree of [:the carrier of G(), NAT:];
assume that
A20: x in f.(n+1) and
A21: not P[x`1];
x in f.n \/ {[o, 0]-tree p where o is Symbol of G(),
p is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
p = q & o ==> pr1 roots q } by A5,A20;
then x in f.n or x in {[o, 0]-tree p where o is Symbol of G(),
p is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st
p = q & o ==> pr1 roots q } by XBOOLE_0:def 3;
then consider o being Symbol of G(), p being Element of (f.n)* such that
A22: x = [o, 0]-tree p and
A23: ex q being FinSequence of FinTrees [:the carrier of G(), NAT:] st p
= q & o ==> pr1 roots q
by A19,A21;
A24: Union f=union rng f by CARD_3:def 4;
n in NAT by ORDINAL1:def 12;
then
A25: f.n in rng f by A3,FUNCT_1:def 3;
A26: rng p c= f.n by FINSEQ_1:def 4;
A27: f.n c= Union f by A24,A25,ZFMISC_1:74;
A28: dom p = Seg len p by FINSEQ_1:def 3;
defpred P[set,set] means
ex dt being Element of FinTrees [:the carrier of G(), NAT:] st
dt = p.$1 & dt`1 = $2 & dt in Union f;
A29: for k being Nat st k in Seg len p
ex x being Element of FinTrees the carrier of G() st P[k,x]
proof
let k be Nat;
assume k in Seg len p;
then
A30: p.k in rng p by A28,FUNCT_1:def 3;
A31: rng p c= Union f by A26,A27;
then p.k in Union f by A30;
then reconsider dt = p.k as
Element of FinTrees [:(the carrier of G()), NAT:] by A7;
A32: dt`1 = pr1(the carrier of G(), NAT) * dt by TREES_3:def 12;
A33: rng dt c= [:the carrier of G(), NAT:] by RELAT_1:def 19;
dom pr1(the carrier of G(), NAT) = [:the carrier of G(), NAT:] by
FUNCT_2:def 1;
then dom dt`1 = dom dt by A32,A33,RELAT_1:27;
then reconsider x = dt`1 as Element of FinTrees the carrier of G()
by TREES_3:def 8;
take x, dt;
thus thesis by A30,A31;
end;
consider p1 being FinSequence of FinTrees the carrier of G() such that
A34: dom p1 = Seg len p and
A35: for k being Nat st k in Seg len p holds P[k,p1.k]
from FINSEQ_1:sch 5(A29);
reconsider p as FinSequence of Trees [:the carrier of G(), NAT:]
by A23,Th1;
A36: dom roots p1 = dom p1 by TREES_3:def 18;
A37: dom pr1 roots p = dom roots p by MCART_1:def 12;
then
A38: dom pr1 roots p = dom p1 by A28,A34,TREES_3:def 18;
now
let k be Nat;
assume
A39: k in dom p1;
then consider dt being Element of FinTrees [:the carrier of G(), NAT:]
such that
A40: dt = p.k and
A41: dt`1 = p1.k and dt in Union f by A34,A35;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st T = p1.k & (roots p1).k = T.{}
by A39,TREES_3:def 18;
then
A42: (roots p1).k = (dt.r)`1 by A41,TREES_3:39;
ex T being DecoratedTree st T = p.k & (roots p).k = T.{}
by A28,A34,A39,TREES_3:def 18;
hence (roots p1).k = (pr1 roots p).k
by A37,A38,A39,A40,A42,MCART_1:def 12;
end;
then
A43: roots p1 = pr1 roots p by A36,A38,FINSEQ_1:13;
rng p1 c= TS(G())
proof
let x be object;
assume x in rng p1;
then consider k being object such that
A44: k in dom p1 and
A45: x = p1.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A44;
ex dt being Element of FinTrees [:the carrier of G(), NAT:] st
dt = p.k & dt`1 = p1.k & dt in Union f by A34,A35,A44;
hence thesis by A8,A12,A45;
end;
then reconsider p1 as FinSequence of TS(G()) by FINSEQ_1:def 4;
now
let t be DecoratedTree of the carrier of G();
assume t in rng p1;
then consider k being object such that
A46: k in dom p1 and
A47: t = p1.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A46;
A48: ex dt being Element of FinTrees [:the carrier of G(), NAT:]
st ( dt = p.k)&( dt`1 = p1.k)&( dt in Union f) by A34,A35,A46;
p.k in rng p by A28,A34,A46,FUNCT_1:def 3;
hence P[t] by A19,A26,A47,A48;
end;
then
A49: P[o-tree p1] by A2,A23,A43;
reconsider p1 as FinSequence of Trees the carrier of G() by Th1;
now
let k be Nat;
assume k in dom p;
then ex dt being Element of FinTrees [:the carrier of G(), NAT:] st
dt = p.k & dt`1 = p1.k & dt in Union f by A28,A35;
hence for T being DecoratedTree of [:the carrier of G(), NAT:] st
T = p.k holds p1.k = T`1;
end;
hence contradiction by A21,A22,A28,A34,A49,TREES_4:27;
end;
end;
A50: for n being Nat holds R[n] from NAT_1:sch 2(A13, A18);
let t be DecoratedTree of the carrier of G();
assume t in TS(G());
then consider tt being Element of FinTrees[:the carrier of G(), NAT:] such
that
A51: t = tt`1 and
A52: tt in Union f by A8,A12;
ex n being object st n in NAT & tt in f.n by A3,A52,CARD_5:2;
hence thesis by A50,A51;
end;
scheme DTConstrIndDef{G()->non empty DTConstrStr, D()->non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D() }:
ex f being Function of TS(G()), D() st
(for t being Symbol of G() st t in Terminals G()
holds f.(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f.(nt-tree ts) = NTermVal(nt, roots ts, f * ts)
proof
set G = G();
deffunc
NTV(Symbol of G, FinSequence) = NTermVal($1, pr1 roots $2, pr2 roots $2);
deffunc F(set,set) = $2 \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G, p is Element of $2* :
ex q being FinSequence of FinTrees [:the carrier of G, D():] st
p = q & o ==> pr1 roots q };
consider f being Function such that
A1: dom f = NAT and
A2: f.0 = { root-tree [t, d] where t is Symbol of G, d is Element of D() :
t in Terminals G & d = TermVal(t) or
t ==> {} & d = NTermVal(t, {}, {}) } and
A3: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A4: for n being Nat holds f.(n+1) =
f.n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G, p is Element of (f.n)* :
ex q being FinSequence of FinTrees [:the carrier of G, D():] st
p = q & o ==> pr1 roots q } by A3;
ex X1 being Subset of FinTrees(the carrier of G) st
X1 = { t`1 where t is Element of FinTrees [:(the carrier of G), D():] :
t in Union f }
& (for d being Symbol of G st d in Terminals G holds root-tree d in X1)
& (for o being Symbol of G, p being FinSequence of X1 st o ==> roots p
holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G st
(for d being Symbol of G st d in Terminals G holds root-tree d in F)
& (for o being Symbol of G, p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds X1 c= F from DTCSymbols (A1, A2, A4);
then
A5: TS(G) = { t`1 where t is Element of FinTrees [:(the carrier of G), D
():] : t in Union f } by Def1;
defpred P[object,object] means
for dt being DecoratedTree of [:(the carrier of G), D():]
st dt in Union f & $1 = dt`1 holds $2 = (dt`2).{};
A6: for e being object st e in TS(G) ex u being object st u in D() & P[e,u]
proof
let e be object;
assume e in TS(G);
then consider DT being Element of FinTrees [:(the carrier of G), D():]
such that
A7: e = DT`1 and
A8: DT in Union f by A5;
reconsider r = {} as Node of DT`2 by TREES_1:22;
take u = (DT`2).r;
thus u in D();
A9: for dt1, dt2 being DecoratedTree of [:(the carrier of G), D():]
st dt1 in Union f & dt2 in Union f & dt1`1 = dt2`1 holds dt1 = dt2
from DTCUniq (A1, A2, A4);
let dt be DecoratedTree of [:(the carrier of G), D():];
assume that
A10: dt in Union f and
A11: e = dt`1;
thus thesis by A7,A8,A9,A10,A11;
end;
consider ff being Function such that
A12: dom ff = TS(G) & rng ff c= D() and
A13: for e being object st e in TS(G) holds P[e,ff.e] from FUNCT_1:sch 6(A6);
reconsider ff as Function of TS(G), D() by A12,FUNCT_2:def 1,RELSET_1:4;
take ff;
consider X be Subset of FinTrees [:the carrier of G, D():] such that
A14: X = Union f and
A15: for d being Symbol of G st d in Terminals G
holds root-tree [d, TermVal(d)] in X and
A16: for o being Symbol of G, p being FinSequence of X st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X and
for F being Subset of FinTrees [:the carrier of G, D():] st
(for d being Symbol of G st d in Terminals G
holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G,
p being FinSequence of F st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
holds X c= F from DTCMin (A1, A2, A4);
hereby
let t be Symbol of G;
assume
A17: t in Terminals G;
A18: (root-tree [t, TermVal(t)])`1 = root-tree t by TREES_4:25;
A19: (root-tree [t, TermVal(t)])`2 = root-tree TermVal(t) by TREES_4:25;
root-tree [t, TermVal(t)] in Union f by A14,A15,A17;
then root-tree t in TS(G) by A5,A18;
hence ff.(root-tree t) = (root-tree TermVal(t)).{} by A13,A14,A15,A17,A18
,A19
.= TermVal(t) by TREES_4:3;
end;
let nt be Symbol of G, ts be FinSequence of TS(G);
set rts = roots ts;
assume
A20: nt ==> rts;
set x = ff * ts;
A21: dom ts = Seg len ts by FINSEQ_1:def 3;
defpred P[set,set] means
ex dt being DecoratedTree of [:the carrier of G, D():] st
dt = $2 & dt`1 = ts.$1 & dt in Union f;
A22: for k being Nat st k in Seg len ts
ex x being Element of FinTrees [:(the carrier of G), D():] st P[k,x]
proof
let k be Nat;
assume k in Seg len ts;
then
A23: ts.k in rng ts by A21,FUNCT_1:def 3;
rng ts c= TS(G) by FINSEQ_1:def 4;
then ts.k in TS(G) by A23;
then ex x being Element of FinTrees [:(the carrier of G), D():] st
ts.k = x`1 & x in Union f by A5;
hence thesis;
end;
consider dts being FinSequence of FinTrees [:(the carrier of G), D():]
such that
A24: dom dts = Seg len ts and
A25: for k being Nat st k in Seg len ts holds P[k,dts.k]
from FINSEQ_1:sch 5(A22);
rng dts c= X
proof
let x be object;
assume x in rng dts;
then consider k being object such that
A26: k in dom ts and
A27: x = dts.k by A21,A24,FUNCT_1:def 3;
reconsider k as Element of NAT by A26;
ex dt being DecoratedTree of [:the carrier of G, D():]
st dt = x & dt`1 = ts.k & dt in Union f by A21,A25,A26,A27;
hence thesis by A14;
end;
then reconsider dts as FinSequence of X by FINSEQ_1:def 4;
A28: dom roots ts = dom ts by TREES_3:def 18;
A29: dom pr1 roots dts = dom roots dts by MCART_1:def 12;
A30: dom pr2 roots dts = dom roots dts by MCART_1:def 13;
A31: dom pr1 roots dts = dom ts by A21,A24,A29,TREES_3:def 18;
A32: dom pr2 roots dts = dom ts by A21,A24,A30,TREES_3:def 18;
now
let k be Nat;
assume
A33: k in dom ts;
then consider dt being DecoratedTree of [:the carrier of G, D():]
such that
A34: dt = dts.k and
A35: dt`1 = ts.k and dt in Union f by A21,A25;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st T = ts.k & (roots ts).k = T.{}
by A33,TREES_3:def 18;
then
A36: (roots ts).k = (dt.r)`1 by A35,TREES_3:39;
ex T being DecoratedTree st T = dts.k & (roots dts).k = T.{}
by A21,A24,A33,TREES_3:def 18;
hence (roots ts).k = (pr1 roots dts).k
by A29,A31,A33,A34,A36,MCART_1:def 12;
end;
then
A37: roots ts = pr1 roots dts by A28,A31,FINSEQ_1:13;
then
A38: [nt, NTV(nt, dts)]-tree dts in X by A16,A20;
A39: rng dts c= FinTrees [:the carrier of G, D():] by FINSEQ_1:def 4;
FinTrees [:the carrier of G,D():] c= Trees [:the carrier of G, D():]
by TREES_3:21;
then rng dts c= Trees [:the carrier of G, D():] by A39;
then reconsider dts9 = dts as FinSequence of Trees [:the carrier of G,D():]
by FINSEQ_1:def 4;
A40: rng ts c= FinTrees the carrier of G by FINSEQ_1:def 4;
FinTrees the carrier of G c= Trees the carrier of G by TREES_3:21;
then rng ts c= Trees the carrier of G by A40;
then reconsider ts9 = ts as FinSequence of Trees the carrier of G
by FINSEQ_1:def 4;
now
let i be Nat;
assume i in dom dts;
then
A41: ex dt being DecoratedTree of [:the carrier of G, D():] st (
dt = dts.i)&( dt`1 = ts.i)&( dt in Union f) by A24,A25;
let T be DecoratedTree of [:the carrier of G, D():];
assume T = dts.i;
hence ts.i = T`1 by A41;
end;
then
A42: ([nt, NTV(nt, dts)]-tree dts9)`1 = nt-tree ts9 by A21,A24,TREES_4:27;
A43: rng ts c= dom ff by A12,FINSEQ_1:def 4;
then
A44: dom (ff * ts) = dom ts by RELAT_1:27;
now
let k be Nat;
assume
A45: k in dom ts;
then consider dt being DecoratedTree of [:the carrier of G, D():] such
that
A46: dt = dts.k and
A47: dt`1 = ts.k and
A48: dt in Union f by A21,A25;
reconsider r = {} as Node of dt by TREES_1:22;
A49: ts.k in rng ts by A45,FUNCT_1:def 3;
A50: x.k = ff.(dt`1) by A44,A45,A47,FUNCT_1:12
.= dt`2.{} by A12,A13,A43,A47,A48,A49
.= (dt.r)`2 by TREES_3:39;
ex T being DecoratedTree st T = dts.k & (roots dts).k = T.r
by A21,A24,A45,TREES_3:def 18;
hence x.k = (pr2 roots dts).k by A29,A31,A45,A46,A50,MCART_1:def 13;
end;
then
A51: x = pr2 roots dts by A32,A44,FINSEQ_1:13;
reconsider r = {} as Node of [nt, NTermVal(nt, rts, x)]-tree dts
by TREES_1:22;
nt-tree ts in TS(G) by A5,A14,A38,A42;
then ff.(nt-tree ts) = (([nt, NTermVal(nt, rts, x)]-tree dts)`2).r
by A13,A14,A16,A20,A37,A42,A51
.= (([nt, NTermVal(nt, rts, x)]-tree dts).r)`2 by TREES_3:39
.= [nt, NTermVal(nt, rts, x)]`2 by TREES_4:def 4;
hence thesis;
end;
scheme DTConstrUniqDef{G()->non empty DTConstrStr, D()->non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D(),
f1, f2() -> Function of TS(G()), D() }: f1() = f2()
provided
A1: (for t being Symbol of G() st t in Terminals G()
holds f1().(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f1().(nt-tree ts) = NTermVal(nt, roots ts, f1() * ts) and
A2: (for t being Symbol of G() st t in Terminals G()
holds f2().(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f2().(nt-tree ts) = NTermVal(nt, roots ts, f2() * ts)
proof
set G = G();
defpred P[set] means f1().$1 = f2().$1;
A3: now
let s be Symbol of G;
assume
A4: s in Terminals G;
then f1().(root-tree s) = TermVal(s) by A1
.= f2().(root-tree s) by A2,A4;
hence P[root-tree s];
end;
A5: now
let nt be Symbol of G, ts be FinSequence of TS(G);
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of G st t in rng ts holds P [t];
A8: rng ts c= TS(G) by FINSEQ_1:def 4;
then rng ts c= dom f1() by FUNCT_2:def 1;
then
A9: dom (f1() * ts) = dom ts by RELAT_1:27;
reconsider ntv1 = f1() * ts as FinSequence;
reconsider ntv1 as FinSequence of D();
rng ts c= dom f2() by A8,FUNCT_2:def 1;
then
A10: dom (f2() * ts) = dom ts by RELAT_1:27;
now
let x be object;
assume
A11: x in dom ts;
then reconsider t =ts.x as Element of FinTrees the carrier of G by Th2;
t in rng ts by A11,FUNCT_1:def 3;
then
A12: f1().t = f2().t by A7;
thus (f1() * ts).x = f1().t by A9,A11,FUNCT_1:12
.= (f2() * ts).x by A10,A11,A12,FUNCT_1:12;
end;
then
A13: f1() * ts = f2() * ts by A9,A10,FUNCT_1:2;
f1().(nt-tree ts) = NTermVal (nt, roots ts, ntv1) by A1,A6
.= f2().(nt-tree ts) by A2,A6,A13;
hence P[nt-tree ts];
end;
for t being DecoratedTree of the carrier of G st t in TS(G)
holds P[t] from DTConstrInd (A3,A5);
then for x being object st x in TS(G) holds f1().x = f2().x;
hence thesis by FUNCT_2:12;
end;
begin
:: Peano naturals: an example of a decorated tree construction
defpred P[set,set] means $1=1 & ($2=<*0*> or $2=<*1*>);
definition
func PeanoNat -> strict non empty DTConstrStr means
:Def2:
the carrier of it = {0, 1} &
for x being Symbol of it, y being FinSequence of the carrier of it
holds x ==> y iff x=1 & (y=<*0*> or y=<*1*>);
existence
proof
thus
ex G be strict non empty DTConstrStr st the carrier of G = {0,1} &
for x being Symbol of G, p being FinSequence of the carrier of G
holds x ==> p iff P[x, p] from DTConstrStrEx;
end;
uniqueness
proof
thus for G1, G2 being strict non empty DTConstrStr
st (the carrier of G1 = {0,1} &
for x being Symbol of G1, p being FinSequence of the carrier of G1
holds x ==> p iff P[x, p]) & (the carrier of G2 = {0,1} &
for x being Symbol of G2, p being FinSequence of the carrier of G2
holds x ==> p iff P[x, p]) holds G1 = G2 from DTConstrStrUniq;
end;
end;
set PN = PeanoNat;
Lm2: the carrier of PN = {0, 1} by Def2;
then reconsider O = 0 , S = 1 as Symbol of PN by TARSKI:def 2;
Lm3: S ==> <*O*> by Def2;
Lm4: S ==> <*S*> by Def2;
Lm5: S ==> <*O*> by Def2;
Lm6: S ==> <*S*> by Def2;
Lm7: Terminals PN = {x where x is Symbol of PN :
not ex tnt being FinSequence st x ==> tnt } by LANG1:def 2;
Lm8: now
given x being FinSequence such that
A1: O ==> x;
[O, x] in the Rules of PN by A1,LANG1:def 1;
then x in (the carrier of PN)* by ZFMISC_1:87;
then x is FinSequence of the carrier of PN by FINSEQ_2:def 3;
hence contradiction by A1,Def2;
end;
then
Lm9: O in Terminals PN by Lm7;
Lm10: Terminals PN c= {O}
proof
let x be object;
assume x in Terminals PN;
then consider y being Symbol of PN such that
A1: x = y and
A2: not ex tnt being FinSequence st y ==> tnt by Lm7;
y = O or y = S & {O, S} <> {} by Lm2,TARSKI:def 2;
hence thesis by A1,A2,Lm5,TARSKI:def 1;
end;
Lm11: NonTerminals PN = {x where x is Symbol of PN :
ex tnt being FinSequence st x ==> tnt } by LANG1:def 3;
then
Lm12: S in NonTerminals PN by Lm5;
then
Lm13: {S} c= NonTerminals PN by ZFMISC_1:31;
Lm14: NonTerminals PN c= {S}
proof
let x be object;
assume x in NonTerminals PN;
then consider y being Symbol of PN such that
A1: x = y and
A2: ex tnt being FinSequence st y ==> tnt by Lm11;
y = O or y = S by Lm2,TARSKI:def 2;
hence thesis by A1,A2,Lm8,TARSKI:def 1;
end;
then
Lm15: NonTerminals PN = { S } by Lm13;
reconsider TSPN = TS(PN) as non empty Subset of FinTrees the carrier of PN by
Def1,Lm9;
begin
:: Some properties of decorated tree constructions
definition
let G be non empty DTConstrStr;
attr G is with_terminals means
:Def3:
Terminals G <> {};
attr G is with_nonterminals means
:Def4:
NonTerminals G <> {};
attr G is with_useful_nonterminals means
:Def5:
for nt being Symbol of G st nt in NonTerminals G
ex p being FinSequence of TS(G) st nt ==> roots p;
end;
Lm16: PN is with_terminals with_nonterminals with_useful_nonterminals
proof
thus Terminals PN <> {} by Lm9;
thus NonTerminals PN <> {} by Lm12;
reconsider rO = root-tree O as Element of TSPN by Def1,Lm9;
reconsider p = <*rO qua Element of TSPN qua non empty set*>
as FinSequence of TSPN;
reconsider p as FinSequence of TS(PN);
let nt be Symbol of PN;
assume nt in NonTerminals PN;
then
A1: nt = S by Lm14,TARSKI:def 1;
take p;
A2: dom <*rO*> = Seg 1 by FINSEQ_1:38;
A3: dom <*O*> = Seg 1 by FINSEQ_1:38;
now
let i be Element of NAT;
assume
A4: i in dom p;
reconsider rO as DecoratedTree;
take rO;
A5: i = 1 by A2,A4,FINSEQ_1:2,TARSKI:def 1;
thus rO = p.i & <*O*>.i = rO.{} by A5,TREES_4:3;
end;
hence thesis by A1,A2,A3,Lm5,TREES_3:def 18;
end;
registration
cluster with_terminals with_nonterminals with_useful_nonterminals strict
for non empty DTConstrStr;
existence by Lm16;
end;
definition
let G be with_terminals non empty DTConstrStr;
redefine func Terminals G -> non empty Subset of G; :: redefines Terminals (LANG1, definition)
coherence
proof
defpred P[Element of G] means not ex tnt being FinSequence st $1 ==> tnt;
{ t where t is Element of G : P[t] } c= the carrier of G
from FRAENKEL:sch 10;
hence thesis by Def3,LANG1:def 2;
end;
end;
registration
let G be with_terminals non empty DTConstrStr;
cluster TS G -> non empty;
coherence
proof
ex t being object st t in Terminals G by XBOOLE_0:def 1;
hence thesis by Def1;
end;
end;
registration
let G be with_useful_nonterminals non empty DTConstrStr;
cluster TS G -> non empty;
coherence
proof
set s = the Symbol of G;
per cases;
suppose not ex tnt being FinSequence st s ==> tnt;
then s in {t where t is Symbol of G:
not ex tnt being FinSequence st t ==> tnt };
then s in Terminals G by LANG1:def 2;
hence thesis by Def1;
end;
suppose ex tnt being FinSequence st s ==> tnt;
then s in {t where t is Symbol of G:
ex tnt being FinSequence st t ==> tnt };
then s in NonTerminals G by LANG1:def 3;
then ex p being FinSequence of TS G st ( s ==> roots p) by Def5;
hence thesis by Def1;
end;
end;
end;
definition
let G be with_nonterminals non empty DTConstrStr;
redefine func NonTerminals G -> non empty Subset of G; :: redefines NonTerminals (LANG1, definition)
coherence
proof
defpred P[Element of G] means ex tnt being FinSequence st $1 ==> tnt;
{ t where t is Element of G : P[t]} c= the carrier of G
from FRAENKEL:sch 10;
hence thesis by Def4,LANG1:def 3;
end;
end;
definition
let G be with_terminals non empty DTConstrStr;
mode Terminal of G is Element of Terminals G;
end;
definition
let G be with_nonterminals non empty DTConstrStr;
mode NonTerminal of G is Element of NonTerminals G;
end;
definition
let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;
let nt be NonTerminal of G;
mode SubtreeSeq of nt -> FinSequence of TS(G) means
:Def6:
nt ==> roots it;
existence by Def5;
end;
definition
let G be with_terminals non empty DTConstrStr;
let t be Terminal of G;
redefine func root-tree t -> Element of TS(G); :: redefines root-tree (TREES_4, definition)
coherence by Def1;
end;
definition
let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;
let nt be NonTerminal of G;
let p be SubtreeSeq of nt;
redefine func nt-tree p -> Element of TS(G); :: redefines -tree (TREES_4, definition)
coherence
proof
nt ==> roots p by Def6;
hence thesis by Def1;
end;
end;
theorem Th9:
for G being with_terminals non empty DTConstrStr,
tsg being Element of TS G, s being Terminal of G
st tsg.{} = s holds tsg = root-tree s
proof
let G be with_terminals non empty DTConstrStr, tsg be Element of TS G,
s be Terminal of G;
assume
A1: tsg.{} = s;
defpred P[DecoratedTree of the carrier of G] means
for s being Terminal of G st $1.{} = s holds $1 = root-tree s;
A2: for s being Symbol of G st s in Terminals G holds P[root-tree s]
by TREES_4:3;
A3: now
let nt be Symbol of G, ts be FinSequence of TS G;
assume that
A4: nt ==> roots ts
and for t being DecoratedTree of the carrier of G st t in rng ts holds P
[t];
thus P[nt-tree ts]
proof
let s be Terminal of G;
assume
A5: (nt-tree ts).{} = s;
A6: (nt-tree ts).{} = nt by TREES_4:def 4;
A7: s in Terminals G;
Terminals G = { t where t is Symbol of G : not ex tnt being FinSequence
st t ==> tnt } by LANG1:def 2;
then ex t being Symbol of G st s = t &
not ex tnt being FinSequence st t ==> tnt by A7;
hence thesis by A4,A5,A6;
end;
end;
for t being DecoratedTree of the carrier of G st t in TS G holds P[t]
from DTConstrInd (A2,A3);
hence thesis by A1;
end;
theorem Th10:
for G being with_terminals with_nonterminals non empty DTConstrStr,
tsg being Element of TS G, nt being NonTerminal of G st tsg.{} = nt
ex ts being FinSequence of TS G st tsg = nt-tree ts & nt ==> roots ts
proof
let G be with_terminals with_nonterminals non empty DTConstrStr;
defpred P[DecoratedTree of the carrier of G] means
for nt being NonTerminal of G st $1.{} = nt ex ts being FinSequence of TS G
st $1 = nt-tree ts & nt ==> roots ts;
A1: now
let s be Symbol of G;
assume
A2: s in Terminals G;
thus P[root-tree s]
proof
let nt be NonTerminal of G;
assume (root-tree s).{} = nt;
then
A3: s = nt by TREES_4:3;
Terminals G = { t where t is Symbol of G :
not ex tnt being FinSequence st t ==> tnt } by LANG1:def 2;
then
A4: ex t being Symbol of G st s = t &
not ex tnt being FinSequence st t ==> tnt by A2;
A5: nt in NonTerminals G;
NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence
st t ==> tnt } by LANG1:def 3;
then ex t being Symbol of G st nt = t &
ex tnt being FinSequence st t ==> tnt by A5;
hence thesis by A3,A4;
end;
end;
A6: now
let nnt be Symbol of G, tts be FinSequence of TS G;
assume that
A7: nnt ==> roots tts
and for t being DecoratedTree of the carrier of G st t in rng tts holds
P[t];
thus P[nnt-tree tts]
proof
let nt be NonTerminal of G;
assume
A8: (nnt-tree tts).{} = nt;
take ts = tts;
thus thesis by A7,A8,TREES_4:def 4;
end;
end;
A9: for t being DecoratedTree of the carrier of G st t in TS G holds P[t]
from DTConstrInd (A1,A6);
let tsg be Element of TS G, nt be NonTerminal of G;
assume tsg.{} = nt;
hence thesis by A9;
end;
begin
:: Peano naturals continued
registration
cluster PeanoNat ->
with_terminals with_nonterminals with_useful_nonterminals;
coherence by Lm16;
end;
set PN = PeanoNat;
reconsider O as Terminal of PN by Lm9;
reconsider S as NonTerminal of PN by Lm12;
definition
let nt be NonTerminal of PeanoNat, t be Element of TS PeanoNat;
redefine func nt-tree t -> Element of TS PeanoNat; :: redefines -tree (TREES_4, definition)
coherence
proof
reconsider r = {} as Node of t by TREES_1:22;
t.r = 0 or t.r = 1 by Lm2,TARSKI:def 2;
then
A1: roots <*t*> = <*0*> or roots <*t*> = <*1*> by Th4;
nt = S by Lm15,TARSKI:def 1;
then nt-tree <*t*> in TS PN by A1,Def1,Lm5,Lm6;
hence thesis by TREES_4:def 5;
end;
end;
definition
let x be FinSequence of NAT;
func plus-one x -> Element of NAT equals
(x.1) + 1;
coherence;
end;
deffunc N(set,set,FinSequence of NAT) = plus-one($3);
definition
func PN-to-NAT -> Function of TS(PeanoNat), NAT means
:Def8:
(for t being Symbol of PeanoNat st t in Terminals PeanoNat
holds it.(root-tree t) = 0) & for nt being Symbol of PeanoNat,
ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
holds it.(nt-tree ts) = plus-one(it * ts);
existence
proof
thus ex f being Function of TS(PeanoNat), NAT st
(for t being Symbol of PeanoNat st t in Terminals PeanoNat
holds f.(root-tree t) = T(t)) & for nt being Symbol of PeanoNat,
ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
holds f.(nt-tree ts) = N(nt, roots ts, f * ts qua FinSequence of NAT)
from DTConstrIndDef;
end;
uniqueness
proof
let it1, it2 be Function of TS(PeanoNat), NAT such that
A1: (for t being Symbol of PeanoNat st t in Terminals PeanoNat
holds it1.(root-tree t) = T(t)) & for nt being Symbol of PeanoNat,
ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
holds it1.(nt-tree ts) =
N(nt,roots ts,it1 * ts qua FinSequence of NAT) and
A2: (for t being Symbol of PeanoNat st t in Terminals PeanoNat
holds it2.(root-tree t) = T(t)) & for nt being Symbol of PeanoNat,
ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
holds it2.(nt-tree ts) = N(nt,roots ts,it2 * ts qua FinSequence of NAT);
thus it1 = it2 from DTConstrUniqDef (A1,A2);
end;
end;
definition
let x be Element of TS(PeanoNat);
func PNsucc x -> Element of TS(PeanoNat) equals
1-tree <*x*>;
coherence
proof
reconsider r = {} as Node of x by TREES_1:22;
A1: roots <*x*> = <*x.r*> by Th4;
x.r = O or x.r = S by Lm2,TARSKI:def 2;
hence thesis by A1,Def1,Lm5,Lm6;
end;
end;
deffunc F(set,Element of TS(PeanoNat)) = PNsucc $2;
definition
func NAT-to-PN -> sequence of TS(PeanoNat) means
:Def10:
it.0 = root-tree 0 & for n being Nat holds it.(n+1) = PNsucc it.n;
existence
proof
ex f being sequence of TS(PeanoNat) st f.0 = root-tree O &
for n being Nat
holds f.(n+1) = F(n,f.n qua Element of TS(PeanoNat)) from NAT_1:sch 12;
hence thesis;
end;
uniqueness
proof
let it1, it2 be sequence of TS(PeanoNat);
assume
A1: not thesis;
then
A2: it1.0 = root-tree O;
A3: for n being Nat
holds it1.(n+1) = F(n,it1.n qua Element of TS(PeanoNat)) by A1;
A4: it2.0 = root-tree O by A1;
A5: for n being Nat
holds it2.(n+1) = F(n,it2.n qua Element of TS(PeanoNat)) by A1;
it1 = it2 from NAT_1:sch 16(A2,A3, A4,A5);
hence thesis by A1;
end;
end;
theorem
for pn being Element of TS(PeanoNat) holds pn = NAT-to-PN.(PN-to-NAT.pn)
proof
defpred P[DecoratedTree of the carrier of PN] means
$1 = NAT-to-PN.(PN-to-NAT.$1);
A1: now
let s be Symbol of PN;
assume
A2: s in Terminals PN;
then NAT-to-PN.(PN-to-NAT.(root-tree s)) = NAT-to-PN.0 by Def8
.= root-tree O by Def10;
hence P[root-tree s] by A2,Lm10,TARSKI:def 1;
end;
A3: now
let nt be Symbol of PN, ts be FinSequence of TS(PN);
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
A6: nt <> O by A4,Lm8;
roots ts = <*O*> or roots ts = <*S*> by A4,Def2;
then len roots ts = 1 by FINSEQ_1:40;
then consider dt being Element of FinTrees the carrier of PN such that
A7: ts = <*dt*> and
A8: dt in TS(PN) by Th5;
reconsider dt as Element of TS(PN) by A8;
rng ts = {dt} by A7,FINSEQ_1:38;
then dt in rng ts by TARSKI:def 1;
then
A9: dt = NAT-to-PN.(PN-to-NAT.dt) by A5;
A10: PN-to-NAT * ts = <*PN-to-NAT.dt*> by A7,FINSEQ_2:35;
set N = PN-to-NAT.dt;
A11: plus-one(<*N*>) = N+1;
NAT-to-PN.(N+1) = PNsucc dt by A9,Def10
.= nt-tree ts by A6,A7,Lm2,TARSKI:def 2;
hence P[nt-tree ts] by A4,A10,A11,Def8;
end;
for t being DecoratedTree of the carrier of PN
st t in TS(PN) holds P[t] from DTConstrInd (A1,A3);
hence thesis;
end;
Lm17: 0 = PN-to-NAT.(root-tree O) by Def8
.= PN-to-NAT.(NAT-to-PN.0) by Def10;
Lm18: now
let n be Element of NAT;
assume
A1: n = PN-to-NAT.(NAT-to-PN.n);
reconsider dt = NAT-to-PN.n as Element of TS(PN);
reconsider r = {} as Node of dt by TREES_1:22;
A2: dt.r = O or dt.r = S by Lm2,TARSKI:def 2;
A3: NAT-to-PN.(n+1) = PNsucc (NAT-to-PN.n) by Def10
.= S-tree <*NAT-to-PN.n*>;
A4: S ==> roots <*NAT-to-PN.n*> by A2,Lm3,Lm4,Th4;
<*PN-to-NAT.(NAT-to-PN.n)*> = PN-to-NAT * <*NAT-to-PN.n*> by FINSEQ_2:35;
then PN-to-NAT.(S-tree <*NAT-to-PN.n*>) = plus-one <*n*> by A1,A4,Def8
.= n+1;
hence n+1 = PN-to-NAT.(NAT-to-PN.(n+1)) by A3;
end;
theorem
for n being Nat holds n = PN-to-NAT.(NAT-to-PN.n)
proof
defpred P[Nat] means $1 = PN-to-NAT.(NAT-to-PN.$1);
A1: P[0] by Lm17;
A2: for n being Nat st P[n] holds P[n+1] by Lm18;
thus for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
end;
begin
:: Tree traversals and terminal language
definition
let G be non empty DTConstrStr, tsg be DecoratedTree of the carrier of G;
assume
A1: tsg in TS G;
defpred C[object] means $1 in Terminals G;
deffunc F(object) = <*$1*>;
deffunc G(object) = {};
A2: now
let x be object;
assume x in the carrier of G;
hereby
assume
A3: C[x];
then reconsider T = Terminals G as non empty set;
reconsider x9 = x as Element of T by A3;
<*x9*> is FinSequence of T;
hence F(x) in (Terminals G)*;
end;
assume not C[x];
<*>Terminals G = {};
hence G(x) in (Terminals G)*;
end;
consider s2t being Function of the carrier of G, (Terminals G)* such that
A4: for s being object st s in the carrier of G holds
(C[s] implies s2t.s = F(s)) &
(not C[s] implies s2t.s = G(s)) from FUNCT_2:sch 5(A2);
deffunc T(Symbol of G) = s2t.$1;
deffunc N(set,set,FinSequence of (Terminals G)*) = FlattenSeq($3);
deffunc F(object) = <*$1*>;
func TerminalString tsg -> FinSequence of Terminals G means
:Def11:
ex f being Function of (TS G), (Terminals G)* st it = f.tsg &
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f.(nt-tree ts) = FlattenSeq(f * ts);
existence
proof
consider f being Function of TS(G), (Terminals G)* such that
A5: (for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = T(t)) & for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f.(nt-tree ts) = N(nt,roots ts,f * ts) from DTConstrIndDef;
f.tsg is Element of (Terminals G)* by A1,FUNCT_2:5;
then reconsider IT = f.tsg as FinSequence of Terminals G;
take IT, f;
thus IT = f.tsg;
hereby
let t be Symbol of G;
assume
A6: t in Terminals G;
then f.(root-tree t) = s2t.t by A5;
hence f.(root-tree t) = <*t*> by A4,A6;
end;
thus thesis by A5;
end;
uniqueness
proof
let it1, it2 be FinSequence of Terminals G;
given f1 being Function of (TS G), (Terminals G)* such that
A7: it1 = f1.tsg and
A8: for t being Symbol of G st t in Terminals G holds f1.(root-tree t)
= <*t*> and
A9: for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==>
roots ts holds f1.(nt-tree ts) = FlattenSeq(f1 * ts);
given f2 being Function of (TS G), (Terminals G)* such that
A10: it2 = f2.tsg and
A11: for t being Symbol of G st t in Terminals G holds f2.(root-tree t)
= <*t*> and
A12: for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==>
roots ts holds f2.(nt-tree ts) = FlattenSeq(f2 * ts);
A13: now
hereby
let t be Symbol of G;
assume
A14: t in Terminals G;
hence f1.(root-tree t) = <*t*> by A8
.= T(t) by A4,A14;
end;
thus for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f1.(nt-tree ts) = N(nt,roots ts,f1 * ts) by A9;
end;
A15: now
hereby
let t be Symbol of G;
assume
A16: t in Terminals G;
hence f2.(root-tree t) = <*t*> by A11
.= T(t) by A4,A16;
end;
thus for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f2.(nt-tree ts) = N(nt,roots ts,f2 * ts) by A12;
end;
f1 = f2 from DTConstrUniqDef (A13, A15);
hence thesis by A7,A10;
end;
A17: now
let x be object;
assume x in the carrier of G;
then reconsider x9 = x as Element of G;
<*x9*> is FinSequence of the carrier of G;
hence F(x) in (the carrier of G)*;
end;
consider s2s being Function of the carrier of G, (the carrier of G)*
such that
A18: for s being object st s in the carrier of G holds s2s.s = F(s)
from FUNCT_2:sch 2(A17);
deffunc T(Symbol of G) = s2s.$1;
deffunc N(Symbol of G,set,FinSequence of (the carrier of G)*) =
s2s.$1^FlattenSeq($3);
func PreTraversal tsg -> FinSequence of the carrier of G means
:Def12:
ex f being Function of (TS G), (the carrier of G)* st it = f.tsg &
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
ts being FinSequence of TS(G),
rts being FinSequence st rts = roots ts & nt ==> rts
for x being FinSequence of (the carrier of G)* st x = f * ts
holds f.(nt-tree ts) = <*nt*>^FlattenSeq(x);
existence
proof
deffunc T(Symbol of G) = s2s.$1;
deffunc N(Symbol of G,set,FinSequence of (the carrier of G)*) =
s2s.$1^FlattenSeq($3);
consider f being Function of TS(G), (the carrier of G)* such that
A19: (for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = T(t)) & for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f.(nt-tree ts) = N(nt,roots ts,f * ts) from DTConstrIndDef;
f.tsg is Element of (the carrier of G)* by A1,FUNCT_2:5;
then reconsider IT=f.tsg as FinSequence of the carrier of G;
take IT, f;
thus IT = f.tsg;
hereby
let t be Symbol of G;
assume t in Terminals G;
then f.(root-tree t) = s2s.t by A19;
hence f.(root-tree t) = <*t*> by A18;
end;
let nt be Symbol of G, ts be FinSequence of TS(G), rts be FinSequence;
assume that
A20: rts = roots ts and
A21: nt ==> rts;
let x be FinSequence of (the carrier of G)*;
assume x = f * ts;
hence f.(nt-tree ts) = s2s.nt^FlattenSeq(x) by A19,A20,A21
.= <*nt*>^FlattenSeq(x) by A18;
end;
uniqueness
proof
let it1, it2 be FinSequence of the carrier of G;
given f1 being Function of (TS G), (the carrier of G)* such that
A22: it1 = f1.tsg and
A23: for t being Symbol of G st t in Terminals G holds f1.(root-tree t)
= <*t*> and
A24: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
carrier of G)* st x = f1 * ts holds f1.(nt-tree ts) = <*nt*>^FlattenSeq(x);
given f2 being Function of (TS G), (the carrier of G)* such that
A25: it2 = f2.tsg and
A26: for t being Symbol of G st t in Terminals G holds f2.(root-tree t)
= <*t*> and
A27: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
carrier of G)* st x = f2 * ts holds f2.(nt-tree ts) = <*nt*>^FlattenSeq(x);
A28: now
hereby
let t be Symbol of G;
assume t in Terminals G;
hence f1.(root-tree t) = <*t*> by A23
.= T(t) by A18;
end;
let nt be Symbol of G, ts be FinSequence of TS(G);
assume nt ==> roots ts;
hence f1.(nt-tree ts) = <*nt*>^FlattenSeq(f1 * ts) by A24
.= N(nt,roots ts,f1 * ts) by A18;
end;
A29: now
hereby
let t be Symbol of G;
assume t in Terminals G;
hence f2.(root-tree t) = <*t*> by A26
.= T(t) by A18;
end;
let nt be Symbol of G, ts be FinSequence of TS(G);
assume nt ==> roots ts;
hence f2.(nt-tree ts) = <*nt*>^FlattenSeq(f2 * ts) by A27
.= N(nt,roots ts,f2 * ts) by A18;
end;
f1 = f2 from DTConstrUniqDef (A28, A29);
hence thesis by A22,A25;
end;
deffunc T(Symbol of G) = s2s.$1;
deffunc N(Symbol of G,set,FinSequence of (the carrier of G)*) =
FlattenSeq($3)^s2s.$1;
func PostTraversal tsg -> FinSequence of the carrier of G means
:Def13:
ex f being Function of (TS G), (the carrier of G)* st it = f.tsg &
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
ts being FinSequence of TS(G),
rts being FinSequence st rts = roots ts & nt ==> rts
for x being FinSequence of (the carrier of G)* st x = f * ts
holds f.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
existence
proof
consider f being Function of TS(G), (the carrier of G)* such that
A30: (for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = T(t)) & for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f.(nt-tree ts) = N(nt,roots ts,f * ts) from DTConstrIndDef;
f.tsg is Element of (the carrier of G)* by A1,FUNCT_2:5;
then reconsider IT=f.tsg as FinSequence of the carrier of G;
take IT, f;
thus IT = f.tsg;
hereby
let t be Symbol of G;
assume t in Terminals G;
then f.(root-tree t) = s2s.t by A30;
hence f.(root-tree t) = <*t*> by A18;
end;
let nt be Symbol of G, ts be FinSequence of TS(G), rts be FinSequence;
assume that
A31: rts = roots ts and
A32: nt ==> rts;
let x be FinSequence of (the carrier of G)*;
assume x = f * ts;
hence f.(nt-tree ts) = FlattenSeq(x)^s2s.nt by A30,A31,A32
.= FlattenSeq(x)^<*nt*> by A18;
end;
uniqueness
proof
let it1, it2 be FinSequence of the carrier of G;
given f1 being Function of (TS G), (the carrier of G)* such that
A33: it1 = f1.tsg and
A34: for t being Symbol of G st t in Terminals G holds f1.(root-tree t)
= <*t*> and
A35: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
carrier of G)* st x = f1 * ts holds f1.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
given f2 being Function of (TS G), (the carrier of G)* such that
A36: it2 = f2.tsg and
A37: for t being Symbol of G st t in Terminals G holds f2.(root-tree t)
= <*t*> and
A38: for nt being Symbol of G, ts being FinSequence of TS(G), rts being
FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (the
carrier of G)* st x = f2 * ts holds f2.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
A39: now
hereby
let t be Symbol of G;
assume t in Terminals G;
hence f1.(root-tree t) = <*t*> by A34
.= T(t) by A18;
end;
let nt be Symbol of G, ts be FinSequence of TS(G);
assume nt ==> roots ts;
hence f1.(nt-tree ts) = FlattenSeq(f1 * ts)^<*nt*> by A35
.= N(nt,roots ts,f1 * ts) by A18;
end;
A40: now
hereby
let t be Symbol of G;
assume t in Terminals G;
hence f2.(root-tree t) = <*t*> by A37
.= T(t) by A18;
end;
let nt be Symbol of G, ts be FinSequence of TS(G);
assume nt ==> roots ts;
hence f2.(nt-tree ts) = FlattenSeq(f2 * ts)^<*nt*> by A38
.= N(nt,roots ts,f2 * ts) by A18;
end;
f1 = f2 from DTConstrUniqDef (A39, A40);
hence thesis by A33,A36;
end;
end;
definition
let G be with_nonterminals non empty non empty DTConstrStr,
nt be Symbol of G;
func TerminalLanguage nt -> Subset of (Terminals G)* equals
{ TerminalString tsg where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
coherence
proof
set TL = { TerminalString tsg
where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
TL c= (Terminals G)*
proof
let x be object;
assume x in TL;
then ex tsg being Element of FinTrees the carrier of G st ( x =
TerminalString tsg)&( tsg in TS G)&( tsg.{} = nt);
hence thesis by FINSEQ_1:def 11;
end;
hence thesis;
end;
func PreTraversalLanguage nt -> Subset of (the carrier of G)* equals
{ PreTraversal tsg where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
coherence
proof
set TL = { PreTraversal tsg
where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
TL c= (the carrier of G)*
proof
let x be object;
assume x in TL;
then ex tsg being Element of FinTrees the carrier of G st ( x =
PreTraversal tsg)&( tsg in TS G)&( tsg.{} = nt);
hence thesis by FINSEQ_1:def 11;
end;
hence thesis;
end;
func PostTraversalLanguage nt -> Subset of (the carrier of G)* equals
{ PostTraversal tsg where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
coherence
proof
set TL = { PostTraversal tsg
where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
TL c= (the carrier of G)*
proof
let x be object;
assume x in TL;
then ex tsg being Element of FinTrees the carrier of G st ( x =
PostTraversal tsg)&( tsg in TS G)&( tsg.{} = nt);
hence thesis by FINSEQ_1:def 11;
end;
hence thesis;
end;
end;
theorem Th13:
for t being DecoratedTree of the carrier of PeanoNat
st t in TS PeanoNat holds TerminalString t = <*0*>
proof
consider f being Function of (TS PN), (Terminals PN)* such that
A1: TerminalString root-tree (O qua Symbol of PN) = f.(root-tree O) and
A2: for t being Symbol of PN st t in Terminals PN holds f.(root-tree t)
= <*t*> and
A3: for nt being Symbol of PN, ts being FinSequence of TS(PN) st nt ==>
roots ts holds f.(nt-tree ts) = FlattenSeq(f * ts)
by Def11;
defpred P[DecoratedTree of the carrier of PN] means
TerminalString $1 = <*0*>;
A4: now
let s be Symbol of PN;
assume s in Terminals PN;
then s = O by Lm10,TARSKI:def 1;
hence P[root-tree s] by A1,A2;
end;
A5: now
let nt be Symbol of PN, ts be FinSequence of TS PN;
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
A8: nt-tree ts in TS PN by A6,Def1;
roots ts = <*O*> or roots ts = <*1*> by A6,Def2;
then len roots ts = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PN such that
A9: ts = <*x*> and
A10: x in TS PN by Th5;
reconsider x9 = x as Element of TS PN by A10;
rng ts = {x} by A9,FINSEQ_1:39;
then
A11: x in rng ts by TARSKI:def 1;
f.x9 is Element of (Terminals PN)*;
then
A12: f.x9 = TerminalString x by A2,A3,Def11
.= <*O*> by A7,A11;
f * ts = <*f.x*> by A9,FINSEQ_2:35;
then f.(nt-tree ts) = FlattenSeq(<*f.x9*>) by A3,A6
.= <*O*> by A12,PRE_POLY:1;
hence P[nt-tree ts] by A2,A3,A8,Def11;
end;
thus for t being DecoratedTree of the carrier of PN
st t in TS PN holds P[t] from DTConstrInd(A4,A5);
end;
theorem
for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}
proof
let nt be Symbol of PeanoNat;
A1: nt = S or nt = O by Lm2,TARSKI:def 2;
hereby
let x be object;
assume x in TerminalLanguage nt;
then ex tsg being Element of FinTrees the carrier of PN st
x = TerminalString tsg & tsg in TS PN & tsg.{} = nt;
then x = <*O*> by Th13;
hence x in {<*0*>} by TARSKI:def 1;
end;
let x be object;
assume x in {<*0*>};
then
A2: x = <*O*> by TARSKI:def 1;
reconsider prtO = root-tree O as Element of (TS PN) qua non empty set;
reconsider rtO = root-tree O as Element of TS PN;
reconsider srtO = <*prtO*> as FinSequence of TS PN;
A3: rtO.{} = O by TREES_4:3;
then S ==> roots <*rtO*> by Lm5,Th4;
then
A4: S-tree <*prtO*> in TS PN by Def1;
then
A5: TerminalString (S-tree srtO) = x by A2,Th13;
A6: (S-tree <*rtO*>).{} = S by TREES_4:def 4;
TerminalString rtO = x by A2,Th13;
hence thesis by A1,A3,A4,A5,A6;
end;
theorem Th15:
for t being Element of TS PeanoNat
holds PreTraversal t = ((height dom t) |-> 1)^<*0*>
proof
consider f being Function of (TS PN), (the carrier of PN)* such that
A1: PreTraversal root-tree (O qua Symbol of PN) = f.(root-tree O) and
A2: for t being Symbol of PN st t in Terminals PN holds f.(root-tree t)
= <*t*> and
A3: for nt being Symbol of PN, ts being FinSequence of TS(PN), rts
being FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (
the carrier of PN)* st x = f * ts holds f.(nt-tree ts) = <*nt*>^FlattenSeq(x)
by Def12;
reconsider rtO = root-tree O as Element of TS PN;
defpred P[DecoratedTree of the carrier of PN] means
ex t being Element of TS PN st $1 = t &
PreTraversal t = ((height dom t) |-> 1)^<*0*>;
A4: now
let s be Symbol of PN;
assume
A5: s in Terminals PN;
thus P[root-tree s]
proof
take t = rtO;
thus root-tree s = t by A5,Lm10,TARSKI:def 1;
thus PreTraversal t = <*O*> by A1,A2
.= {}^<*O*> by FINSEQ_1:34
.= (0 |-> 1)^<*0*>
.= ((height dom t) |-> 1)^<*0*> by TREES_1:42,TREES_4:3;
end;
end;
A6: now
let nt be Symbol of PN, ts be FinSequence of TS PN;
assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
reconsider t9 = nt-tree ts as Element of TS PN by A7,Def1;
A9: nt = S by A7,Def2;
roots ts = <*O*> or roots ts = <*1*> by A7,Def2;
then len roots ts = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PN such that
A10: ts = <*x*> and
A11: x in TS PN by Th5;
reconsider x9 = x as Element of TS PN by A11;
rng ts = {x} by A10,FINSEQ_1:39;
then x in rng ts by TARSKI:def 1;
then
A12: ex t9 being Element of TS PN st
x = t9 & PreTraversal t9 = ((height dom t9) |-> 1)^<*0*> by A8;
f.x9 is Element of (the carrier of PN)*;
then
A13: f.x9 = ((height dom x9) |-> 1)^<*0*> by A2,A3,A12,Def12;
f * ts = <*f.x*> by A10,FINSEQ_2:35;
then
A14: f.(nt-tree ts) = <*nt*>^FlattenSeq(<*f.x9*>) by A3,A7
.= <*nt*>^(((height dom x9) |-> 1)^<*0*>) by A13,PRE_POLY:1
.= <*nt*>^((height dom x9) |-> 1)^<*0*> by FINSEQ_1:32
.= (1|->1)^((height dom x9) |-> 1)^<*0*> by A9,FINSEQ_2:59
.= (((height dom x9)+1) |-> 1)^<*0*> by FINSEQ_2:123
.= ((height ^dom x9) |-> 1)^<*0*> by TREES_3:80;
A15: dom (nt-tree x9) = ^dom x9 by TREES_4:13;
A16: t9 = nt-tree x9 by A10,TREES_4:def 5;
f.t9 is Element of (the carrier of PN)*;
then PreTraversal(nt-tree ts) = f.(nt-tree ts) by A2,A3,Def12;
hence P[nt-tree ts] by A14,A15,A16;
end;
A17: for t being DecoratedTree of the carrier of PN
st t in TS PN holds P[t] from DTConstrInd(A4,A6);
let t be Element of TS PeanoNat;
P[t] by A17;
hence thesis;
end;
theorem
for nt being Symbol of PeanoNat holds
(nt = 0 implies PreTraversalLanguage nt = {<*0*>}) &
(nt = 1 implies PreTraversalLanguage nt = { (n|->1)^<*0*>
where n is Element of NAT : n <> 0 })
proof
let nt be Symbol of PeanoNat;
reconsider rtO = root-tree O as Element of TS PN;
height dom root-tree 0 = 0 by TREES_1:42,TREES_4:3;
then PreTraversal rtO = (0 |-> 1)^<*O*> by Th15;
then
A1: PreTraversal rtO = {}^<*O*> .= <*O*> by FINSEQ_1:34;
thus nt = 0 implies PreTraversalLanguage nt = {<*0*>}
proof
assume
A2: nt = 0;
hereby
let x be object;
assume x in PreTraversalLanguage nt;
then consider tsg being Element of FinTrees the carrier of PN such that
A3: x = PreTraversal tsg and
A4: tsg in TS PN and
A5: tsg.{} = O by A2;
tsg = root-tree O by A4,A5,Th9;
hence x in {<*0*>} by A1,A3,TARSKI:def 1;
end;
let x be object;
assume x in {<*0*>};
then
A6: x = <*O*> by TARSKI:def 1;
rtO.{} = O by TREES_4:3;
hence thesis by A1,A2,A6;
end;
assume
A7: nt = 1;
hereby
let x be object;
assume x in PreTraversalLanguage nt;
then consider tsg being Element of FinTrees the carrier of PN such that
A8: x = PreTraversal tsg and
A9: tsg in TS PN and
A10: tsg.{} = S by A7;
consider ts being FinSequence of TS PN such that
A11: tsg = S-tree ts and
A12: S ==> roots ts by A9,A10,Th10;
roots ts = <*0*> or roots ts = <*1*> by A12,Def2;
then len roots ts = 1 by FINSEQ_1:40;
then consider t being Element of FinTrees the carrier of PN such that
A13: ts = <*t*> and t in TS PN by Th5;
tsg = S-tree t by A11,A13,TREES_4:def 5;
then dom tsg = ^dom t by TREES_4:13;
then
A14: height dom tsg = (height dom t) + 1 by TREES_3:80;
x=((height dom tsg)|->1)^<*0*> by A8,A9,Th15;
hence x in { (n|->1)^<*0*> where n is Element of NAT : n <> 0 } by A14;
end;
let x be object;
assume x in { (n|->1)^<*0*> where n is Element of NAT : n <> 0 };
then consider n being Element of NAT such that
A15: x = (n |-> 1)^<*0*> and
A16: n <> 0;
defpred P[Nat] means
$1 <> 0 implies ex tsg being Element of TS PN st
tsg.{} = S & PreTraversal tsg = ($1|->1)^<*0*>;
A17: P[0];
A18: now
let n be Nat;
assume
A19: P[n];
thus P[n+1]
proof
assume n+1 <> 0;
per cases;
suppose n <> 0;
then consider tsg being Element of TS PN such that
tsg.{} = S and
A20: PreTraversal tsg = (n|->1)^<*0*> by A19;
PreTraversal tsg = ((height dom tsg) |-> 1)^<*0*> by Th15;
then
A21: n |-> 1 = (height dom tsg) |-> 1 by A20,FINSEQ_1:33;
len(n |-> 1) = n by CARD_1:def 7;
then
A22: height dom tsg = n by A21,CARD_1:def 7;
take tsg9 = S-tree tsg;
A23: tsg9 = S-tree <*tsg*> by TREES_4:def 5;
height dom tsg9 = height ^dom tsg by TREES_4:13
.= n+1 by A22,TREES_3:80;
hence thesis by A23,Th15,TREES_4:def 4;
end;
suppose
A24: n = 0;
take tsg9 = S-tree rtO;
A25: tsg9 = S-tree <*rtO*> by TREES_4:def 5;
height dom tsg9 = height ^dom rtO by TREES_4:13
.= (height dom rtO)+1 by TREES_3:80
.= n+1 by A24,TREES_1:42,TREES_4:3;
hence thesis by A25,Th15,TREES_4:def 4;
end;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A17, A18);
then ex tsg being Element of TS PN st
tsg.{} = S & PreTraversal tsg = (n|->1)^<*0*> by A16;
hence thesis by A7,A15;
end;
theorem Th17:
for t being Element of TS PeanoNat
holds PostTraversal t = <*0*>^((height dom t) |-> 1)
proof
consider f being Function of (TS PN), (the carrier of PN)* such that
A1: PostTraversal root-tree (O qua Symbol of PN) = f.(root-tree O) and
A2: for t being Symbol of PN st t in Terminals PN holds f.(root-tree t)
= <*t*> and
A3: for nt being Symbol of PN, ts being FinSequence of TS(PN), rts
being FinSequence st rts = roots ts & nt ==> rts for x being FinSequence of (
the carrier of PN)* st x = f * ts holds f.(nt-tree ts) = FlattenSeq(x)^<*nt*>
by Def13;
reconsider rtO = root-tree O as Element of TS PN;
defpred P[DecoratedTree of the carrier of PN] means
ex t being Element of TS PN st $1 = t &
PostTraversal t = <*0*>^((height dom t) |-> 1);
A4: now
let s be Symbol of PN;
assume
A5: s in Terminals PN;
thus P[root-tree s]
proof
take t = rtO;
thus root-tree s = t by A5,Lm10,TARSKI:def 1;
thus PostTraversal t = <*O*> by A1,A2
.= <*O*>^{} by FINSEQ_1:34
.= <*0*>^(0 |-> 1)
.= <*0*>^((height dom t) |-> 1) by TREES_1:42,TREES_4:3;
end;
end;
A6: now
let nt be Symbol of PN, ts be FinSequence of TS PN;
assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PN st t in rng ts holds P[t];
reconsider t9 = nt-tree ts as Element of TS PN by A7,Def1;
A9: nt = S by A7,Def2;
roots ts = <*O*> or roots ts = <*1*> by A7,Def2;
then len roots ts = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PN such that
A10: ts = <*x*> and
A11: x in TS PN by Th5;
reconsider x9 = x as Element of TS PN by A11;
rng ts = {x} by A10,FINSEQ_1:39;
then x in rng ts by TARSKI:def 1;
then
A12: ex t9 being Element of TS PN st
x=t9 & PostTraversal t9 = <*O*>^((height dom t9) |-> 1) by A8;
f.x9 is Element of (the carrier of PN)*;
then
A13: f.x9 = <*O*>^((height dom x9) |-> 1) by A2,A3,A12,Def13;
f * ts = <*f.x*> by A10,FINSEQ_2:35;
then
A14: f.(nt-tree ts) = FlattenSeq(<*f.x9*>)^<*nt*> by A3,A7
.= <*O*>^((height dom x9) |-> 1)^<*nt*> by A13,PRE_POLY:1
.= <*O*>^(((height dom x9) |-> 1)^<*nt*>) by FINSEQ_1:32
.= <*O*>^(((height dom x9)|->1)^(1|->1)) by A9,FINSEQ_2:59
.= <*O*>^(((height dom x9)+1) |-> 1) by FINSEQ_2:123
.= <*O*>^((height ^dom x9) |-> 1) by TREES_3:80;
A15: dom (nt-tree x9) = ^dom x9 by TREES_4:13;
A16: t9 = nt-tree x9 by A10,TREES_4:def 5;
f.t9 is Element of (the carrier of PN)*;
then PostTraversal(nt-tree ts) = f.(nt-tree ts) by A2,A3,Def13;
hence P[nt-tree ts] by A14,A15,A16;
end;
A17: for t being DecoratedTree of the carrier of PN
st t in TS PN holds P[t] from DTConstrInd(A4,A6);
let t be Element of TS PeanoNat;
P[t] by A17;
hence thesis;
end;
theorem
for nt being Symbol of PeanoNat holds
(nt = 0 implies PostTraversalLanguage nt = {<*0*>}) &
(nt = 1 implies PostTraversalLanguage nt = { <*0*>^(n|->1)
where n is Element of NAT : n <> 0 })
proof
let nt be Symbol of PeanoNat;
reconsider rtO = root-tree O as Element of TS PN;
height dom root-tree 0 = 0 by TREES_1:42,TREES_4:3;
then PostTraversal rtO = <*0*>^(0 |-> 1) by Th17;
then
A1: PostTraversal rtO = <*O*>^{} .= <*O*> by FINSEQ_1:34;
thus nt = 0 implies PostTraversalLanguage nt = {<*0*>}
proof
assume
A2: nt = 0;
hereby
let x be object;
assume x in PostTraversalLanguage nt;
then consider tsg being Element of FinTrees the carrier of PN such that
A3: x = PostTraversal tsg and
A4: tsg in TS PN and
A5: tsg.{} = O by A2;
tsg = root-tree O by A4,A5,Th9;
hence x in {<*0*>} by A1,A3,TARSKI:def 1;
end;
let x be object;
assume x in {<*0*>};
then
A6: x = <*O*> by TARSKI:def 1;
rtO.{} = O by TREES_4:3;
hence thesis by A1,A2,A6;
end;
assume
A7: nt = 1;
hereby
let x be object;
assume x in PostTraversalLanguage nt;
then consider tsg being Element of FinTrees the carrier of PN such that
A8: x = PostTraversal tsg and
A9: tsg in TS PN and
A10: tsg.{} = S by A7;
consider ts being FinSequence of TS PN such that
A11: tsg = S-tree ts and
A12: S ==> roots ts by A9,A10,Th10;
roots ts = <*0*> or roots ts = <*1*> by A12,Def2;
then len roots ts = 1 by FINSEQ_1:40;
then consider t being Element of FinTrees the carrier of PN such that
A13: ts = <*t*> and t in TS PN by Th5;
tsg = S-tree t by A11,A13,TREES_4:def 5;
then dom tsg = ^dom t by TREES_4:13;
then
A14: height dom tsg = (height dom t) + 1 by TREES_3:80;
x=<*0*>^((height dom tsg)|->1) by A8,A9,Th17;
hence x in { <*0*>^(n|->1) where n is Element of NAT : n <> 0 } by A14;
end;
let x be object;
assume x in { <*0*>^(n|->1) where n is Element of NAT : n <> 0 };
then consider n being Element of NAT such that
A15: x = <*0*>^(n |-> 1) and
A16: n <> 0;
defpred P[Nat] means
$1 <> 0 implies ex tsg being Element of TS PN st
tsg.{} = S & PostTraversal tsg = <*0*>^($1|->1);
A17: P[0];
A18: now
let n be Nat;
assume
A19: P[n];
thus P[n+1]
proof
assume n+1 <> 0;
per cases;
suppose n <> 0;
then consider tsg being Element of TS PN such that
tsg.{} = S and
A20: PostTraversal tsg = <*0*>^(n|->1) by A19;
PostTraversal tsg = <*0*>^((height dom tsg) |-> 1) by Th17;
then
A21: n |-> 1 = (height dom tsg) |-> 1 by A20,FINSEQ_1:33;
len(n |-> 1) = n by CARD_1:def 7;
then
A22: height dom tsg = n by A21,CARD_1:def 7;
take tsg9 = S-tree tsg;
A23: tsg9 = S-tree <*tsg*> by TREES_4:def 5;
height dom tsg9 = height ^dom tsg by TREES_4:13
.= n+1 by A22,TREES_3:80;
hence thesis by A23,Th17,TREES_4:def 4;
end;
suppose
A24: n = 0;
take tsg9 = S-tree rtO;
A25: tsg9 = S-tree <*rtO*> by TREES_4:def 5;
height dom tsg9 = height ^dom rtO by TREES_4:13
.= (height dom rtO)+1 by TREES_3:80
.= n+1 by A24,TREES_1:42,TREES_4:3;
hence thesis by A25,Th17,TREES_4:def 4;
end;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A17, A18);
then ex tsg being Element of TS PN st
tsg.{} = S & PostTraversal tsg = <*0*>^(n|->1) by A16;
hence thesis by A7,A15;
end;
:: What remains to be done, but in another article:
::
:: - partial trees (grown from the root towards the leaves)
:: - phrases