:: DTCONSTR semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

theorem Th1: :: DTCONSTR:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being FinSequence of FinTrees D holds p is FinSequence of Trees D
proof end;

theorem Th2: :: DTCONSTR:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for p being FinSequence of x st y in dom p holds
p . y in x
proof end;

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

registration
let D be non empty set ;
let T be DTree-set of D;
cluster -> DTree-yielding FinSequence of T;
coherence
for b1 being FinSequence of T holds b1 is DTree-yielding
proof end;
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;
:: original: Element
redefine mode Element of Tset -> Element of F;
coherence
for b1 being Element of Tset holds b1 is Element of F
proof end;
end;

definition
let D be non empty set ;
let T be DTree-set of D;
let p be FinSequence of T;
:: original: roots
redefine func roots p -> FinSequence of D;
coherence
roots p is FinSequence of D
proof end;
end;

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

theorem Th3: :: DTCONSTR:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
roots {} = {} by Lm1, FINSEQ_1:26;

theorem Th4: :: DTCONSTR:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being DecoratedTree holds roots <*T*> = <*(T . {} )*>
proof end;

theorem Th5: :: DTCONSTR:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being Subset of (FinTrees D)
for p being FinSequence of F st len (roots p) = 1 holds
ex x being Element of FinTrees D st
( p = <*x*> & x in F )
proof end;

theorem :: DTCONSTR:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being DecoratedTree holds roots <*T1,T2*> = <*(T1 . {} ),(T2 . {} )*>
proof end;

definition
let X, Y be set ;
let f be FinSequence of [:X,Y:];
:: original: pr1
redefine func pr1 f -> FinSequence of X;
coherence
pr1 f is FinSequence of X
proof end;
:: original: pr2
redefine func pr2 f -> FinSequence of Y;
coherence
pr2 f is FinSequence of Y
proof end;
end;

theorem Th7: :: DTCONSTR:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( pr1 {} = {} & pr2 {} = {} )
proof end;

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

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

scheme :: DTCONSTR:sch 2
DTConstrStrUniq{ F1() -> non empty set , P1[ set , set ] } :
for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = F1() & ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P1[x,p] ) ) & the carrier of G2 = F1() & ( for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff P1[x,p] ) ) holds
G1 = G2
proof end;

theorem :: DTCONSTR:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty DTConstrStr holds Terminals G misses NonTerminals G
proof end;

scheme :: DTCONSTR:sch 3
DTCMin{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex X being Subset of (FinTrees [:the carrier of F2(),F3():]) st
( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [:the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{} ,{} ) ) ) } and
A3: for n being Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof end;

