:: On Defining Functions on Binary Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 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, XBOOLE_0, TREES_2, SUBSET_1, FUNCT_1, TREES_4, TREES_3,
FINSEQ_1, TREES_1, ORDINAL1, ORDINAL4, CARD_1, XXREAL_0, ARYTM_3,
FINSET_1, RELAT_1, TARSKI, TREES_A, LANG1, TDGROUP, DTCONSTR, STRUCT_0,
ZFMISC_1, FUNCT_2, BINTREE1, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
NAT_1, RELAT_1, STRUCT_0, MCART_1, DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2,
FINSEQ_1, FINSET_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR,
PRE_POLY, XXREAL_0;
constructors DOMAIN_1, FINSEQOP, DTCONSTR, RELSET_1, PRE_POLY, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, MEMBERED, FINSEQ_1,
TREES_2, TREES_3, STRUCT_0, DTCONSTR, FINSET_1, TREES_4, TREES_1,
RELSET_1, XXREAL_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions DTCONSTR;
theorems TARSKI, NAT_1, ZFMISC_1, ENUMSET1, RELSET_1, FUNCT_1, FUNCT_2,
FINSEQ_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR, FINSET_1,
XTUPLE_0;
schemes FUNCT_2, DTCONSTR, MULTOP_1;
begin
definition
let D be non empty set, t be DecoratedTree of D;
func root-label t -> Element of D equals
t.{};
coherence
proof
reconsider r = {} as Node of t by TREES_1:22;
t.r is Element of D;
hence thesis;
end;
end;
theorem
for D being non empty set, t being DecoratedTree of D holds roots <*t
*> = <*root-label t*> by DTCONSTR:4;
theorem
for D being non empty set, t1, t2 being DecoratedTree of D holds roots
<*t1, t2*> = <*root-label t1, root-label t2*> by DTCONSTR:6;
definition
let IT be Tree;
attr IT is binary means
for t being Element of IT st not t in Leaves
IT holds succ t = { t^<*0*>, t^<*1*> };
end;
theorem :: LeavesDef3:
for T being Tree, t being Element of T holds succ t = {} iff t in Leaves T
proof
let T be Tree, t be Element of T;
hereby
assume succ t = {};
then not t^<*0*> in {t^<*n*> where n is Nat:t^<*n*> in T } by
TREES_2:def 5;
then not t^<*0*> in T;
hence t in Leaves T by TREES_1:54;
end;
set x = the Element of succ t;
assume t in Leaves T;
then
A1: not t^<*0*> in T by TREES_1:54;
assume succ t <> {};
then x in succ t;
then x in { t^<*n*> where n is Nat : t^<*n*> in T} by
TREES_2:def 5;
then consider n being Nat such that
x = t^<*n*> and
A2: t^<*n*> in T;
0 <= n by NAT_1:2;
hence contradiction by A1,A2,TREES_1:def 3;
end;
registration
cluster elementary_tree 0 -> binary;
coherence
proof
set T = elementary_tree 0;
let t be Element of T;
now
let s be FinSequence of NAT;
assume s in T;
then s = {} by TARSKI:def 1,TREES_1:29;
hence not t is_a_proper_prefix_of s by TARSKI:def 1,TREES_1:29;
end;
hence thesis by TREES_1:def 5;
end;
cluster elementary_tree 2 -> binary;
coherence
proof
set T = elementary_tree 2;
let t be Element of T;
assume
A1: not t in Leaves T;
per cases by ENUMSET1:def 1,TREES_1:53;
suppose
A2: t = {};
A3: for x being object holds x in { t^<*n*> where n is Nat : t^<*n
*> in T} iff x in {t^<*0*>,t^<*1*>}
proof
let x be object;
hereby
assume x in { t^<*n*> where n is Nat : t^<*n*> in T};
then
A4: ex n being Nat st x = t^<*n*> & t^<*n*> in T;
then reconsider x9 = x as FinSequence;
per cases by A4,ENUMSET1:def 1,TREES_1:53;
suppose
x = {};
hence x in {t^<*0*>,t^<*1*>} by A4;
end;
suppose
x = <*0*>;
then x9 = t^<*0*> by A2,FINSEQ_1:34;
hence x in {t^<*0*>,t^<*1*>} by TARSKI:def 2;
end;
suppose
x = <*1*>;
then x9 = t^<*1*> by A2,FINSEQ_1:34;
hence x in {t^<*0*>,t^<*1*>} by TARSKI:def 2;
end;
end;
assume
A5: x in {t^<*0*>,t^<*1*>};
then reconsider x9 = x as FinSequence by TARSKI:def 2;
A6: x = t^<*0*> or x = t^<*1*> by A5,TARSKI:def 2;
then x9 = <*0*> or x9 = <*1*> by A2,FINSEQ_1:34;
then x9 in T by ENUMSET1:def 1,TREES_1:53;
hence thesis by A6;
end;
succ t = { t^<*n*> where n is Nat : t^<*n*> in T} by
TREES_2:def 5;
hence thesis by A3,TARSKI:2;
end;
suppose
A7: t = <*0*>;
now
assume
A8: t^<*0*> in T;
per cases by A8,ENUMSET1:def 1,TREES_1:53;
suppose
t^<*0*> = {};
hence contradiction;
end;
suppose
t^<*0*> = <*0*>;
then len <*0*> + len <*0*> = len <*0*> by A7,FINSEQ_1:22;
hence contradiction by FINSEQ_1:39;
end;
suppose
t^<*0*> = <*1*>;
then len <*0*> + len <*0*> = len <*1*> by A7,FINSEQ_1:22;
then 1 + len <*0*> = len <*1*> by FINSEQ_1:39;
then 1 + 1 = len <*1*> by FINSEQ_1:39;
hence contradiction by FINSEQ_1:39;
end;
end;
hence thesis by A1,TREES_1:54;
end;
suppose
A9: t = <*1*>;
now
assume
A10: t^<*0*> in T;
per cases by A10,ENUMSET1:def 1,TREES_1:53;
suppose
t^<*0*> = {};
hence contradiction;
end;
suppose
t^<*0*> = <*0*>;
then len <*1*> + len <*0*> = len <*0*> by A9,FINSEQ_1:22;
hence contradiction by FINSEQ_1:39;
end;
suppose
t^<*0*> = <*1*>;
then len <*1*> + len <*0*> = len <*1*> by A9,FINSEQ_1:22;
hence contradiction by FINSEQ_1:39;
end;
end;
hence thesis by A1,TREES_1:54;
end;
end;
end;
theorem
elementary_tree 0 is binary;
theorem
elementary_tree 2 is binary;
registration
cluster binary finite for Tree;
existence
proof
take elementary_tree 0;
thus thesis;
end;
end;
definition
let IT be DecoratedTree;
attr IT is binary means
:Def3:
dom IT is binary;
end;
registration
let D be non empty set;
cluster binary finite for DecoratedTree of D;
existence
proof
set t = the binary finite Tree;
set T = the Function of t, D;
reconsider T as DecoratedTree of D;
take T;
thus dom T is binary & T is finite by FUNCT_2:def 1;
end;
end;
registration
cluster binary finite for DecoratedTree;
existence
proof
set t = the binary finite DecoratedTree of {{}};
take t;
thus thesis;
end;
end;
registration
cluster binary -> finite-order for Tree;
coherence
proof
let T be Tree;
assume
A1: T is binary;
now
let t be Element of T;
assume
A2: t^<*2*> in T;
then
A3: t^<*0*> in T by TREES_1:def 3;
per cases;
suppose
t in Leaves T;
hence contradiction by A3,TREES_1:54;
end;
suppose
A4: not t in Leaves T;
A5: now
A6: <*2*>.1 = 2;
assume <*2*> = <*0*>;
hence contradiction by A6,FINSEQ_1:40;
end;
A7: now
A8: <*2*>.1 = 2;
assume <*2*> = <*1*>;
hence contradiction by A8,FINSEQ_1:40;
end;
t^<*2*> in { t^<*n*> where n is Nat : t^<*n*> in T } by A2;
then
A9: t^<*2*> in succ t by TREES_2:def 5;
succ t = { t^<*0*>, t^<*1*> } by A1,A4;
then t^<*2*> = t^<*0*> or t^<*2*> = t^<*1*> by A9,TARSKI:def 2;
hence contradiction by A5,A7,FINSEQ_1:33;
end;
end;
hence thesis by TREES_2:def 2;
end;
end;
theorem Th6:
for T0,T1 being Tree, t being Element of tree(T0,T1) holds (for p
being Element of T0 st t = <*0*>^p holds t in Leaves tree(T0,T1) iff p in
Leaves T0) & for p being Element of T1 st t = <*1*>^p holds t in Leaves tree(T0
,T1) iff p in Leaves T1
proof
let T0,T1 be Tree, t be Element of tree(T0,T1);
set RT = tree(T0,T1);
hereby
let p be Element of T0;
assume
A1: t = <*0*>^p;
hereby
assume
A2: t in Leaves RT;
assume not p in Leaves T0;
then consider n being Nat such that
A3: p^<*n*> in T0 by TREES_1:55;
<*0*>^(p^<*n*>) in RT by A3,TREES_3:69;
then (<*0*>^p)^<*n*> in RT by FINSEQ_1:32;
hence contradiction by A1,A2,TREES_1:55;
end;
assume
A4: p in Leaves T0;
assume not t in Leaves RT;
then consider n being Nat such that
A5: t^<*n*> in RT by TREES_1:55;
<*0*>^(p^<*n*>) in RT by A1,A5,FINSEQ_1:32;
then p^<*n*> in T0 by TREES_3:69;
hence contradiction by A4,TREES_1:55;
end;
let p be Element of T1;
assume
A6: t = <*1*>^p;
hereby
assume
A7: t in Leaves RT;
assume not p in Leaves T1;
then consider n being Nat such that
A8: p^<*n*> in T1 by TREES_1:55;
<*1*>^(p^<*n*>) in RT by A8,TREES_3:70;
then (<*1*>^p)^<*n*> in RT by FINSEQ_1:32;
hence contradiction by A6,A7,TREES_1:55;
end;
assume
A9: p in Leaves T1;
assume not t in Leaves RT;
then consider n being Nat such that
A10: t^<*n*> in RT by TREES_1:55;
<*1*>^(p^<*n*>) in RT by A6,A10,FINSEQ_1:32;
then p^<*n*> in T1 by TREES_3:70;
hence contradiction by A9,TREES_1:55;
end;
theorem Th7:
for T0,T1 being Tree, t being Element of tree(T0,T1) holds (t =
{} implies succ t = { t^<*0*>, t^<*1*> }) & (for p being Element of T0 st t =
<*0*>^p for sp being FinSequence holds sp in succ p iff <*0*>^sp in succ t) &
for p being Element of T1 st t = <*1*>^p for sp being FinSequence holds sp in
succ p iff <*1*>^sp in succ t
proof
let T0,T1 be Tree, t be Element of tree(T0,T1);
set RT = tree(T0,T1);
hereby
assume
A1: t = {};
{} in T1 & <*1*> = <*1*>^{} by FINSEQ_1:34,TREES_1:22;
then <*1*> in RT by TREES_3:68;
then
A2: t^<*1*> in RT by A1,FINSEQ_1:34;
A3: succ t = { t^<*n*> where n is Nat:t^<*n*> in RT } by
TREES_2:def 5;
{} in T0 & <*0*> = <*0*>^{} by FINSEQ_1:34,TREES_1:22;
then <*0*> in RT by TREES_3:68;
then
A4: t^<*0*> in RT by A1,FINSEQ_1:34;
now
let x1 be object;
hereby
assume x1 in succ t;
then consider n being Nat such that
A5: x1 = t^<*n*> and
A6: t^<*n*> in RT by A3;
reconsider x = x1 as FinSequence by A5;
ex p being FinSequence st ( p in T0 & x = <*0*>^p or p in T1 & x =
<*1*>^p) by A5,A6,TREES_3:68;
then
A7: x.1 = 0 or x.1 = 1 by FINSEQ_1:41;
x1 = <*n*> by A1,A5,FINSEQ_1:34;
then x = <*0*> or x = <*1*> by A7;
then x = t^<*0*> or x = t^<*1*> by A1,FINSEQ_1:34;
hence x1 in { t^<*0*>, t^<*1*> } by TARSKI:def 2;
end;
assume x1 in { t^<*0*>, t^<*1*> };
then x1 = t^<*0*> or x1 = t^<*1*> by TARSKI:def 2;
hence x1 in succ t by A3,A4,A2;
end;
hence succ t = { t^<*0*>, t^<*1*> } by TARSKI:2;
end;
hereby
let p be Element of T0 such that
A8: t = <*0*>^p;
let sp be FinSequence;
hereby
assume sp in succ p;
then sp in { p^<*n*> where n is Nat : p^<*n*> in T0 } by
TREES_2:def 5;
then consider n being Nat such that
A9: sp = p^<*n*> and
A10: p^<*n*> in T0;
<*0*>^(p^<*n*>) in RT by A10,TREES_3:69;
then (<*0*>^p)^<*n*> in RT by FINSEQ_1:32;
then t^<*n*> in {t^<*k*> where k is Nat : t^<*k*> in RT} by A8;
then t^<*n*> in succ t by TREES_2:def 5;
hence <*0*>^sp in succ t by A8,A9,FINSEQ_1:32;
end;
set zsp = <*0*>^sp;
assume zsp in succ t;
then zsp in {t^<*n*> where n is Nat:t^<*n*> in RT} by
TREES_2:def 5;
then consider n being Nat such that
A11: zsp = t^<*n*> and
A12: t^<*n*> in RT;
<*0*>^(p^<*n*>) in RT by A8,A12,FINSEQ_1:32;
then p^<*n*> in T0 by TREES_3:69;
then p^<*n*> in { p^<*k*> where k is Nat : p^<*k*> in T0 };
then
A13: p^<*n*> in succ p by TREES_2:def 5;
<*0*>^sp = <*0*>^(p^<*n*>) by A8,A11,FINSEQ_1:32;
hence sp in succ p by A13,FINSEQ_1:33;
end;
let p be Element of T1 such that
A14: t = <*1*>^p;
let sp be FinSequence;
hereby
assume sp in succ p;
then sp in { p^<*n*> where n is Nat : p^<*n*> in T1 } by
TREES_2:def 5;
then consider n being Nat such that
A15: sp = p^<*n*> and
A16: p^<*n*> in T1;
<*1*>^(p^<*n*>) in RT by A16,TREES_3:70;
then (<*1*>^p)^<*n*> in RT by FINSEQ_1:32;
then
t^<*n*> in {t^<*k*> where k is Nat : t^<*k*> in RT} by A14;
then t^<*n*> in succ t by TREES_2:def 5;
hence <*1*>^sp in succ t by A14,A15,FINSEQ_1:32;
end;
set zsp = <*1*>^sp;
assume zsp in succ t;
then zsp in {t^<*n*> where n is Nat:t^<*n*> in RT} by
TREES_2:def 5;
then consider n being Nat such that
A17: zsp = t^<*n*> and
A18: t^<*n*> in RT;
<*1*>^(p^<*n*>) in RT by A14,A18,FINSEQ_1:32;
then p^<*n*> in T1 by TREES_3:70;
then p^<*n*> in { p^<*k*> where k is Nat : p^<*k*> in T1 };
then
A19: p^<*n*> in succ p by TREES_2:def 5;
<*1*>^sp = <*1*>^(p^<*n*>) by A14,A17,FINSEQ_1:32;
hence thesis by A19,FINSEQ_1:33;
end;
theorem Th8:
for T1,T2 being Tree holds T1 is binary & T2 is binary iff tree(
T1,T2) is binary
proof
let T1,T2 be Tree;
set RT = tree(T1,T2);
hereby
assume that
A1: T1 is binary and
A2: T2 is binary;
now
let t be Element of RT;
assume
A3: not t in Leaves RT;
per cases by TREES_3:68;
suppose
t = {};
hence succ t = { t^<*0*>, t^<*1*> } by Th7;
end;
suppose
ex p being FinSequence st p in T1 & t = <*0*>^p or p in T2 & t
= <*1*>^p;
then consider p being FinSequence such that
A4: p in T1 & t = <*0*>^p or p in T2 & t = <*1*>^p;
A5: now
assume that
A6: p in T2 and
A7: t = <*1*>^p;
reconsider p as Element of T2 by A6;
per cases;
suppose
p in Leaves T2;
hence succ t = { t^<*0*>, t^<*1*> } by A3,A7,Th6;
end;
suppose
not p in Leaves T2;
then
A8: succ p = { p^<*0*>, p^<*1*> } by A2;
now
let x be object;
hereby
assume
A9: x in succ t;
then x in { t^<*n*> where n is Nat : t^<*n*> in RT
} by TREES_2:def 5;
then consider n being Nat such that
A10: x = t^<*n*> and
A11: t^<*n*> in RT;
A12: x = <*1*>^(p^<*n*>) by A7,A10,FINSEQ_1:32;
then reconsider pn = p^<*n*> as Element of T2 by A10,A11,
TREES_3:70;
pn in succ p by A7,A9,A12,Th7;
then pn = p^<*0*> or pn = p^<*1*> by A8,TARSKI:def 2;
then x = t^<*0*> or x = t^<*1*> by A10,FINSEQ_1:33;
hence x in { t^<*0*>, t^<*1*> } by TARSKI:def 2;
end;
assume x in { t^<*0*>, t^<*1*> };
then x = <*1*>^p^<*0*> or x = <*1*>^p^<*1*> by A7,TARSKI:def 2;
then
A13: x = <*1*>^(p^<*0*>) or x = <*1*>^(p^<*1*>) by FINSEQ_1:32;
p^<*0*> in succ p & p^<*1*> in succ p by A8,TARSKI:def 2;
hence x in succ t by A7,A13,Th7;
end;
hence succ t = { t^<*0*>, t^<*1*> } by TARSKI:2;
end;
end;
now
assume that
A14: p in T1 and
A15: t = <*0*>^p;
reconsider p as Element of T1 by A14;
per cases;
suppose
p in Leaves T1;
hence succ t = { t^<*0*>, t^<*1*> } by A3,A15,Th6;
end;
suppose
not p in Leaves T1;
then
A16: succ p = { p^<*0*>, p^<*1*> } by A1;
now
let x be object;
hereby
assume
A17: x in succ t;
then x in { t^<*n*> where n is Nat : t^<*n*> in RT
} by TREES_2:def 5;
then consider n being Nat such that
A18: x = t^<*n*> and
A19: t^<*n*> in RT;
A20: x = <*0*>^(p^<*n*>) by A15,A18,FINSEQ_1:32;
then reconsider pn = p^<*n*> as Element of T1 by A18,A19,
TREES_3:69;
pn in succ p by A15,A17,A20,Th7;
then pn = p^<*0*> or pn = p^<*1*> by A16,TARSKI:def 2;
then x = t^<*0*> or x = t^<*1*> by A18,FINSEQ_1:33;
hence x in { t^<*0*>, t^<*1*> } by TARSKI:def 2;
end;
assume x in { t^<*0*>, t^<*1*> };
then x = <*0*>^p^<*0*> or x = <*0*>^p^<*1*> by A15,TARSKI:def 2;
then
A21: x = <*0*>^(p^<*0*>) or x = <*0*>^(p^<*1*>) by FINSEQ_1:32;
p^<*0*> in succ p & p^<*1*> in succ p by A16,TARSKI:def 2;
hence x in succ t by A15,A21,Th7;
end;
hence succ t = { t^<*0*>, t^<*1*> } by TARSKI:2;
end;
end;
hence succ t = { t^<*0*>, t^<*1*> } by A4,A5;
end;
end;
hence tree(T1,T2) is binary;
end;
assume
A22: RT is binary;
now
let t be Element of T1;
reconsider zt = <*0*>^t as Element of RT by TREES_3:69;
assume not t in Leaves T1;
then not zt in Leaves RT by Th6;
then
A23: succ zt = { <*0*>^t^<*0*>, <*0*>^t^<*1*> } by A22;
A24: succ zt = {zt^<*n*> where n is Nat:zt^<*n*> in RT} by
TREES_2:def 5;
now
let x be object;
hereby
assume x in succ t;
then
x in { t^<*n*> where n is Nat : t^<*n*> in T1 } by TREES_2:def 5;
then consider n being Nat such that
A25: x = t^<*n*> and
A26: t^<*n*> in T1;
<*0*>^(t^<*n*>) in RT by A26,TREES_3:69;
then zt^<*n*> in RT by FINSEQ_1:32;
then zt^<*n*> in {zt^<*k*> where k is Nat:zt^<*k*> in RT};
then zt^<*n*> = zt^<*0*> or zt^<*n*> = zt^<*1*> by A23,A24,TARSKI:def 2
;
then x = t^<*0*> or x = t^<*1*> by A25,FINSEQ_1:33;
hence x in { t^<*0*>, t^<*1*> } by TARSKI:def 2;
end;
assume x in { t^<*0*>, t^<*1*> };
then
A27: x = t^<*0*> or x = t^<*1*> by TARSKI:def 2;
<*0*>^t^<*1*> in succ zt by A23,TARSKI:def 2;
then
A28: <*0*>^(t^<*1*>) in succ zt by FINSEQ_1:32;
<*0*>^t^<*0*> in succ zt by A23,TARSKI:def 2;
then <*0*>^(t^<*0*>) in succ zt by FINSEQ_1:32;
hence x in succ t by A27,A28,Th7;
end;
hence succ t = { t^<*0*>, t^<*1*> } by TARSKI:2;
end;
hence T1 is binary;
now
let t be Element of T2;
reconsider zt = <*1*>^t as Element of RT by TREES_3:70;
assume not t in Leaves T2;
then not zt in Leaves RT by Th6;
then
A29: succ zt = { <*1*>^t^<*0*>, <*1*>^t^<*1*> } by A22;
A30: succ zt = {zt^<*n*> where n is Nat:zt^<*n*> in RT} by
TREES_2:def 5;
now
let x be object;
hereby
assume x in succ t;
then
x in { t^<*n*> where n is Nat : t^<*n*> in T2 } by TREES_2:def 5;
then consider n being Nat such that
A31: x = t^<*n*> and
A32: t^<*n*> in T2;
<*1*>^(t^<*n*>) in RT by A32,TREES_3:70;
then zt^<*n*> in RT by FINSEQ_1:32;
then zt^<*n*> in {zt^<*k*> where k is Nat:zt^<*k*> in RT};
then zt^<*n*> = zt^<*0*> or zt^<*n*> = zt^<*1*> by A29,A30,TARSKI:def 2
;
then x = t^<*0*> or x = t^<*1*> by A31,FINSEQ_1:33;
hence x in { t^<*0*>, t^<*1*> } by TARSKI:def 2;
end;
assume x in { t^<*0*>, t^<*1*> };
then
A33: x = t^<*0*> or x = t^<*1*> by TARSKI:def 2;
<*1*>^t^<*1*> in succ zt by A29,TARSKI:def 2;
then
A34: <*1*>^(t^<*1*>) in succ zt by FINSEQ_1:32;
<*1*>^t^<*0*> in succ zt by A29,TARSKI:def 2;
then <*1*>^(t^<*0*>) in succ zt by FINSEQ_1:32;
hence x in succ t by A33,A34,Th7;
end;
hence succ t = { t^<*0*>, t^<*1*> } by TARSKI:2;
end;
hence thesis;
end;
theorem Th9:
for T1,T2 being DecoratedTree, x being set holds T1 is binary &
T2 is binary iff x-tree (T1,T2) is binary
proof
let T1,T2 be DecoratedTree, x be set;
hereby
assume T1 is binary & T2 is binary;
then dom T1 is binary & dom T2 is binary;
then
A1: tree(dom T1, dom T2) is binary by Th8;
dom (x-tree (T1, T2)) = tree(dom T1, dom T2) by TREES_4:14;
hence x-tree (T1,T2) is binary by A1;
end;
assume x-tree (T1,T2) is binary;
then
A2: dom (x-tree (T1,T2)) is binary;
dom (x-tree (T1, T2)) = tree(dom T1, dom T2) by TREES_4:14;
then dom T1 is binary & dom T2 is binary by A2,Th8;
hence thesis;
end;
registration
let D be non empty set, x be Element of D, T1, T2 be binary finite
DecoratedTree of D;
cluster x-tree (T1,T2) -> binary finite D-valued;
coherence
proof
set t1t2 = <*T1,T2*>;
dom T1 is finite;
then
A1: T1 in FinTrees D by TREES_3:def 8;
dom T2 is finite;
then
A2: T2 in FinTrees D by TREES_3:def 8;
rng <*T1, T2*> = rng (<*T1*>^<*T2*>) by FINSEQ_1:def 9
.= rng <*T1*> \/ rng <*T2*> by FINSEQ_1:31
.= {T1} \/ rng <*T2*> by FINSEQ_1:39
.= {T1} \/ {T2} by FINSEQ_1:39
.= {T1, T2} by ENUMSET1:1;
then for x being object st x in rng t1t2 holds x in FinTrees D by A1,A2,
TARSKI:def 2;
then rng t1t2 c= FinTrees D by TARSKI:def 3;
then reconsider T1T2 = t1t2 as FinSequence of FinTrees D by FINSEQ_1:def 4;
x-tree (T1, T2) = x-tree T1T2 by TREES_4:def 6;
then dom (x-tree (T1, T2)) is finite;
hence thesis by Th9,FINSET_1:10;
end;
end;
definition
let IT be non empty DTConstrStr;
attr IT is binary means
:Def4:
for s being Symbol of IT, p being FinSequence
st s ==> p ex x1, x2 being Symbol of IT st p = <* x1, x2 *>;
end;
registration
cluster binary with_terminals with_nonterminals with_useful_nonterminals
strict for non empty DTConstrStr;
existence
proof
reconsider 01 = {0,1} as non empty set;
reconsider a90 = 0, a91 = 1 as Element of 01 by TARSKI:def 2;
reconsider a9119 = <*a91*>^<*a91*> as Element of 01*;
reconsider P = {[a90,a9119]} as Relation of 01, 01*;
take cherry = DTConstrStr (# 01, P #);
reconsider a90, a91 as Symbol of cherry;
hereby
let s be Symbol of cherry, p be FinSequence;
assume
A1: s ==> p;
take x1 = a91, x2 = a91;
[s,p] in P by A1,LANG1:def 1;
then [s,p] = [0,a9119] by TARSKI:def 1;
then p = a9119 by XTUPLE_0:1
.= <*1,1*> by FINSEQ_1:def 9;
hence p = <*x1,x2*>;
end;
now
let s be FinSequence;
assume a91 ==> s;
then [1,s] in P by LANG1:def 1;
then [1,s] = [0,a9119] by TARSKI:def 1;
hence contradiction by XTUPLE_0:1;
end;
then
A2: a91 in {t where t is Symbol of cherry: not ex s being FinSequence st t
==> s};
then
A3: a91 in Terminals cherry by LANG1:def 2;
thus Terminals cherry <> {} by A2,LANG1:def 2;
[a90,a9119] in P by TARSKI:def 1;
then a90 ==> a9119 by LANG1:def 1;
then
a90 in {t where t is Symbol of cherry: ex s being FinSequence st t ==> s };
hence NonTerminals cherry <> {} by LANG1:def 3;
A4: {s where s is Symbol of cherry: ex p being FinSequence st s ==> p} =
NonTerminals cherry by LANG1:def 3;
hereby
reconsider X = TS cherry as non empty set by A3,DTCONSTR:def 1;
let nt be Symbol of cherry;
reconsider rt1 = root-tree a91 as Element of X by A3,DTCONSTR:def 1;
reconsider q = <*rt1*>^<*rt1*> as FinSequence of TS cherry;
q = <*root-tree 1, root-tree 1*> by FINSEQ_1:def 9;
then
A5: roots q = <*(root-tree a91).{}, (root-tree a91).{}*> by DTCONSTR:6;
assume nt in NonTerminals cherry;
then
ex s being Symbol of cherry st nt = s & ex p being FinSequence st s
==> p by A4;
then consider p being FinSequence such that
A6: nt ==> p;
take q9 = q;
[nt, p] in P by A6,LANG1:def 1;
then
A7: [nt, p] = [0, a9119] by TARSKI:def 1;
a9119 = <*1, 1*> & (root-tree 1).{} = 1 by FINSEQ_1:def 9,TREES_4:3;
hence nt ==> roots q9 by A6,A7,A5,XTUPLE_0:1;
end;
thus thesis;
end;
end;
scheme
BinDTConstrStrEx { S() -> non empty set, P[set, set, set] }: ex G be binary
strict non empty DTConstrStr st the carrier of G = S() & for x, y, z being
Symbol of G holds x ==> <*y,z*> iff P[x, y, z] proof
defpred Q[set, FinSequence] means P[$1, $2.1, $2.2] & $2 = <*$2.1, $2.2*>;
consider G being strict non empty DTConstrStr such that
A1: the carrier of G = S() and
A2: for x being Symbol of G, p being FinSequence of the carrier of G
holds x ==> p iff Q[x, p] from DTCONSTR:sch 1;
now
let s be Symbol of G, p be FinSequence;
assume
A3: s ==> p;
then [s,p] in the Rules of G by LANG1:def 1;
then p in (the carrier of G)* by ZFMISC_1:87;
then reconsider pp = p as FinSequence of the carrier of G
by FINSEQ_1:def 11;
pp = <*pp.1, pp.2*> by A2,A3;
then rng pp = rng (<*pp.1*>^<*pp.2*>) by FINSEQ_1:def 9
.= rng <*pp.1*> \/ rng <*pp.2*> by FINSEQ_1:31
.= {pp.1} \/ rng <*pp.2*> by FINSEQ_1:39
.= {pp.1} \/ {pp.2} by FINSEQ_1:39
.= {pp.1, pp.2} by ENUMSET1:1;
then pp.1 in rng pp & pp.2 in rng pp by TARSKI:def 2;
then reconsider pp1 = pp.1, pp2 = pp.2 as Symbol of G;
take pp1, pp2;
thus p = <*pp1, pp2*> by A2,A3;
end;
then
A4: G is binary;
now
let x, y, z be Symbol of G;
reconsider yz = <*y,z*> as FinSequence of the carrier of G;
yz.1 = y & yz.2 = z;
hence x ==> <*y,z*> iff P[x, y, z] by A2;
end;
hence thesis by A1,A4;
end;
theorem Th10:
for G being binary with_terminals with_nonterminals non empty
DTConstrStr, ts being FinSequence of TS G, nt being Symbol of G st nt ==>
roots ts holds nt is NonTerminal of G & dom ts = {1, 2} & 1 in dom ts & 2 in
dom ts & ex tl, tr being Element of TS G st roots ts = <*root-label tl,
root-label tr*> & tl = ts.1 & tr = ts.2 & nt-tree ts = nt-tree (tl, tr) & tl in
rng ts & tr in rng ts
proof
let G be binary with_terminals with_nonterminals non empty DTConstrStr, ts
be FinSequence of TS G, nt be Symbol of G;
assume
A1: nt ==> roots ts;
then consider rtl, rtr being Symbol of G such that
A2: roots ts = <* rtl, rtr *> by Def4;
nt in {s where s is Symbol of G:ex rts being FinSequence st s ==> rts} by A1;
hence nt is NonTerminal of G by LANG1:def 3;
A3: len <*rtl, rtr*> = 2 by FINSEQ_1:44;
A4: dom <*rtl, rtr*> = dom ts by A2,TREES_3:def 18;
hence dom ts = {1, 2} by A3,FINSEQ_1:2,def 3;
hence
A5: 1 in dom ts & 2 in dom ts by TARSKI:def 2;
then consider tl being DecoratedTree such that
A6: tl = ts.1 and
A7: <*rtl, rtr*>.1 = tl.{} by A2,TREES_3:def 18;
A8: rng ts c= TS G & tl in rng ts by A5,A6,FINSEQ_1:def 4,FUNCT_1:def 3;
consider tr being DecoratedTree such that
A9: tr = ts.2 and
A10: <*rtl, rtr*>.2 = tr.{} by A2,A5,TREES_3:def 18;
tr in rng ts by A5,A9,FUNCT_1:def 3;
then reconsider tl, tr as Element of TS(G) by A8;
take tl, tr;
thus roots ts = <*root-label tl, root-label tr*> by A2,A7,A10;
Seg len <*rtl, rtr*> = dom <*rtl, rtr*> by FINSEQ_1:def 3
.= Seg len ts by A4,FINSEQ_1:def 3;
then len ts = 2 by A3,FINSEQ_1:6;
then ts = <*tl, tr*> by A6,A9,FINSEQ_1:44;
hence tl = ts.1 & tr = ts.2 & nt-tree ts = nt-tree (tl, tr) by
TREES_4:def 6;
thus thesis by A5,A6,A9,FUNCT_1:def 3;
end;
scheme
BinDTConstrInd { G() -> binary with_terminals with_nonterminals non empty
DTConstrStr, P[set] }: for t being Element of TS(G()) holds P[t]
provided
A1: for s being Terminal of G() holds P[root-tree s] and
A2: for nt being NonTerminal of G(), tl, tr being Element of TS(G()) st
nt ==> <*root-label tl, root-label tr*> & P[tl] & P[tr] holds P[nt-tree(tl, tr)
]
proof
A3: 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
let nt be Symbol of G(), ts be FinSequence of TS(G()) such that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of G() st t in rng ts holds P[t];
A6: nt is NonTerminal of G() by A4,Th10;
consider tl, tr being Element of TS G() such that
A7: roots ts = <*root-label tl, root-label tr*> and
tl = ts.1 and
tr = ts.2 and
A8: nt-tree ts = nt-tree (tl, tr) and
A9: tl in rng ts & tr in rng ts by A4,Th10;
( P[tl])& P[tr] by A5,A9;
hence thesis by A2,A4,A6,A7,A8;
end;
A10: for s being Symbol of G() st s in Terminals G() holds P[root-tree s] by A1
;
for t being DecoratedTree of the carrier of G() st t in TS(G()) holds P
[t] from DTCONSTR:sch 7(A10, A3);
hence thesis;
end;
scheme
BinDTConstrIndDef { G() -> binary with_terminals with_nonterminals
with_useful_nonterminals non empty DTConstrStr, D()->non empty set, TermVal(
set) -> Element of D(), NTermVal(set, set, set, set, set) -> Element of D() }:
ex f being Function of TS(G()), D() st (for t being Terminal of G() holds f.(
root-tree t) = TermVal(t)) & for nt being NonTerminal of G(), tl, tr being
Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr =
root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f
.tl & xr = f.tr holds f.(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr)
proof
deffunc BNTV(Symbol of G(), FinSequence, FinSequence of D()) = NTermVal($1,
$2.1, $2.2, $3.1, $3.2);
consider f being Function of TS(G()), D() such that
A1: for t being Symbol of G() st t in Terminals G() holds f.(root-tree t
) = TermVal(t) and
A2: for nt being Symbol of G(), ts being FinSequence of TS(G()) st nt
==> roots ts holds f.(nt-tree ts) = BNTV(nt, roots ts, f * ts) from DTCONSTR:
sch 8;
take f;
thus for t be Terminal of G() holds f.(root-tree t) = TermVal(t) by A1;
let nt be NonTerminal of G(), tl, tr be Element of TS(G()), rtl, rtr be
Symbol of G();
assume that
A3: rtl = root-label tl and
A4: rtr = root-label tr and
A5: nt ==> <* rtl, rtr *>;
reconsider rts = <*rtl, rtr*> as FinSequence;
reconsider ts = <*tl, tr*> as FinSequence of TS G();
let xl, xr be Element of D();
A7: dom ts = {1, 2} by FINSEQ_1:2,89;
reconsider x = <*xl, xr*> as FinSequence of D();
A8: dom x = {1, 2} by FINSEQ_1:2,89;
A10: dom f = TS G() by FUNCT_2:def 1;
A11: now
let y be object;
A12: now
assume that
A13: y in dom ts and
ts.y in dom f;
per cases by A7,A13,TARSKI:def 2;
suppose
y = 1;
hence y in dom x by A8,TARSKI:def 2;
end;
suppose
y = 2;
hence y in dom x by A8,TARSKI:def 2;
end;
end;
now
assume
A14: y in dom x;
per cases by A8,A14,TARSKI:def 2;
suppose
y = 1;
hence y in dom ts & ts.y in dom f by A10,A7,TARSKI:def 2;
end;
suppose
y = 2;
hence y in dom ts & ts.y in dom f by A10,A7,TARSKI:def 2;
end;
end;
hence y in dom x iff y in dom ts & ts.y in dom f by A12;
end;
assume
A15: xl = f.tl & xr = f.tr;
now
let y be object;
assume y in dom x;
then y = 1 or y = 2 by A8,TARSKI:def 2;
hence x.y = f.(ts.y) by A15;
end;
then
A16: x = f * ts by A11,FUNCT_1:10;
A19: now
let i be Element of NAT;
assume i in dom ts;
then i in Seg len ts by FINSEQ_1:def 3;
then
A20: i in Seg 2 by FINSEQ_1:44;
per cases by A20,FINSEQ_1:2,TARSKI:def 2;
suppose
i = 1;
hence ex T being DecoratedTree st T = ts.i & rts.i = T.{} by A3;
end;
suppose
i = 2;
hence ex T being DecoratedTree st T = ts.i & rts.i = T.{} by A4;
end;
end;
dom rts = {1, 2} by FINSEQ_1:2,89;
then rts = roots ts by A7,A19,TREES_3:def 18;
then
A21: f.(nt-tree ts) = NTermVal(nt, rts.1, rts.2, x.1, x.2) by A2,A5,A16;
thus thesis by A21,TREES_4:def 6;
end;
scheme
BinDTConstrUniqDef { G() -> binary with_terminals with_nonterminals
with_useful_nonterminals non empty DTConstrStr, D()->non empty set, f1, f2()
-> Function of TS(G()), D(), TermVal(set) -> Element of D(), NTermVal(set, set,
set, set, set) -> Element of D() }: f1() = f2()
provided
A1: (for t being Terminal of G() holds f1().(root-tree t) = TermVal(t))
& for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr
being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <*
rtl, rtr *> for xl, xr being Element of D() st xl = f1().tl & xr = f1().tr
holds f1().(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr) and
A2: (for t being Terminal of G() holds f2().(root-tree t) = TermVal(t))
& for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr
being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <*
rtl, rtr *> for xl, xr being Element of D() st xl = f2().tl & xr = f2().tr
holds f2().(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr)
proof
deffunc BNTV(Symbol of G(), FinSequence, FinSequence of D()) = NTermVal($1,
$2.1, $2.2, $3.1, $3.2);
A3: now
thus for t be Symbol of G() st t in Terminals G() holds f2().(root-tree t)
= TermVal(t) by A2;
let nt be Symbol of G(), ts be FinSequence of TS G();
set rts = roots ts;
set x = f2() * ts;
assume
A4: nt ==> rts;
then consider tl, tr being Element of TS G() such that
A5: roots ts = <*root-label tl, root-label tr*> and
A6: tl = ts.1 and
A7: tr = ts.2 and
A8: nt-tree ts = nt-tree (tl, tr) and
tl in rng ts and
tr in rng ts by Th10;
A9: nt is NonTerminal of G() by A4,Th10;
reconsider xr = f2().tr as Element of D();
2 in dom ts by A4,Th10;
then
A10: x.2 = xr by A7,FUNCT_1:13;
reconsider xl = f2().tl as Element of D();
1 in dom ts by A4,Th10;
then
A11: x.1 = xl by A6,FUNCT_1:13;
thus f2().(nt-tree ts) = BNTV(nt, rts, x) by A2,A4,A5,A8,A9,A11,A10;
end;
A12: now
thus for t being Symbol of G() st t in Terminals G() holds f1().(root-tree
t) = TermVal(t) by A1;
let nt be Symbol of G(), ts be FinSequence of TS G();
set rts = roots ts;
set x = f1() * ts;
assume
A13: nt ==> rts;
then consider tl, tr being Element of TS G() such that
A14: roots ts = <*root-label tl, root-label tr*> and
A15: tl = ts.1 and
A16: tr = ts.2 and
A17: nt-tree ts = nt-tree (tl, tr) and
tl in rng ts and
tr in rng ts by Th10;
A18: nt is NonTerminal of G() by A13,Th10;
reconsider xr = f1().tr as Element of D();
2 in dom ts by A13,Th10;
then
A19: x.2 = xr by A16,FUNCT_1:13;
reconsider xl = f1().tl as Element of D();
1 in dom ts by A13,Th10;
then
A20: x.1 = xl by A15,FUNCT_1:13;
thus f1().(nt-tree ts) = BNTV(nt, rts, x) by A1,A13,A14,A17,A18,A20,A19;
end;
thus thesis from DTCONSTR:sch 9(A12, A3);
end;
scheme
BinDTCDefLambda { G() -> binary with_terminals with_nonterminals
with_useful_nonterminals non empty DTConstrStr, A, B() -> non empty set, F(
set, set) -> Element of B(), H(set, set, set, set) -> Element of B() }: ex f
being Function of TS G(), Funcs(A(), B()) st (for t being Terminal of G() ex g
being Function of A(), B() st g = f.(root-tree t) & for a being Element of A()
holds g.a = F(t, a)) & for nt being NonTerminal of G(), t1, t2 being Element of
TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label
t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f.(nt
-tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 & for a being Element of A() holds g.a
= H(nt, f1, f2, a) proof
defpred P[set,set,set,set] means for a being Element of A() for ntv being
Function of A(), B() st ntv = $4 holds ntv.a = H($1, $2, $3, a);
defpred P[set,set] means for tv being Function of A(), B() st tv = $2 for a
being Element of A() holds tv.a = F($1, a);
reconsider FAB = Funcs(A(), B()) as non empty set;
A1: now
let x be Element of Terminals G();
deffunc F(set) = F(x,$1);
consider y being Function of A(), B() such that
A2: for a being Element of A() holds y.a = F(a) from FUNCT_2:sch 4;
A() = dom y & rng y c= B() by FUNCT_2:def 1;
then reconsider y as Element of FAB by FUNCT_2:def 2;
take y;
thus P[x,y] by A2;
end;
consider TV being Function of Terminals G(), FAB such that
A3: for e being Element of Terminals G() holds P[e,TV.e] from FUNCT_2:
sch 3 (A1);
deffunc TermVal(Terminal of G()) = TV.$1;
A4: now
let x be Element of NonTerminals G(), y, z be Element of FAB;
deffunc F(set) = H(x, y, z, $1);
consider fab being Function of A(), B() such that
A5: for a being Element of A() holds fab.a = F(a) from FUNCT_2:sch 4;
A() = dom fab & rng fab c= B() by FUNCT_2:def 1;
then reconsider fab as Element of FAB by FUNCT_2:def 2;
take fab;
thus P[x,y,z,fab] by A5;
end;
consider NTV being Function of [:NonTerminals G(), FAB, FAB:], FAB such that
A6: for x being Element of NonTerminals G(), y,z being Element of FAB
holds P[x,y,z,NTV.[x,y,z]] from MULTOP_1:sch 1 (A4);
deffunc NTermVal(Element of NonTerminals G(), set, set, Element of FAB,
Element of FAB) = NTV.[$1, $4, $5];
consider f being Function of TS(G()), FAB such that
A7: (for t being Terminal of G() holds f.(root-tree t) = TermVal(t)) &
for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr
being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <*
rtl, rtr *> for xl, xr being Element of FAB st xl = f.tl & xr = f.tr holds f.(
nt-tree (tl, tr)) = NTermVal(nt,rtl,rtr,xl,xr) from BinDTConstrIndDef;
reconsider f9 = f as Function of TS G(), Funcs(A(), B());
take f9;
hereby
let t be Terminal of G();
consider TVt being Function such that
A8: TV.t = TVt and
A9: dom TVt = A() & rng TVt c= B() by FUNCT_2:def 2;
reconsider TVt as Function of A(), B() by A9,FUNCT_2:def 1,RELSET_1:4;
take TVt;
thus TVt = f9.(root-tree t) by A7,A8;
let a be Element of A();
thus TVt.a = F(t, a) by A3,A8;
end;
let nt be NonTerminal of G(), t1, t2 be Element of TS G(), rtl, rtr be
Symbol of G();
assume
A10: rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *>;
ex f2 being Function st f.t2 = f2 & dom f2 = A() & rng f2 c= B() by
FUNCT_2:def 2;
then reconsider f2 = f.t2 as Function of A(), B() by FUNCT_2:def 1,RELSET_1:4
;
ex f1 being Function st f.t1 = f1 & dom f1 = A() & rng f1 c= B() by
FUNCT_2:def 2;
then reconsider f1 = f.t1 as Function of A(), B() by FUNCT_2:def 1,RELSET_1:4
;
NTV.[nt, f.t1, f.t2] in FAB;
then consider ntvval being Function such that
A11: ntvval = NTV.[nt, f1, f2] and
A12: dom ntvval = A() & rng ntvval c= B() by FUNCT_2:def 2;
reconsider ntvval as Function of A(), B() by A12,FUNCT_2:def 1,RELSET_1:4;
take ntvval, f1, f2;
thus ntvval = f9.(nt-tree (t1, t2)) & f1 = f9.t1 & f2 = f9.t2 by A7,A10,A11;
thus thesis by A6,A11;
end;
scheme
BinDTCDefLambdaUniq { G() -> binary with_terminals with_nonterminals
with_useful_nonterminals non empty DTConstrStr, A, B() -> non empty set, f1,
f2() -> Function of TS G(), Funcs (A(), B()), F(set, set) -> Element of B(), H(
set, set, set, set) -> Element of B() }: f1() = f2()
provided
A1: (for t being Terminal of G() ex g being Function of A(), B() st g =
f1().(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & for nt
being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol
of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex
g, f1, f2 being Function of A(), B() st g = f1().(nt-tree (t1, t2)) & f1 = f1()
.t1 & f2 = f1().t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a)
and
A2: (for t being Terminal of G() ex g being Function of A(), B() st g =
f2().(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & for nt
being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol
of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex
g, f1, f2 being Function of A(), B() st g = f2().(nt-tree (t1, t2)) & f1 = f2()
.t1 & f2 = f2().t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a)
proof
defpred P[set,set,set,set] means for a being Element of A() for ntv being
Function of A(), B() st ntv = $4 holds ntv.a = H($1, $2, $3, a);
defpred P[set,set] means for tv being Function of A(), B() st tv = $2 for a
being Element of A() holds tv.a = F($1, a);
reconsider FAB = Funcs(A(), B()) as non empty set;
reconsider f29 = f2() as Function of TS G(), FAB;
A3: now
let x be Element of Terminals G();
deffunc F(Element of A()) = F(x,$1);
consider y being Function of A(), B() such that
A4: for a being Element of A() holds y.a = F(a) from FUNCT_2:sch 4;
A() = dom y & rng y c= B() by FUNCT_2:def 1;
then reconsider y as Element of FAB by FUNCT_2:def 2;
take y;
thus P[x,y] by A4;
end;
consider TV being Function of Terminals G(), FAB such that
A5: for e being Element of Terminals G() holds P[e,TV.e] from FUNCT_2:
sch 3 (A3);
deffunc TermVal(Terminal of G()) = TV.$1;
A6: now
let x be Element of NonTerminals G(), y, z be Element of FAB;
deffunc F(Element of A()) = H(x, y, z, $1);
consider fab being Function of A(), B() such that
A7: for a being Element of A() holds fab.a = F(a) from FUNCT_2:sch 4;
A() = dom fab & rng fab c= B() by FUNCT_2:def 1;
then reconsider fab as Element of FAB by FUNCT_2:def 2;
take fab;
thus P[x,y,z,fab] by A7;
end;
consider NTV being Function of [:NonTerminals G(), FAB, FAB:], FAB such that
A8: for x being Element of NonTerminals G(), y being Element of FAB, z
being Element of FAB holds P[x,y,z,NTV.[x,y,z]] from MULTOP_1:sch 1 (A6);
deffunc NTV(NonTerminal of G(),set,set,Element of FAB,Element of FAB) = NTV.
[$1, $4, $5];
A9: now
hereby
let t be Terminal of G();
consider TVt being Function such that
A10: TV.t = TVt and
A11: dom TVt = A() and
A12: rng TVt c= B() by FUNCT_2:def 2;
reconsider TVt as Function of A(), B() by A11,A12,FUNCT_2:def 1
,RELSET_1:4;
consider g being Function of A(), B() such that
A13: g = f2().(root-tree t) and
A14: for a being Element of A() holds g.a = F(t, a) by A2;
now
thus A() = dom g by FUNCT_2:def 1;
thus A() = dom TVt by A11;
let x be object;
assume x in A();
then reconsider xx = x as Element of A();
g.xx = F(t, xx) by A14
.= (TVt).xx by A5,A10;
hence g.x = TVt.x;
end;
hence f29.(root-tree t) = TermVal(t) by A13,A10,FUNCT_1:2;
end;
let nt be NonTerminal of G(), tl, tr be Element of TS(G()), rtl, rtr be
Symbol of G();
assume rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *>;
then consider g, ff1, ff2 being Function of A(), B() such that
A15: g = f2().(nt-tree (tl, tr)) and
A16: ff1 = f2().tl & ff2 = f2().tr & for a being Element of A() holds
g.a = H (nt, ff1, ff2, a) by A2;
let xl, xr be Element of FAB;
consider ntvnt being Function such that
A17: ntvnt = NTV.[nt, xl, xr] and
A18: dom ntvnt = A() & rng ntvnt c= B() by FUNCT_2:def 2;
reconsider ntvnt as Function of A(), B() by A18,FUNCT_2:def 1,RELSET_1:4;
assume
A19: xl = f29.tl & xr = f29.tr;
now
thus A() = dom g by FUNCT_2:def 1;
thus A() = dom ntvnt by FUNCT_2:def 1;
let x be object;
assume x in A();
then reconsider xx = x as Element of A();
g.xx = H(nt, xl, xr, xx) by A19,A16
.= ntvnt.xx by A8,A17;
hence g.x = ntvnt.x;
end;
hence f29.(nt-tree (tl, tr)) = NTV(nt, rtl,rtr,xl, xr) by A15,A17,FUNCT_1:2
;
end;
reconsider f19 = f1() as Function of TS G(), FAB;
A20: now
hereby
let t be Terminal of G();
consider TVt being Function such that
A21: TV.t = TVt and
A22: dom TVt = A() and
A23: rng TVt c= B() by FUNCT_2:def 2;
reconsider TVt as Function of A(), B() by A22,A23,FUNCT_2:def 1
,RELSET_1:4;
consider g being Function of A(), B() such that
A24: g = f1().(root-tree t) and
A25: for a being Element of A() holds g.a = F(t, a) by A1;
now
thus A() = dom g by FUNCT_2:def 1;
thus A() = dom TVt by A22;
let x be object;
assume x in A();
then reconsider xx = x as Element of A();
g.xx = F(t, xx) by A25
.= (TVt).xx by A5,A21;
hence g.x = TVt.x;
end;
hence f19.(root-tree t) = TermVal(t) by A24,A21,FUNCT_1:2;
end;
let nt be NonTerminal of G(), tl, tr be Element of TS(G()), rtl, rtr be
Symbol of G();
assume rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *>;
then consider g, ff1, ff2 being Function of A(), B() such that
A26: g = f1().(nt-tree (tl, tr)) and
A27: ff1 = f1().tl & ff2 = f1().tr & for a being Element of A() holds
g.a = H (nt, ff1, ff2, a) by A1;
let xl, xr be Element of FAB;
consider ntvnt being Function such that
A28: ntvnt = NTV.[nt, xl, xr] and
A29: dom ntvnt = A() & rng ntvnt c= B() by FUNCT_2:def 2;
reconsider ntvnt as Function of A(), B() by A29,FUNCT_2:def 1,RELSET_1:4;
assume
A30: xl = f19.tl & xr = f19.tr;
now
thus A() = dom g by FUNCT_2:def 1;
thus A() = dom ntvnt by FUNCT_2:def 1;
let x be object;
assume x in A();
then reconsider xx = x as Element of A();
g.xx = H(nt, xl, xr, xx) by A30,A27
.= ntvnt.xx by A8,A28;
hence g.x = ntvnt.x;
end;
hence f19.(nt-tree (tl, tr)) = NTV(nt,rtl,rtr,xl,xr) by A26,A28,FUNCT_1:2;
end;
f19 = f29 from BinDTConstrUniqDef ( A20, A9 );
hence thesis;
end;
registration
let G be binary with_terminals with_nonterminals non empty DTConstrStr;
cluster -> binary for Element of TS G;
coherence
proof
defpred P[DecoratedTree] means $1 is binary;
A1: now
let s be Terminal of G;
dom root-tree s is binary by TREES_4:3;
hence P[root-tree s] by Def3;
end;
A2: for nt being NonTerminal of G, tl, tr being Element of TS(G) st nt ==>
<*root-label tl, root-label tr*> & P[tl] & P[tr] holds P[nt-tree(tl, tr)] by
Th9;
thus for x being Element of TS(G) holds P[x] from BinDTConstrInd ( A1, A2);
end;
end;