let nt be Symbol of PeanoNat ; :: thesis: ( ( nt = 0 implies PostTraversalLanguage nt = {<*0 *>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) )
reconsider rtO = root-tree O as Element of TS PeanoNat ;
height (dom (root-tree 0 )) = 0 by TREES_1:79, TREES_4:3;
then PostTraversal rtO = <*0 *> ^ (0 |-> 1) by Th18;
then A1: PostTraversal rtO = <*O*> ^ {} by FINSEQ_2:72
.= <*O*> by FINSEQ_1:47 ;
thus ( nt = 0 implies PostTraversalLanguage nt = {<*0 *>} ) :: thesis: ( nt = 1 implies PostTraversalLanguage nt = { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } )

proof

assume A2: nt = 0 ; :: thesis: PostTraversalLanguage nt = {<*0 *>}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {<*0 *>} c= PostTraversalLanguage nt

let x be set ; :: thesis: ( x in PostTraversalLanguage nt implies x in {<*0 *>} )
assume x in PostTraversalLanguage nt ; :: thesis: x in {<*0 *>}
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A3: ( x = PostTraversal tsg & tsg in TS PeanoNat & tsg . {} = O ) by A2;
tsg = root-tree O by A3, Th9;
hence x in {<*0 *>} by A1, A3, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*0 *>} or x in PostTraversalLanguage nt )
assume x in {<*0 *>} ; :: thesis: x in PostTraversalLanguage nt
then A4: x = <*O*> by TARSKI:def 1;
rtO . {} = O by TREES_4:3;
hence x in PostTraversalLanguage nt by A1, A2, A4; :: thesis: verum

end;

assume A5: nt = 1 ; :: thesis: PostTraversalLanguage nt = { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } c= PostTraversalLanguage nt

let x be set ; :: thesis: ( x in PostTraversalLanguage nt implies x in { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } )
assume x in PostTraversalLanguage nt ; :: thesis: x in { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 }
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A6: ( x = PostTraversal tsg & tsg in TS PeanoNat & tsg . {} = S ) by A5;
consider ts being FinSequence of TS PeanoNat such that
A7: ( tsg = S -tree ts & S ==> roots ts ) by A6, Th10;
( roots ts = <*0 *> or roots ts = <*1*> ) by A7, Def5;
then len (roots ts) = 1 by FINSEQ_1:57;
then consider t being Element of FinTrees the carrier of PeanoNat such that
A8: ( ts = <*t*> & t in TS PeanoNat ) by Th5;
tsg = S -tree t by A7, A8, TREES_4:def 5;
then dom tsg = ^ (dom t) by TREES_4:13;
then height (dom tsg) = (height (dom t)) + 1 by TREES_3:83;
then ( height (dom tsg) <> 0 & x = <*0 *> ^ ((height (dom tsg)) |-> 1) ) by A6, Th18;
hence x in { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } or x in PostTraversalLanguage nt )
assume x in { (<*0 *> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ; :: thesis: x in PostTraversalLanguage nt
then consider n being Element of NAT such that
A9: ( x = <*0 *> ^ (n |-> 1) & n <> 0 ) ;
defpred S₂[ Element of NAT ] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0 *> ^ ($1 |-> 1) ) );
A10: S₂[ 0 ] ;

A11: now

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A12: S₂[n] ; :: thesis: S₂[n + 1]
thus S₂[n + 1] :: thesis: verum

proof

assume n + 1 <> 0 ; :: thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0 *> ^ ((n + 1) |-> 1) )

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0 *> ^ ((n + 1) |-> 1) )

then consider tsg being Element of TS PeanoNat such that
A13: ( tsg . {} = S & PostTraversal tsg = <*0 *> ^ (n |-> 1) ) by A12;
PostTraversal tsg = <*0 *> ^ ((height (dom tsg)) |-> 1) by Th18;
then ( n |-> 1 = (height (dom tsg)) |-> 1 & len (n |-> 1) = n ) by A13, FINSEQ_1:46, FINSEQ_1:def 18;
then A14: height (dom tsg) = n by FINSEQ_1:def 18;
take tsg' = S -tree tsg; :: thesis: ( tsg' . {} = S & PostTraversal tsg' = <*0 *> ^ ((n + 1) |-> 1) )
A15: tsg' = S -tree <*tsg*> by TREES_4:def 5;
height (dom tsg') = height (^ (dom tsg)) by TREES_4:13
.= n + 1 by A14, TREES_3:83 ;
hence ( tsg' . {} = S & PostTraversal tsg' = <*0 *> ^ ((n + 1) |-> 1) ) by A15, Th18, TREES_4:def 4; :: thesis: verum

end;

suppose A16: n = 0 ; :: thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0 *> ^ ((n + 1) |-> 1) )

take tsg' = S -tree rtO; :: thesis: ( tsg' . {} = S & PostTraversal tsg' = <*0 *> ^ ((n + 1) |-> 1) )
A17: tsg' = S -tree <*rtO*> by TREES_4:def 5;
height (dom tsg') = height (^ (dom rtO)) by TREES_4:13
.= (height (dom rtO)) + 1 by TREES_3:83
.= n + 1 by A16, TREES_1:79, TREES_4:3 ;
hence ( tsg' . {} = S & PostTraversal tsg' = <*0 *> ^ ((n + 1) |-> 1) ) by A17, Th18, TREES_4:def 4; :: thesis: verum

end;

end;

end;

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A10, A11);
then ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0 *> ^ (n |-> 1) ) by A9;
hence x in PostTraversalLanguage nt by A5, A9; :: thesis: verum