scheme :: DTCONSTR:sch 4
DTCSymbols{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex X1 being Subset of (FinTrees the carrier of F2()) st
( X1 = { (t `1 ) where t is Element of FinTrees [:the carrier of F2(),F3():] : t in Union F1() } & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in X1 ) & ( for o being Symbol of F2()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{} ,{} ) ) ) } and
A3: for n being Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof end;

scheme :: DTCONSTR:sch 5
DTCHeight{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for n being Nat
for dt being Element of FinTrees [:the carrier of F2(),F3():] st dt in Union F1() holds
( dt in F1() . n iff height (dom dt) <= n )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{} ,{} ) ) ) } and
A3: for n being Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof end;

scheme :: DTCONSTR:sch 6
DTCUniq{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for dt1, dt2 being DecoratedTree of [:the carrier of F2(),F3():] st dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 holds
dt1 = dt2
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{} ,{} ) ) ) } and
A3: for n being Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [:the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof end;

definition
let G be non empty DTConstrStr ;
canceled;
canceled;
canceled;
func TS G -> Subset of (FinTrees the carrier of G) means :Def4: :: DTCONSTR:def 4
( ( for d being Symbol of G st d in Terminals G holds
root-tree d in it ) & ( for o being Symbol of G
for 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
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
it c= F ) );
existence
ex b1 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 b1 ) & ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) & ( 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
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b1 c= F ) )
proof end;
uniqueness
for b1, b2 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 b1 ) & ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) & ( 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
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) & ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) & ( 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
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b2 c= F ) holds
b1 = b2
proof end;
end;

:: deftheorem DTCONSTR:def 1 :
canceled;

:: deftheorem DTCONSTR:def 2 :
canceled;

:: deftheorem DTCONSTR:def 3 :
canceled;

:: deftheorem Def4 defines TS DTCONSTR:def 4 :
for G being non empty DTConstrStr
for b2 being Subset of (FinTrees the carrier of G) holds
( b2 = TS G iff ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) & ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) & ( 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
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b2 c= F ) ) );

scheme :: DTCONSTR:sch 7
DTConstrInd{ F1() -> non empty DTConstrStr , P1[ set ] } :
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
P1[t]
provided
A1: for s being Symbol of F1() st s in Terminals F1() holds
P1[ root-tree s] and
A2: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof end;

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

scheme :: DTCONSTR:sch 9
DTConstrUniqDef{ 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
A1: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F5() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F5() . (nt -tree ts) = F4(nt,(roots ts),(F5() * ts)) ) ) and
A2: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F6() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F6() . (nt -tree ts) = F4(nt,(roots ts),(F6() * ts)) ) )
proof end;

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

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

set PN = PeanoNat ;

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

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

Lm3: ( S ==> <*O*> & S ==> <*S*> )
by Def5;

Lm4: S ==> <*O*>
by Def5;

Lm5: S ==> <*S*>
by Def5;

Lm6: Terminals PeanoNat = { x where x is Symbol of PeanoNat : for tnt being FinSequence holds not x ==> tnt }
by LANG1:def 2;

Lm7: now
given x being FinSequence such that A1: O ==> x ; :: thesis: contradiction
[O,x] in the Rules of PeanoNat by A1, LANG1:def 1;
then x in the carrier of PeanoNat * by ZFMISC_1:106;
then x is FinSequence of the carrier of PeanoNat by FINSEQ_2:def 3;
hence contradiction by A1, Def5; :: thesis: verum
end;

then Lm8: O in Terminals PeanoNat
by Lm6;

Lm9: Terminals PeanoNat c= {O}
proof end;

Lm10: NonTerminals PeanoNat = { x where x is Symbol of PeanoNat : ex tnt being FinSequence st x ==> tnt }
by LANG1:def 3;

then Lm11: S in NonTerminals PeanoNat
by Lm4;

then Lm12: {S} c= NonTerminals PeanoNat
by ZFMISC_1:37;

Lm13: NonTerminals PeanoNat c= {S}
proof end;

then Lm14: NonTerminals PeanoNat = {S}
by Lm12, XBOOLE_0:def 10;

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

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

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

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

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

Lm15: ( 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 Lm15;
end;

definition
let G be non empty with_terminals DTConstrStr ;
:: original: Terminals
redefine func Terminals G -> non empty Subset of G;
coherence
Terminals G is non empty Subset of G
proof end;
end;

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

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

definition
let G be non empty with_nonterminals DTConstrStr ;
:: original: NonTerminals
redefine func NonTerminals G -> non empty Subset of G;
coherence
NonTerminals G is non empty Subset of G
proof end;
end;

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

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

definition
let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let nt be NonTerminal of G;
mode SubtreeSeq of nt -> FinSequence of TS G means :Def9: :: DTCONSTR:def 9
nt ==> roots it;
existence
ex b1 being FinSequence of TS G st nt ==> roots b1 by Def8;
end;

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

definition
let G be non empty with_terminals DTConstrStr ;
let t be Terminal of G;
:: original: root-tree
redefine func root-tree t -> Element of TS G;
coherence
root-tree t is Element of TS G by Def4;
end;

definition
let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let nt be NonTerminal of G;
let p be SubtreeSeq of nt;
:: original: -tree
redefine func nt -tree p -> Element of TS G;
coherence
nt -tree p is Element of TS G
proof end;
end;

theorem Th9: :: DTCONSTR:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty with_terminals DTConstrStr
for tsg being Element of TS G
for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s
proof end;

theorem Th10: :: DTCONSTR:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty with_terminals with_nonterminals DTConstrStr
for tsg being Element of TS G
for nt being NonTerminal of G st tsg . {} = nt holds
ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts )
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 Lm15;
end;

set PN = PeanoNat ;

reconsider O = O as Terminal of PeanoNat by Lm8;

reconsider S = S as NonTerminal of PeanoNat by Lm11;

definition
let nt be NonTerminal of PeanoNat ;
let t be Element of TS PeanoNat ;
:: original: -tree
redefine func nt -tree t -> Element of TS PeanoNat ;
coherence
nt -tree t is Element of TS PeanoNat
proof end;
end;

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

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

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

definition
func PN-to-NAT -> Function of TS PeanoNat , NAT means :Def11: :: DTCONSTR:def 11
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it . (nt -tree ts) = plus-one (it * ts) ) );
existence
ex b1 being Function of TS PeanoNat , NAT st
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) )
proof end;
uniqueness
for b1, b2 being Function of TS PeanoNat , NAT st ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b2 . (nt -tree ts) = plus-one (b2 * ts) ) 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 t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) ) );

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

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

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

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

theorem :: DTCONSTR:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn)
proof end;

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

Lm17: now
let n be Nat; :: thesis: ( n = PN-to-NAT . (NAT-to-PN . n) implies n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) )
assume A1: n = PN-to-NAT . (NAT-to-PN . n) ; :: thesis: n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1))
reconsider dt = NAT-to-PN . n as Element of TS PeanoNat ;
reconsider r = {} as Node of dt by TREES_1:47;
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 Def13
.= S -tree <*(NAT-to-PN . n)*> ;
A4: S ==> roots <*(NAT-to-PN . n)*> by A2, Lm3, Th4;
consider k being Nat such that
A5: ( plus-one <*n*> = k + 1 & <*n*> . 1 = k ) by Def10;
<*(PN-to-NAT . (NAT-to-PN . n))*> = PN-to-NAT * <*(NAT-to-PN . n)*> by FINSEQ_2:39;
then PN-to-NAT . (S -tree <*(NAT-to-PN . n)*>) = plus-one <*n*> by A1, A4, Def11
.= n + 1 by A5, FINSEQ_1:57 ;
hence n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) by A3; :: thesis: verum
end;

theorem :: DTCONSTR:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds n = PN-to-NAT . (NAT-to-PN . n)
proof end;

definition
let D be set ;
let F be FinSequence of D * ;
func FlattenSeq F -> Element of D * means :Def14: :: DTCONSTR:def 14
 ex g being BinOp of D * st
( ( for p, q being Element of D * holds g . p,q = p ^ q ) & it = g "**" F );
existence
ex b1 being Element of D * ex g being BinOp of D * st
( ( for p, q being Element of D * holds g . p,q = p ^ q ) & b1 = g "**" F )
proof end;
uniqueness
for b1, b2 being Element of D * st ex g being BinOp of D * st
( ( for p, q being Element of D * holds g . p,q = p ^ q ) & b1 = g "**" F ) & ex g being BinOp of D * st
( ( for p, q being Element of D * holds g . p,q = p ^ q ) & b2 = g "**" F ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines FlattenSeq DTCONSTR:def 14 :
for D being set
for F being FinSequence of D *
for b3 being Element of D * holds
( b3 = FlattenSeq F iff ex g being BinOp of D * st
( ( for p, q being Element of D * holds g . p,q = p ^ q ) & b3 = g "**" F ) );

theorem Th13: :: DTCONSTR:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for d being Element of D * holds FlattenSeq <*d*> = d
proof end;

definition
let G be non empty DTConstrStr ;
let tsg be DecoratedTree of the carrier of G;
assume A1: tsg in TS G ;
defpred S2[ set ] means $1 in Terminals G;
deffunc H5( set ) -> set = <*$1*>;
deffunc H6( set ) -> set = {} ;
A2: now
let x be set ; :: thesis: ( x in the carrier of G implies ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) ) )
assume x in the carrier of G ; :: thesis: ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) )
hereby :: thesis: ( not S2[x] implies H6(x) in (Terminals G) * )
assume A3: S2[x] ; :: thesis: H5(x) in (Terminals G) *
then reconsider T = Terminals G as non empty set ;
reconsider x' = x as Element of T by A3;
<*x'*> is FinSequence of T ;
hence H5(x) in (Terminals G) * ; :: thesis: verum
end;
assume not S2[x] ; :: thesis: H6(x) in (Terminals G) *
{} is FinSequence of Terminals G by FINSEQ_1:29;
hence H6(x) in (Terminals G) * by FINSEQ_1:def 11; :: thesis: verum
end;
consider s2t being Function of the carrier of G,(Terminals G) * such that
A4: for s being set st s in the carrier of G holds
( ( S2[s] implies s2t . s = H5(s) ) & ( not S2[s] implies s2t . s = H6(s) ) ) from FUNCT_2:sch 9( the carrier of nt (Terminals nt) * , A2);
deffunc H7( Symbol of G) -> Element of (Terminals G) * = s2t . $1;
deffunc H8( set , set , FinSequence of (Terminals G) * ) -> Element of (Terminals G) * = FlattenSeq $3;
deffunc H9( set ) -> set = <*$1*>;
func TerminalString tsg -> FinSequence of Terminals G means :Def15: :: DTCONSTR:def 15
 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
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) );
existence
ex b1 being FinSequence of Terminals G ex f being Function of TS G,(Terminals G) * st
( b1 = 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
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of Terminals G st ex f being Function of TS G,(Terminals G) * st
( b1 = 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
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) & ex f being Function of TS G,(Terminals G) * st
( b2 = 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
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) holds
b1 = b2
proof end;
A13: now
let x be set ; :: thesis: ( x in the carrier of G implies H9(x) in the carrier of G * )
assume x in the carrier of G ; :: thesis: H9(x) in the carrier of G *
then reconsider x' = x as Element of G ;
<*x'*> is FinSequence of the carrier of G ;
hence H9(x) in the carrier of G * ; :: thesis: verum
end;
consider s2s being Function of the carrier of G,the carrier of G * such that
A14: for s being set st s in the carrier of G holds
s2s . s = H9(s) from FUNCT_2:sch 2( the carrier of nt the carrier of nt * , A13);
deffunc H10( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H11( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3);
func PreTraversal tsg -> FinSequence of the carrier of G means :Def16: :: DTCONSTR:def 16
 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) );
existence
ex b1 being FinSequence of the carrier of G ex f being Function of TS G,the carrier of G * st
( b1 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of G st ex f being Function of TS G,the carrier of G * st
( b1 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) & ex f being Function of TS G,the carrier of G * st
( b2 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) holds
b1 = b2
proof end;
deffunc H12( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H13( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (FlattenSeq $3) ^ (s2s . $1);
func PostTraversal tsg -> FinSequence of the carrier of G means :Def17: :: DTCONSTR:def 17
 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) );
existence
ex b1 being FinSequence of the carrier of G ex f being Function of TS G,the carrier of G * st
( b1 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of G st ex f being Function of TS G,the carrier of G * st
( b1 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) & ex f being Function of TS G,the carrier of G * st
( b2 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines TerminalString DTCONSTR:def 15 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of Terminals G holds
( b3 = TerminalString tsg iff ex f being Function of TS G,(Terminals G) * st
( b3 = 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
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) );

:: deftheorem Def16 defines PreTraversal DTCONSTR:def 16 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of the carrier of G holds
( b3 = PreTraversal tsg iff ex f being Function of TS G,the carrier of G * st
( b3 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) );

:: deftheorem Def17 defines PostTraversal DTCONSTR:def 17 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of the carrier of G holds
( b3 = PostTraversal tsg iff ex f being Function of TS G,the carrier of G * st
( b3 = 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
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) );

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

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

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

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

theorem Th14: :: DTCONSTR:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
TerminalString t = <*0*>
proof end;

theorem :: DTCONSTR:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}
proof end;

theorem Th16: :: DTCONSTR:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t being Element of TS PeanoNat holds PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
proof end;

theorem :: DTCONSTR:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nt being Symbol of PeanoNat holds
( ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Nat : n <> 0 } ) )
proof end;

theorem Th18: :: DTCONSTR:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t being Element of TS PeanoNat holds PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
proof end;

theorem :: DTCONSTR:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nt being Symbol of PeanoNat holds
( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Nat : n <> 0 } ) )
proof end;