:: DTCONSTR semantic presentation

deffunc H1( set ) -> Element of NAT = 0;

deffunc H2( set , set , set ) -> Element of NAT = 0;

theorem Th1: :: DTCONSTR:1
for b1 being non empty set
for b2 being FinSequence of FinTrees b1 holds b2 is FinSequence of Trees b1
proof end;

theorem Th2: :: DTCONSTR:2
for b1, b2 being set
for b3 being FinSequence of b1 st b2 in dom b3 holds
b3 . b2 in b1
proof end;

registration
let c1 be set ;
cluster -> FinSequence-like Element of a1 * ;
coherence
for b1 being Element of c1 * holds b1 is FinSequence-like ;
end;

registration
let c1 be non empty set ;
let c2 be DTree-set of c1;
cluster -> DTree-yielding FinSequence of a2;
coherence
for b1 being FinSequence of c2 holds b1 is DTree-yielding
proof end;
end;

definition
let c1 be non empty set ;
let c2 be non empty DTree-set of c1;
let c3 be non empty Subset of c2;
redefine mode Element as Element of c3 -> Element of a2;
coherence
for b1 being Element of c3 holds b1 is Element of c2
proof end;
end;

definition
let c1 be non empty set ;
let c2 be DTree-set of c1;
let c3 be FinSequence of c2;
redefine func roots as roots c3 -> FinSequence of a1;
coherence
roots c3 is FinSequence of c1
proof end;
end;

E3: dom (roots {} ) = dom {} by TREES_3:23, TREES_3:def 18
.= {} by FINSEQ_1:26 ;

theorem Th3: :: DTCONSTR:3
roots {} = {} by Lemma3, FINSEQ_1:26;

theorem Th4: :: DTCONSTR:4
for b1 being DecoratedTree holds roots <*b1*> = <*(b1 . {} )*>
proof end;

theorem Th5: :: DTCONSTR:5
for b1 being non empty set
for b2 being Subset of (FinTrees b1)
for b3 being FinSequence of b2 st len (roots b3) = 1 holds
ex b4 being Element of FinTrees b1 st
( b3 = <*b4*> & b4 in b2 )
proof end;

theorem Th6: :: DTCONSTR:6
for b1, b2 being DecoratedTree holds roots <*b1,b2*> = <*(b1 . {} ),(b2 . {} )*>
proof end;

definition
let c1, c2 be set ;
let c3 be FinSequence of [:c1,c2:];
redefine func pr1 as pr1 c3 -> FinSequence of a1;
coherence
pr1 c3 is FinSequence of c1
proof end;
redefine func pr2 as pr2 c3 -> FinSequence of a2;
coherence
pr2 c3 is FinSequence of c2
proof end;
end;

theorem Th7: :: DTCONSTR:7
( pr1 {} = {} & pr2 {} = {} )
proof end;

registration
let c1 be non empty set ;
let c2 be Relation of c1,c1 * ;
cluster DTConstrStr(# a1,a2 #) -> non empty ;
coherence
not DTConstrStr(# c1,c2 #) is empty by STRUCT_0:def 1;
end;

scheme :: DTCONSTR:sch 1
s1{ F1() -> non empty set , P1[ set , set ] } :
ex b1 being non empty strict DTConstrStr st
( the carrier of b1 = F1() & ( for b2 being Symbol of b1
for b3 being FinSequence of the carrier of b1 holds
( b2 ==> b3 iff P1[b2,b3] ) ) )
proof end;

scheme :: DTCONSTR:sch 2
s2{ F1() -> non empty set , P1[ set , set ] } :
for b1, b2 being non empty strict DTConstrStr st the carrier of b1 = F1() & ( for b3 being Symbol of b1
for b4 being FinSequence of the carrier of b1 holds
( b3 ==> b4 iff P1[b3,b4] ) ) & the carrier of b2 = F1() & ( for b3 being Symbol of b2
for b4 being FinSequence of the carrier of b2 holds
( b3 ==> b4 iff P1[b3,b4] ) ) holds
b1 = b2
proof end;

theorem Th8: :: DTCONSTR:8
for b1 being non empty DTConstrStr holds Terminals b1 misses NonTerminals b1
proof end;

scheme :: DTCONSTR:sch 3
s3{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex b1 being Subset of (FinTrees [:the carrier of F2(),F3():]) st
( b1 = Union F1() & ( for b2 being Symbol of F2() st b2 in Terminals F2() holds
root-tree [b2,F4(b2)] in b1 ) & ( for b2 being Symbol of F2()
for b3 being FinSequence of b1 st b2 ==> pr1 (roots b3) holds
[b2,F5(b2,(pr1 (roots b3)),(pr2 (roots b3)))] -tree b3 in b1 ) & ( for b2 being Subset of (FinTrees [:the carrier of F2(),F3():]) st ( for b3 being Symbol of F2() st b3 in Terminals F2() holds
root-tree [b3,F4(b3)] in b2 ) & ( for b3 being Symbol of F2()
for b4 being FinSequence of b2 st b3 ==> pr1 (roots b4) holds
[b3,F5(b3,(pr1 (roots b4)),(pr2 (roots b4)))] -tree b4 in b2 ) holds
b1 c= b2 ) )
provided
E8: dom F1() = NAT and
E9: F1() . 0 = { (root-tree [b1,b2]) where B is Symbol of F2(), B is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{} ,{} ) ) ) } and
E10: for b1 being Nat holds F1() . (b1 + 1) = (F1() . b1) \/ { ([b2,F5(b2,(pr1 (roots b3)),(pr2 (roots b3)))] -tree b3) where B is Symbol of F2(), B is Element of (F1() . b1) * : ex b1 being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( b3 = b4 & b2 ==> pr1 (roots b4) ) }
proof end;

scheme :: DTCONSTR:sch 4
s4{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex b1 being Subset of (FinTrees the carrier of F2()) st
( b1 = { (b2 `1 ) where B is Element of FinTrees [:the carrier of F2(),F3():] : b2 in Union F1() } & ( for b2 being Symbol of F2() st b2 in Terminals F2() holds
root-tree b2 in b1 ) & ( for b2 being Symbol of F2()
for b3 being FinSequence of b1 st b2 ==> roots b3 holds
b2 -tree b3 in b1 ) & ( for b2 being Subset of (FinTrees the carrier of F2()) st ( for b3 being Symbol of F2() st b3 in Terminals F2() holds
root-tree b3 in b2 ) & ( for b3 being Symbol of F2()
for b4 being FinSequence of b2 st b3 ==> roots b4 holds
b3 -tree b4 in b2 ) holds
b1 c= b2 ) )
provided
E8: dom F1() = NAT and
E9: F1() . 0 = { (root-tree [b1,b2]) where B is Symbol of F2(), B is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{} ,{} ) ) ) } and
E10: for b1 being Nat holds F1() . (b1 + 1) = (F1() . b1) \/ { ([b2,F5(b2,(pr1 (roots b3)),(pr2 (roots b3)))] -tree b3) where B is Symbol of F2(), B is Element of (F1() . b1) * : ex b1 being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( b3 = b4 & b2 ==> pr1 (roots b4) ) }
proof end;

scheme :: DTCONSTR:sch 5
s5{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for b1 being Nat
for b2 being Element of FinTrees [:the carrier of F2(),F3():] st b2 in Union F1() holds
( b2 in F1() . b1 iff height (dom b2) <= b1 )
provided
E8: dom F1() = NAT and
E9: F1() . 0 = { (root-tree [b1,b2]) where B is Symbol of F2(), B is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{} ,{} ) ) ) } and
E10: for b1 being Nat holds F1() . (b1 + 1) = (F1() . b1) \/ { ([b2,F5(b2,(pr1 (roots b3)),(pr2 (roots b3)))] -tree b3) where B is Symbol of F2(), B is Element of (F1() . b1) * : ex b1 being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( b3 = b4 & b2 ==> pr1 (roots b4) ) }
proof end;

scheme :: DTCONSTR:sch 6
s6{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for b1, b2 being DecoratedTree of [:the carrier of F2(),F3():] st b1 in Union F1() & b2 in Union F1() & b1 `1 = b2 `1 holds
b1 = b2
provided
E8: dom F1() = NAT and
E9: F1() . 0 = { (root-tree [b1,b2]) where B is Symbol of F2(), B is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{} ,{} ) ) ) } and
E10: for b1 being Nat holds F1() . (b1 + 1) = (F1() . b1) \/ { ([b2,F5(b2,(pr1 (roots b3)),(pr2 (roots b3)))] -tree b3) where B is Symbol of F2(), B is Element of (F1() . b1) * : ex b1 being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( b3 = b4 & b2 ==> pr1 (roots b4) ) }
proof end;

definition
let c1 be non empty DTConstrStr ;
canceled;
canceled;
canceled;
func TS c1 -> Subset of (FinTrees the carrier of a1) means :Def4: :: DTCONSTR:def 4
( ( for b1 being Symbol of a1 st b1 in Terminals a1 holds
root-tree b1 in a2 ) & ( for b1 being Symbol of a1
for b2 being FinSequence of a2 st b1 ==> roots b2 holds
b1 -tree b2 in a2 ) & ( for b1 being Subset of (FinTrees the carrier of a1) st ( for b2 being Symbol of a1 st b2 in Terminals a1 holds
root-tree b2 in b1 ) & ( for b2 being Symbol of a1
for b3 being FinSequence of b1 st b2 ==> roots b3 holds
b2 -tree b3 in b1 ) holds
a2 c= b1 ) );
existence
ex b1 being Subset of (FinTrees the carrier of c1) st
( ( for b2 being Symbol of c1 st b2 in Terminals c1 holds
root-tree b2 in b1 ) & ( for b2 being Symbol of c1
for b3 being FinSequence of b1 st b2 ==> roots b3 holds
b2 -tree b3 in b1 ) & ( for b2 being Subset of (FinTrees the carrier of c1) st ( for b3 being Symbol of c1 st b3 in Terminals c1 holds
root-tree b3 in b2 ) & ( for b3 being Symbol of c1
for b4 being FinSequence of b2 st b3 ==> roots b4 holds
b3 -tree b4 in b2 ) holds
b1 c= b2 ) )
proof end;
uniqueness
for b1, b2 being Subset of (FinTrees the carrier of c1) st ( for b3 being Symbol of c1 st b3 in Terminals c1 holds
root-tree b3 in b1 ) & ( for b3 being Symbol of c1
for b4 being FinSequence of b1 st b3 ==> roots b4 holds
b3 -tree b4 in b1 ) & ( for b3 being Subset of (FinTrees the carrier of c1) st ( for b4 being Symbol of c1 st b4 in Terminals c1 holds
root-tree b4 in b3 ) & ( for b4 being Symbol of c1
for b5 being FinSequence of b3 st b4 ==> roots b5 holds
b4 -tree b5 in b3 ) holds
b1 c= b3 ) & ( for b3 being Symbol of c1 st b3 in Terminals c1 holds
root-tree b3 in b2 ) & ( for b3 being Symbol of c1
for b4 being FinSequence of b2 st b3 ==> roots b4 holds
b3 -tree b4 in b2 ) & ( for b3 being Subset of (FinTrees the carrier of c1) st ( for b4 being Symbol of c1 st b4 in Terminals c1 holds
root-tree b4 in b3 ) & ( for b4 being Symbol of c1
for b5 being FinSequence of b3 st b4 ==> roots b5 holds
b4 -tree b5 in b3 ) holds
b2 c= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 DTCONSTR:def 1 :
canceled;

:: deftheorem Def2 DTCONSTR:def 2 :
canceled;

:: deftheorem Def3 DTCONSTR:def 3 :
canceled;

:: deftheorem Def4 defines TS DTCONSTR:def 4 :
for b1 being non empty DTConstrStr
for b2 being Subset of (FinTrees the carrier of b1) holds
( b2 = TS b1 iff ( ( for b3 being Symbol of b1 st b3 in Terminals b1 holds
root-tree b3 in b2 ) & ( for b3 being Symbol of b1
for b4 being FinSequence of b2 st b3 ==> roots b4 holds
b3 -tree b4 in b2 ) & ( for b3 being Subset of (FinTrees the carrier of b1) st ( for b4 being Symbol of b1 st b4 in Terminals b1 holds
root-tree b4 in b3 ) & ( for b4 being Symbol of b1
for b5 being FinSequence of b3 st b4 ==> roots b5 holds
b4 -tree b5 in b3 ) holds
b2 c= b3 ) ) );

scheme :: DTCONSTR:sch 7
s7{ F1() -> non empty DTConstrStr , P1[ set ] } :
for b1 being DecoratedTree of the carrier of F1() st b1 in TS F1() holds
P1[b1]
provided
E9: for b1 being Symbol of F1() st b1 in Terminals F1() holds
P1[ root-tree b1] and
E10: for b1 being Symbol of F1()
for b2 being FinSequence of TS F1() st b1 ==> roots b2 & ( for b3 being DecoratedTree of the carrier of F1() st b3 in rng b2 holds
P1[b3] ) holds
P1[b1 -tree b2]
proof end;

scheme :: DTCONSTR:sch 8
s8{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2() } :
ex b1 being Function of TS F1(),F2() st
( ( for b2 being Symbol of F1() st b2 in Terminals F1() holds
b1 . (root-tree b2) = F3(b2) ) & ( for b2 being Symbol of F1()
for b3 being FinSequence of TS F1() st b2 ==> roots b3 holds
b1 . (b2 -tree b3) = F4(b2,(roots b3),(b1 * b3)) ) )
proof end;

scheme :: DTCONSTR:sch 9
s9{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of TS F1(),F2(), F6() -> Function of TS F1(),F2() } :
F5() = F6()
provided
E9: ( ( for b1 being Symbol of F1() st b1 in Terminals F1() holds
F5() . (root-tree b1) = F3(b1) ) & ( for b1 being Symbol of F1()
for b2 being FinSequence of TS F1() st b1 ==> roots b2 holds
F5() . (b1 -tree b2) = F4(b1,(roots b2),(F5() * b2)) ) ) and
E10: ( ( for b1 being Symbol of F1() st b1 in Terminals F1() holds
F6() . (root-tree b1) = F3(b1) ) & ( for b1 being Symbol of F1()
for b2 being FinSequence of TS F1() st b1 ==> roots b2 holds
F6() . (b1 -tree b2) = F4(b1,(roots b2),(F6() * b2)) ) )
proof end;

defpred S1[ set , set ] means ( a1 = 1 & ( a2 = <*0*> or a2 = <*1*> ) );

definition
func PeanoNat -> non empty strict DTConstrStr means :Def5: :: DTCONSTR:def 5
( the carrier of a1 = {0,1} & ( for b1 being Symbol of a1
for b2 being FinSequence of the carrier of a1 holds
( b1 ==> b2 iff ( b1 = 1 & ( b2 = <*0*> or b2 = <*1*> ) ) ) ) );
existence
ex b1 being non empty strict DTConstrStr st
( the carrier of b1 = {0,1} & ( for b2 being Symbol of b1
for b3 being FinSequence of the carrier of b1 holds
( b2 ==> b3 iff ( b2 = 1 & ( b3 = <*0*> or b3 = <*1*> ) ) ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict DTConstrStr st the carrier of b1 = {0,1} & ( for b3 being Symbol of b1
for b4 being FinSequence of the carrier of b1 holds
( b3 ==> b4 iff ( b3 = 1 & ( b4 = <*0*> or b4 = <*1*> ) ) ) ) & the carrier of b2 = {0,1} & ( for b3 being Symbol of b2
for b4 being FinSequence of the carrier of b2 holds
( b3 ==> b4 iff ( b3 = 1 & ( b4 = <*0*> or b4 = <*1*> ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines PeanoNat DTCONSTR:def 5 :
for b1 being non empty strict DTConstrStr holds
( b1 = PeanoNat iff ( the carrier of b1 = {0,1} & ( for b2 being Symbol of b1
for b3 being FinSequence of the carrier of b1 holds
( b2 ==> b3 iff ( b2 = 1 & ( b3 = <*0*> or b3 = <*1*> ) ) ) ) ) );

set c1 = PeanoNat ;

Lemma10: the carrier of PeanoNat = {0,1}
by Def5;

then reconsider c2 = 0, c3 = 1 as Symbol of PeanoNat by TARSKI:def 2;

Lemma11: ( c3 ==> <*c2*> & c3 ==> <*c3*> )
by Def5;

Lemma12: c3 ==> <*c2*>
by Def5;

Lemma13: c3 ==> <*c3*>
by Def5;

Lemma14: Terminals PeanoNat = { b1 where B is Symbol of PeanoNat : for b1 being FinSequence holds not b1 ==> b2 }
by LANG1:def 2;

E15: now
given c4 being FinSequence such that E16: c2 ==> c4 ;
[c2,c4] in the Rules of PeanoNat by E16, LANG1:def 1;
then c4 in the carrier of PeanoNat * by ZFMISC_1:106;
then c4 is FinSequence of the carrier of PeanoNat by FINSEQ_2:def 3;
hence contradiction by E16, Def5;
end;

then Lemma16: c2 in Terminals PeanoNat
by Lemma14;

Lemma17: Terminals PeanoNat c= {c2}
proof end;

Lemma18: NonTerminals PeanoNat = { b1 where B is Symbol of PeanoNat : ex b1 being FinSequence st b1 ==> b2 }
by LANG1:def 3;

then Lemma19: c3 in NonTerminals PeanoNat
by Lemma12;

then Lemma20: {c3} c= NonTerminals PeanoNat
by ZFMISC_1:37;

Lemma21: NonTerminals PeanoNat c= {c3}
proof end;

then Lemma22: NonTerminals PeanoNat = {c3}
by Lemma20, XBOOLE_0:def 10;

reconsider c4 = TS PeanoNat as non empty Subset of (FinTrees the carrier of PeanoNat ) by Def4, Lemma16;

definition
let c5 be non empty DTConstrStr ;
attr a1 is with_terminals means :Def6: :: DTCONSTR:def 6
 Terminals a1 <> {} ;
attr a1 is with_nonterminals means :Def7: :: DTCONSTR:def 7
 NonTerminals a1 <> {} ;
attr a1 is with_useful_nonterminals means :Def8: :: DTCONSTR:def 8
for b1 being Symbol of a1 st b1 in NonTerminals a1 holds
ex b2 being FinSequence of TS a1 st b1 ==> roots b2;
end;

:: deftheorem Def6 defines with_terminals DTCONSTR:def 6 :
for b1 being non empty DTConstrStr holds
( b1 is with_terminals iff Terminals b1 <> {} );

:: deftheorem Def7 defines with_nonterminals DTCONSTR:def 7 :
for b1 being non empty DTConstrStr holds
( b1 is with_nonterminals iff NonTerminals b1 <> {} );

:: deftheorem Def8 defines with_useful_nonterminals DTCONSTR:def 8 :
for b1 being non empty DTConstrStr holds
( b1 is with_useful_nonterminals iff for b2 being Symbol of b1 st b2 in NonTerminals b1 holds
ex b3 being FinSequence of TS b1 st b2 ==> roots b3 );

Lemma26: ( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
proof end;

registration
cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr ;
existence
ex b1 being non empty DTConstrStr st
( b1 is with_terminals & b1 is with_nonterminals & b1 is with_useful_nonterminals & b1 is strict ) by Lemma26;
end;

definition
let c5 be non empty with_terminals DTConstrStr ;
redefine func Terminals as Terminals c1 -> non empty Subset of a1;
coherence
Terminals c5 is non empty Subset of c5
proof end;
end;

registration
let c5 be non empty with_terminals DTConstrStr ;
cluster TS a1 -> non empty ;
coherence
not TS c5 is empty
proof end;
end;

registration
let c5 be non empty with_useful_nonterminals DTConstrStr ;
cluster TS a1 -> non empty ;
coherence
not TS c5 is empty
proof end;
end;

definition
let c5 be non empty with_nonterminals DTConstrStr ;
redefine func NonTerminals as NonTerminals c1 -> non empty Subset of a1;
coherence
NonTerminals c5 is non empty Subset of c5
proof end;
end;

definition
let c5 be non empty with_terminals DTConstrStr ;
mode Terminal of a1 is Element of Terminals a1;
end;

definition
let c5 be non empty with_nonterminals DTConstrStr ;
mode NonTerminal of a1 is Element of NonTerminals a1;
end;

definition
let c5 be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let c6 be NonTerminal of c5;
mode SubtreeSeq of c2 -> FinSequence of TS a1 means :Def9: :: DTCONSTR:def 9
a2 ==> roots a3;
existence
ex b1 being FinSequence of TS c5 st c6 ==> roots b1 by Def8;
end;

:: deftheorem Def9 defines SubtreeSeq DTCONSTR:def 9 :
for b1 being non empty with_nonterminals with_useful_nonterminals DTConstrStr
for b2 being NonTerminal of b1
for b3 being FinSequence of TS b1 holds
( b3 is SubtreeSeq of b2 iff b2 ==> roots b3 );

definition
let c5 be non empty with_terminals DTConstrStr ;
let c6 be Terminal of c5;
redefine func root-tree as root-tree c2 -> Element of TS a1;
coherence
root-tree c6 is Element of TS c5 by Def4;
end;

definition
let c5 be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let c6 be NonTerminal of c5;
let c7 be SubtreeSeq of c6;
redefine func -tree as c2 -tree c3 -> Element of TS a1;
coherence
c6 -tree c7 is Element of TS c5
proof end;
end;

theorem Th9: :: DTCONSTR:9
for b1 being non empty with_terminals DTConstrStr
for b2 being Element of TS b1
for b3 being Terminal of b1 st b2 . {} = b3 holds
b2 = root-tree b3
proof end;

theorem Th10: :: DTCONSTR:10
for b1 being non empty with_terminals with_nonterminals DTConstrStr
for b2 being Element of TS b1
for b3 being NonTerminal of b1 st b2 . {} = b3 holds
ex b4 being FinSequence of TS b1 st
( b2 = b3 -tree b4 & b3 ==> roots b4 )
proof end;

registration
cluster PeanoNat -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) by Lemma26;
end;

set c5 = PeanoNat ;

reconsider c6 = c2 as Terminal of PeanoNat by Lemma16;

reconsider c7 = c3 as NonTerminal of PeanoNat by Lemma19;

definition
let c8 be NonTerminal of PeanoNat ;
let c9 be Element of TS PeanoNat ;
redefine func -tree as c1 -tree c2 -> Element of TS PeanoNat ;
coherence
c8 -tree c9 is Element of TS PeanoNat
proof end;
end;

definition
let c8 be FinSequence of NAT ;
assume E30: c8 <> {} ;
func plus-one c1 -> Nat means :Def10: :: DTCONSTR:def 10
ex b1 being Nat st
( a2 = b1 + 1 & a1 . 1 = b1 );
existence
ex b1, b2 being Nat st
( b1 = b2 + 1 & c8 . 1 = b2 )
proof end;
correctness
uniqueness
for b1, b2 being Nat st ex b3 being Nat st
( b1 = b3 + 1 & c8 . 1 = b3 ) & ex b3 being Nat st
( b2 = b3 + 1 & c8 . 1 = b3 ) holds
b1 = b2;
;
end;

:: deftheorem Def10 defines plus-one DTCONSTR:def 10 :
for b1 being FinSequence of NAT st b1 <> {} holds
for b2 being Nat holds
( b2 = plus-one b1 iff ex b3 being Nat st
( b2 = b3 + 1 & b1 . 1 = b3 ) );

deffunc H3( set , set , FinSequence of NAT ) -> Nat = plus-one a3;

definition
func PN-to-NAT -> Function of TS PeanoNat , NAT means :Def11: :: DTCONSTR:def 11
( ( for b1 being Symbol of PeanoNat st b1 in Terminals PeanoNat holds
a1 . (root-tree b1) = 0 ) & ( for b1 being Symbol of PeanoNat
for b2 being FinSequence of TS PeanoNat st b1 ==> roots b2 holds
a1 . (b1 -tree b2) = plus-one (a1 * b2) ) );
existence
ex b1 being Function of TS PeanoNat , NAT st
( ( for b2 being Symbol of PeanoNat st b2 in Terminals PeanoNat holds
b1 . (root-tree b2) = 0 ) & ( for b2 being Symbol of PeanoNat
for b3 being FinSequence of TS PeanoNat st b2 ==> roots b3 holds
b1 . (b2 -tree b3) = plus-one (b1 * b3) ) )
proof end;
uniqueness
for b1, b2 being Function of TS PeanoNat , NAT st ( for b3 being Symbol of PeanoNat st b3 in Terminals PeanoNat holds
b1 . (root-tree b3) = 0 ) & ( for b3 being Symbol of PeanoNat
for b4 being FinSequence of TS PeanoNat st b3 ==> roots b4 holds
b1 . (b3 -tree b4) = plus-one (b1 * b4) ) & ( for b3 being Symbol of PeanoNat st b3 in Terminals PeanoNat holds
b2 . (root-tree b3) = 0 ) & ( for b3 being Symbol of PeanoNat
for b4 being FinSequence of TS PeanoNat st b3 ==> roots b4 holds
b2 . (b3 -tree b4) = plus-one (b2 * b4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines PN-to-NAT DTCONSTR:def 11 :
for b1 being Function of TS PeanoNat , NAT holds
( b1 = PN-to-NAT iff ( ( for b2 being Symbol of PeanoNat st b2 in Terminals PeanoNat holds
b1 . (root-tree b2) = 0 ) & ( for b2 being Symbol of PeanoNat
for b3 being FinSequence of TS PeanoNat st b2 ==> roots b3 holds
b1 . (b2 -tree b3) = plus-one (b1 * b3) ) ) );

definition
let c8 be Element of TS PeanoNat ;
func PNsucc c1 -> Element of TS PeanoNat equals :: DTCONSTR:def 12
1 -tree <*a1*>;
coherence
1 -tree <*c8*> is Element of TS PeanoNat
proof end;
end;

:: deftheorem Def12 defines PNsucc DTCONSTR:def 12 :
for b1 being Element of TS PeanoNat holds PNsucc b1 = 1 -tree <*b1*>;

deffunc H4( set , Element of TS PeanoNat ) -> Element of TS PeanoNat = PNsucc a2;

definition
func NAT-to-PN -> Function of NAT , TS PeanoNat means :Def13: :: DTCONSTR:def 13
( a1 . 0 = root-tree 0 & ( for b1 being Nat holds a1 . (b1 + 1) = PNsucc (a1 . b1) ) );
existence
ex b1 being Function of NAT , TS PeanoNat st
( b1 . 0 = root-tree 0 & ( for b2 being Nat holds b1 . (b2 + 1) = PNsucc (b1 . b2) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , TS PeanoNat st b1 . 0 = root-tree 0 & ( for b3 being Nat holds b1 . (b3 + 1) = PNsucc (b1 . b3) ) & b2 . 0 = root-tree 0 & ( for b3 being Nat holds b2 . (b3 + 1) = PNsucc (b2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines NAT-to-PN DTCONSTR:def 13 :
for b1 being Function of NAT , TS PeanoNat holds
( b1 = NAT-to-PN iff ( b1 . 0 = root-tree 0 & ( for b2 being Nat holds b1 . (b2 + 1) = PNsucc (b1 . b2) ) ) );

theorem Th11: :: DTCONSTR:11
for b1 being Element of TS PeanoNat holds b1 = NAT-to-PN . (PN-to-NAT . b1)
proof end;

E33: 0 = PN-to-NAT . (root-tree c6) by Def11
.= PN-to-NAT . (NAT-to-PN . 0) by Def13 ;

E34: now
let c8 be Nat;
assume E35: c8 = PN-to-NAT . (NAT-to-PN . c8) ;
reconsider c9 = NAT-to-PN . c8 as Element of TS PeanoNat ;
reconsider c10 = {} as Node of c9 by TREES_1:47;
E36: ( c9 . c10 = c6 or c9 . c10 = c7 ) by Lemma10, TARSKI:def 2;
E37: NAT-to-PN . (c8 + 1) = PNsucc (NAT-to-PN . c8) by Def13
.= c7 -tree <*(NAT-to-PN . c8)*> ;
E38: c7 ==> roots <*(NAT-to-PN . c8)*> by E36, Lemma11, Th4;
consider c11 being Nat such that
E39: ( plus-one <*c8*> = c11 + 1 & <*c8*> . 1 = c11 ) by Def10;
<*(PN-to-NAT . (NAT-to-PN . c8))*> = PN-to-NAT * <*(NAT-to-PN . c8)*> by FINSEQ_2:39;
then PN-to-NAT . (c7 -tree <*(NAT-to-PN . c8)*>) = plus-one <*c8*> by E35, E38, Def11
.= c8 + 1 by E39, FINSEQ_1:57 ;
hence c8 + 1 = PN-to-NAT . (NAT-to-PN . (c8 + 1)) by E37;
end;

theorem Th12: :: DTCONSTR:12
for b1 being Nat holds b1 = PN-to-NAT . (NAT-to-PN . b1)
proof end;

definition
let c8 be set ;
let c9 be FinSequence of c8 * ;
func FlattenSeq c2 -> Element of a1 * means :Def14: :: DTCONSTR:def 14
ex b1 being BinOp of a1 * st
( ( for b2, b3 being Element of a1 * holds b1 . b2,b3 = b2 ^ b3 ) & a3 = b1 "**" a2 );
existence
ex b1 being Element of c8 * ex b2 being BinOp of c8 * st
( ( for b3, b4 being Element of c8 * holds b2 . b3,b4 = b3 ^ b4 ) & b1 = b2 "**" c9 )
proof end;
uniqueness
for b1, b2 being Element of c8 * st ex b3 being BinOp of c8 * st
( ( for b4, b5 being Element of c8 * holds b3 . b4,b5 = b4 ^ b5 ) & b1 = b3 "**" c9 ) & ex b3 being BinOp of c8 * st
( ( for b4, b5 being Element of c8 * holds b3 . b4,b5 = b4 ^ b5 ) & b2 = b3 "**" c9 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines FlattenSeq DTCONSTR:def 14 :
for b1 being set
for b2 being FinSequence of b1 *
for b3 being Element of b1 * holds
( b3 = FlattenSeq b2 iff ex b4 being BinOp of b1 * st
( ( for b5, b6 being Element of b1 * holds b4 . b5,b6 = b5 ^ b6 ) & b3 = b4 "**" b2 ) );

theorem Th13: :: DTCONSTR:13
for b1 being set
for b2 being Element of b1 * holds FlattenSeq <*b2*> = b2
proof end;

definition
let c8 be non empty DTConstrStr ;
let c9 be DecoratedTree of the carrier of c8;
assume E37: c9 in TS c8 ;
defpred S2[ set ] means a1 in Terminals c8;
deffunc H5( set ) -> set = <*a1*>;
deffunc H6( set ) -> set = {} ;
E38: now
let c10 be set ;
assume c10 in the carrier of c8 ;
hereby
assume E39: S2[c10] ;
then reconsider c11 = Terminals c8 as non empty set ;
reconsider c12 = c10 as Element of c11 by E39;
<*c12*> is FinSequence of c11 ;
hence H5(c10) in (Terminals c8) * ;
end;
assume not S2[c10] ;
{} is FinSequence of Terminals c8 by FINSEQ_1:29;
hence H6(c10) in (Terminals c8) * by FINSEQ_1:def 11;
end;
consider c10 being Function of the carrier of c8,(Terminals c8) * such that
E39: for b1 being set st b1 in the carrier of c8 holds
( ( S2[b1] implies c10 . b1 = H5(b1) ) & ( not S2[b1] implies c10 . b1 = H6(b1) ) ) from FUNCT_2:sch 9(E38);
deffunc H7( Symbol of c8) -> Element of (Terminals c8) * = c10 . a1;
deffunc H8( set , set , FinSequence of (Terminals c8) * ) -> Element of (Terminals c8) * = FlattenSeq a3;
deffunc H9( set ) -> set = <*a1*>;
func TerminalString c2 -> FinSequence of Terminals a1 means :Def15: :: DTCONSTR:def 15
ex b1 being Function of TS a1,(Terminals a1) * st
( a3 = b1 . a2 & ( for b2 being Symbol of a1 st b2 in Terminals a1 holds
b1 . (root-tree b2) = <*b2*> ) & ( for b2 being Symbol of a1
for b3 being FinSequence of TS a1 st b2 ==> roots b3 holds
b1 . (b2 -tree b3) = FlattenSeq (b1 * b3) ) );
existence
ex b1 being FinSequence of Terminals c8ex b2 being Function of TS c8,(Terminals c8) * st
( b1 = b2 . c9 & ( for b3 being Symbol of c8 st b3 in Terminals c8 holds
b2 . (root-tree b3) = <*b3*> ) & ( for b3 being Symbol of c8
for b4 being FinSequence of TS c8 st b3 ==> roots b4 holds
b2 . (b3 -tree b4) = FlattenSeq (b2 * b4) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of Terminals c8 st ex b3 being Function of TS c8,(Terminals c8) * st
( b1 = b3 . c9 & ( for b4 being Symbol of c8 st b4 in Terminals c8 holds
b3 . (root-tree b4) = <*b4*> ) & ( for b4 being Symbol of c8
for b5 being FinSequence of TS c8 st b4 ==> roots b5 holds
b3 . (b4 -tree b5) = FlattenSeq (b3 * b5) ) ) & ex b3 being Function of TS c8,(Terminals c8) * st
( b2 = b3 . c9 & ( for b4 being Symbol of c8 st b4 in Terminals c8 holds
b3 . (root-tree b4) = <*b4*> ) & ( for b4 being Symbol of c8
for b5 being FinSequence of TS c8 st b4 ==> roots b5 holds
b3 . (b4 -tree b5) = FlattenSeq (b3 * b5) ) ) holds
b1 = b2
proof end;
E40: now
let c11 be set ;
assume c11 in the carrier of c8 ;
then reconsider c12 = c11 as Element of c8 ;
<*c12*> is FinSequence of the carrier of c8 ;
hence H9(c11) in the carrier of c8 * ;
end;
consider c11 being Function of the carrier of c8,the carrier of c8 * such that
E41: for b1 being set st b1 in the carrier of c8 holds
c11 . b1 = H9(b1) from FUNCT_2:sch 2(E40);
deffunc H10( Symbol of c8) -> Element of the carrier of c8 * = c11 . a1;
deffunc H11( Symbol of c8, set , FinSequence of the carrier of c8 * ) -> Element of the carrier of c8 * = (c11 . a1) ^ (FlattenSeq a3);
func PreTraversal c2 -> FinSequence of the carrier of a1 means :Def16: :: DTCONSTR:def 16
ex b1 being Function of TS a1,the carrier of a1 * st
( a3 = b1 . a2 & ( for b2 being Symbol of a1 st b2 in Terminals a1 holds
b1 . (root-tree b2) = <*b2*> ) & ( for b2 being Symbol of a1
for b3 being FinSequence of TS a1
for b4 being FinSequence st b4 = roots b3 & b2 ==> b4 holds
for b5 being FinSequence of the carrier of a1 * st b5 = b1 * b3 holds
b1 . (b2 -tree b3) = <*b2*> ^ (FlattenSeq b5) ) );
existence
ex b1 being FinSequence of the carrier of c8ex b2 being Function of TS c8,the carrier of c8 * st
( b1 = b2 . c9 & ( for b3 being Symbol of c8 st b3 in Terminals c8 holds
b2 . (root-tree b3) = <*b3*> ) & ( for b3 being Symbol of c8
for b4 being FinSequence of TS c8
for b5 being FinSequence st b5 = roots b4 & b3 ==> b5 holds
for b6 being FinSequence of the carrier of c8 * st b6 = b2 * b4 holds
b2 . (b3 -tree b4) = <*b3*> ^ (FlattenSeq b6) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of c8 st ex b3 being Function of TS c8,the carrier of c8 * st
( b1 = b3 . c9 & ( for b4 being Symbol of c8 st b4 in Terminals c8 holds
b3 . (root-tree b4) = <*b4*> ) & ( for b4 being Symbol of c8
for b5 being FinSequence of TS c8
for b6 being FinSequence st b6 = roots b5 & b4 ==> b6 holds
for b7 being FinSequence of the carrier of c8 * st b7 = b3 * b5 holds
b3 . (b4 -tree b5) = <*b4*> ^ (FlattenSeq b7) ) ) & ex b3 being Function of TS c8,the carrier of c8 * st
( b2 = b3 . c9 & ( for b4 being Symbol of c8 st b4 in Terminals c8 holds
b3 . (root-tree b4) = <*b4*> ) & ( for b4 being Symbol of c8
for b5 being FinSequence of TS c8
for b6 being FinSequence st b6 = roots b5 & b4 ==> b6 holds
for b7 being FinSequence of the carrier of c8 * st b7 = b3 * b5 holds
b3 . (b4 -tree b5) = <*b4*> ^ (FlattenSeq b7) ) ) holds
b1 = b2
proof end;
deffunc H12( Symbol of c8) -> Element of the carrier of c8 * = c11 . a1;
deffunc H13( Symbol of c8, set , FinSequence of the carrier of c8 * ) -> Element of the carrier of c8 * = (FlattenSeq a3) ^ (c11 . a1);
func PostTraversal c2 -> FinSequence of the carrier of a1 means :Def17: :: DTCONSTR:def 17
ex b1 being Function of TS a1,the carrier of a1 * st
( a3 = b1 . a2 & ( for b2 being Symbol of a1 st b2 in Terminals a1 holds
b1 . (root-tree b2) = <*b2*> ) & ( for b2 being Symbol of a1
for b3 being FinSequence of TS a1
for b4 being FinSequence st b4 = roots b3 & b2 ==> b4 holds
for b5 being FinSequence of the carrier of a1 * st b5 = b1 * b3 holds
b1 . (b2 -tree b3) = (FlattenSeq b5) ^ <*b2*> ) );
existence
ex b1 being FinSequence of the carrier of c8ex b2 being Function of TS c8,the carrier of c8 * st
( b1 = b2 . c9 & ( for b3 being Symbol of c8 st b3 in Terminals c8 holds
b2 . (root-tree b3) = <*b3*> ) & ( for b3 being Symbol of c8
for b4 being FinSequence of TS c8
for b5 being FinSequence st b5 = roots b4 & b3 ==> b5 holds
for b6 being FinSequence of the carrier of c8 * st b6 = b2 * b4 holds
b2 . (b3 -tree b4) = (FlattenSeq b6) ^ <*b3*> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of c8 st ex b3 being Function of TS c8,the carrier of c8 * st
( b1 = b3 . c9 & ( for b4 being Symbol of c8 st b4 in Terminals c8 holds
b3 . (root-tree b4) = <*b4*> ) & ( for b4 being Symbol of c8
for b5 being FinSequence of TS c8
for b6 being FinSequence st b6 = roots b5 & b4 ==> b6 holds
for b7 being FinSequence of the carrier of c8 * st b7 = b3 * b5 holds
b3 . (b4 -tree b5) = (FlattenSeq b7) ^ <*b4*> ) ) & ex b3 being Function of TS c8,the carrier of c8 * st
( b2 = b3 . c9 & ( for b4 being Symbol of c8 st b4 in Terminals c8 holds
b3 . (root-tree b4) = <*b4*> ) & ( for b4 being Symbol of c8
for b5 being FinSequence of TS c8
for b6 being FinSequence st b6 = roots b5 & b4 ==> b6 holds
for b7 being FinSequence of the carrier of c8 * st b7 = b3 * b5 holds
b3 . (b4 -tree b5) = (FlattenSeq b7) ^ <*b4*> ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines TerminalString DTCONSTR:def 15 :
for b1 being non empty DTConstrStr
for b2 being DecoratedTree of the carrier of b1 st b2 in TS b1 holds
for b3 being FinSequence of Terminals b1 holds
( b3 = TerminalString b2 iff ex b4 being Function of TS b1,(Terminals b1) * st
( b3 = b4 . b2 & ( for b5 being Symbol of b1 st b5 in Terminals b1 holds
b4 . (root-tree b5) = <*b5*> ) & ( for b5 being Symbol of b1
for b6 being FinSequence of TS b1 st b5 ==> roots b6 holds
b4 . (b5 -tree b6) = FlattenSeq (b4 * b6) ) ) );

:: deftheorem Def16 defines PreTraversal DTCONSTR:def 16 :
for b1 being non empty DTConstrStr
for b2 being DecoratedTree of the carrier of b1 st b2 in TS b1 holds
for b3 being FinSequence of the carrier of b1 holds
( b3 = PreTraversal b2 iff ex b4 being Function of TS b1,the carrier of b1 * st
( b3 = b4 . b2 & ( for b5 being Symbol of b1 st b5 in Terminals b1 holds
b4 . (root-tree b5) = <*b5*> ) & ( for b5 being Symbol of b1
for b6 being FinSequence of TS b1
for b7 being FinSequence st b7 = roots b6 & b5 ==> b7 holds
for b8 being FinSequence of the carrier of b1 * st b8 = b4 * b6 holds
b4 . (b5 -tree b6) = <*b5*> ^ (FlattenSeq b8) ) ) );

:: deftheorem Def17 defines PostTraversal DTCONSTR:def 17 :
for b1 being non empty DTConstrStr
for b2 being DecoratedTree of the carrier of b1 st b2 in TS b1 holds
for b3 being FinSequence of the carrier of b1 holds
( b3 = PostTraversal b2 iff ex b4 being Function of TS b1,the carrier of b1 * st
( b3 = b4 . b2 & ( for b5 being Symbol of b1 st b5 in Terminals b1 holds
b4 . (root-tree b5) = <*b5*> ) & ( for b5 being Symbol of b1
for b6 being FinSequence of TS b1
for b7 being FinSequence st b7 = roots b6 & b5 ==> b7 holds
for b8 being FinSequence of the carrier of b1 * st b8 = b4 * b6 holds
b4 . (b5 -tree b6) = (FlattenSeq b8) ^ <*b5*> ) ) );

definition
let c8 be non empty with_nonterminals DTConstrStr ;
let c9 be Symbol of c8;
func TerminalLanguage c2 -> Subset of ((Terminals a1) * ) equals :: DTCONSTR:def 18
{ (TerminalString b1) where B is Element of FinTrees the carrier of a1 : ( b1 in TS a1 & b1 . {} = a2 ) } ;
coherence
{ (TerminalString b1) where B is Element of FinTrees the carrier of c8 : ( b1 in TS c8 & b1 . {} = c9 ) } is Subset of ((Terminals c8) * )
proof end;
func PreTraversalLanguage c2 -> Subset of (the carrier of a1 * ) equals :: DTCONSTR:def 19
{ (PreTraversal b1) where B is Element of FinTrees the carrier of a1 : ( b1 in TS a1 & b1 . {} = a2 ) } ;
coherence
{ (PreTraversal b1) where B is Element of FinTrees the carrier of c8 : ( b1 in TS c8 & b1 . {} = c9 ) } is Subset of (the carrier of c8 * )
proof end;
func PostTraversalLanguage c2 -> Subset of (the carrier of a1 * ) equals :: DTCONSTR:def 20
{ (PostTraversal b1) where B is Element of FinTrees the carrier of a1 : ( b1 in TS a1 & b1 . {} = a2 ) } ;
coherence
{ (PostTraversal b1) where B is Element of FinTrees the carrier of c8 : ( b1 in TS c8 & b1 . {} = c9 ) } is Subset of (the carrier of c8 * )
proof end;
end;

:: deftheorem Def18 defines TerminalLanguage DTCONSTR:def 18 :
for b1 being non empty with_nonterminals DTConstrStr
for b2 being Symbol of b1 holds TerminalLanguage b2 = { (TerminalString b3) where B is Element of FinTrees the carrier of b1 : ( b3 in TS b1 & b3 . {} = b2 ) } ;

:: deftheorem Def19 defines PreTraversalLanguage DTCONSTR:def 19 :
for b1 being non empty with_nonterminals DTConstrStr
for b2 being Symbol of b1 holds PreTraversalLanguage b2 = { (PreTraversal b3) where B is Element of FinTrees the carrier of b1 : ( b3 in TS b1 & b3 . {} = b2 ) } ;

:: deftheorem Def20 defines PostTraversalLanguage DTCONSTR:def 20 :
for b1 being non empty with_nonterminals DTConstrStr
for b2 being Symbol of b1 holds PostTraversalLanguage b2 = { (PostTraversal b3) where B is Element of FinTrees the carrier of b1 : ( b3 in TS b1 & b3 . {} = b2 ) } ;

theorem Th14: :: DTCONSTR:14
for b1 being DecoratedTree of the carrier of PeanoNat st b1 in TS PeanoNat holds
TerminalString b1 = <*0*>
proof end;

theorem Th15: :: DTCONSTR:15
for b1 being Symbol of PeanoNat holds TerminalLanguage b1 = {<*0*>}
proof end;

theorem Th16: :: DTCONSTR:16
for b1 being Element of TS PeanoNat holds PreTraversal b1 = ((height (dom b1)) |-> 1) ^ <*0*>
proof end;

theorem Th17: :: DTCONSTR:17
for b1 being Symbol of PeanoNat holds
( ( b1 = 0 implies PreTraversalLanguage b1 = {<*0*>} ) & ( b1 = 1 implies PreTraversalLanguage b1 = { ((b2 |-> 1) ^ <*0*>) where B is Nat : b2 <> 0 } ) )
proof end;

theorem Th18: :: DTCONSTR:18
for b1 being Element of TS PeanoNat holds PostTraversal b1 = <*0*> ^ ((height (dom b1)) |-> 1)
proof end;

theorem Th19: :: DTCONSTR:19
for b1 being Symbol of PeanoNat holds
( ( b1 = 0 implies PostTraversalLanguage b1 = {<*0*>} ) & ( b1 = 1 implies PostTraversalLanguage b1 = { (<*0*> ^ (b2 |-> 1)) where B is Nat : b2 <> 0 } ) )
proof end;