:: DTCONSTR  semantic presentation begin  
theorem :: DTCONSTR:1 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set (Var "D"))) "holds"  (Bool (Set (Var "p")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_trees_3 :::"Trees"::: )  (Set (Var "D")))))) ; 
 
theorem :: DTCONSTR:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "x"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "x"))))) ; 
 registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be    ($#m1_trees_3 :::"DTree-set"::: )   "of" (Set (Const "D")); 
cluster   ->   ($#v6_trees_3 :::"DTree-yielding"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" "T"; 
end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "F" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_trees_3 :::"DTree-set"::: )   "of" (Set (Const "D")); let "Tset" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "F")); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "Tset" ->    ($#m1_subset_1 :::"Element"::: )   "of" "F"; end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be    ($#m1_trees_3 :::"DTree-set"::: )   "of" (Set (Const "D")); let "p" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "T")); :: original: :::"roots"::: redefine func  :::"roots"::: "p" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D"; end; 
theorem :: DTCONSTR:3 (Bool (Set   ($#k14_trees_3 :::"roots"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 
theorem :: DTCONSTR:4 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set   ($#k14_trees_3 :::"roots"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: DTCONSTR:5 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set (Var "D")) ")" )  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set (Var "D"))) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "x")) ($#k3_pre_poly :::"*>"::: ) )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ))))) ; 
 
theorem :: DTCONSTR:6 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set   ($#k14_trees_3 :::"roots"::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k10_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "T1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "," (Set  "(" (Set (Var "T2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) ; 
 definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "Y")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"pr1"::: redefine func  :::"pr1"::: "f" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "X"; :: original: :::"pr2"::: redefine func  :::"pr2"::: "f" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "Y"; end; 
theorem :: DTCONSTR:7 (Bool  "("  (Bool (Set   ($#k11_mcart_1 :::"pr1"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k12_mcart_1 :::"pr2"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ) ; 
 begin  registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")) "," (Set  "(" (Set (Const "A"))  ($#k3_finseq_2 :::"*"::: )  ")" ); 
cluster (Set   ($#g1_lang1 :::"DTConstrStr"::: )  "(#"  "A" "," "R" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; scheme  :: DTCONSTR:sch 1 DTConstrStrEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )     ($#l1_lang1 :::"DTConstrStr"::: )   "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "p"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "p"))])  ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: DTCONSTR:sch 2 DTConstrStrUniq{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G1")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G1"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G1"))) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "p"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "p"))])  ")" ))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G2")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G2"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G2"))) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "p"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "p"))])  ")" ))  ")" )) "holds"  (Bool (Set (Var "G1"))  ($#r1_hidden :::"="::: )  (Set (Var "G2"))))
 proof 


end; 
theorem :: DTCONSTR:8 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_lang1 :::"NonTerminals"::: )  (Set (Var "G"))))) ; 
 scheme  :: DTCONSTR:sch 3 DTCMin{ F1() ->   ($#m1_hidden :::"Function":::), F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) } : 
(Bool  "ex" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F1 "("  ")" ))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" )))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set F4 "(" (Set (Var "d")) ")" ) ($#k1_domain_1 :::"]"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" )))) "holds"  (Bool (Set (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o")) "," (Set F5 "(" (Set (Var "o")) "," (Set  "("  ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) "," (Set  "("  ($#k3_dtconstr :::"pr2"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" ) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" )))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set F4 "(" (Set (Var "d")) ")" ) ($#k1_domain_1 :::"]"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" )))) "holds"  (Bool (Set (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o")) "," (Set F5 "(" (Set (Var "o")) "," (Set  "("  ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) "," (Set  "("  ($#k3_dtconstr :::"pr2"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "F")))  ")" )  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ")" ) where t "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool  "("  (Bool  "("  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" ))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "t")) ")" ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "t"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "t")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ))  ")" )  ")" )  "}"  )
 and  
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  "(" (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o")) "," (Set F5 "(" (Set (Var "o")) "," (Set  "("  ($#k11_mcart_1 :::"pr1"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) "," (Set  "("  ($#k12_mcart_1 :::"pr2"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p")) ")" ) where o "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), p "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "q")) ")" )))  ")" ))  "}"  )))
 proof 


end; scheme  :: DTCONSTR:sch 4 DTCSymbols{ F1() ->   ($#m1_hidden :::"Function":::), F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) } : 
(Bool  "ex" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) ")" ) "st"  (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k8_trees_3 :::"`1"::: )  ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) : (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F1 "("  ")" )))  "}"  ) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" )))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "d")))  ($#r2_hidden :::"in"::: )  (Set (Var "X1")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "X1"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "X1"))))  ")" ) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" )))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "d")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))  ")" )) "holds"  (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set (Var "F")))  ")" )  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ")" ) where t "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool  "("  (Bool  "("  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" ))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "t")) ")" ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "t"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "t")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ))  ")" )  ")" )  "}"  )
 and  
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  "(" (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o")) "," (Set F5 "(" (Set (Var "o")) "," (Set  "("  ($#k11_mcart_1 :::"pr1"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) "," (Set  "("  ($#k12_mcart_1 :::"pr2"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p")) ")" ) where o "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), p "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "q")) ")" )))  ")" ))  "}"  )))
 proof 


end; scheme  :: DTCONSTR:sch 5 DTCHeight{ F1() ->   ($#m1_hidden :::"Function":::), F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) } : 
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "dt")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))  "st" (Bool (Bool (Set (Var "dt"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F1 "("  ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "dt"))  ($#r2_hidden :::"in"::: )  (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) "iff" (Bool (Set   ($#k6_trees_1 :::"height"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "dt")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ")" ) where t "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool  "("  (Bool  "("  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" ))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "t")) ")" ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "t"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "t")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ))  ")" )  ")" )  "}"  )
 and  
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  "(" (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o")) "," (Set F5 "(" (Set (Var "o")) "," (Set  "("  ($#k11_mcart_1 :::"pr1"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) "," (Set  "("  ($#k12_mcart_1 :::"pr2"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p")) ")" ) where o "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), p "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "q")) ")" )))  ")" ))  "}"  )))
 proof 


end; scheme  :: DTCONSTR:sch 6 DTCUniq{ F1() ->   ($#m1_hidden :::"Function":::), F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) } : 
(Bool  "for" (Set (Var "dt1")) "," (Set (Var "dt2")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "dt1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "dt2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "dt1"))  ($#k8_trees_3 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "dt2"))  ($#k8_trees_3 :::"`1"::: )  ))) "holds"  (Bool (Set (Var "dt1"))  ($#r1_hidden :::"="::: )  (Set (Var "dt2"))))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ")" ) where t "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool  "("  (Bool  "("  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F2 "("  ")" ))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "t")) ")" ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "t"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "t")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ))  ")" )  ")" )  "}"  )
 and  
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  "(" (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o")) "," (Set F5 "(" (Set (Var "o")) "," (Set  "("  ($#k11_mcart_1 :::"pr1"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) "," (Set  "("  ($#k12_mcart_1 :::"pr2"::: )  (Set  "("  ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p")) ")" ) where o "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F2 "("  ")" ), p "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" )) "," (Set F3 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k2_dtconstr :::"pr1"::: )  (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "q")) ")" )))  ")" ))  "}"  )))
 proof 


end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; func  :::"TS"::: "G" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") ")" ) means :: DTCONSTR:def 1 (Bool  "("  (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "G"))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "d")))  ($#r2_hidden :::"in"::: )  it)  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" it  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  it))  ")" ) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "G"))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "d")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))  ")" )) "holds"  (Bool it  ($#r1_tarski :::"c="::: )  (Set (Var "F")))  ")" )  ")" ); end; 





:: deftheorem    defines :::"TS"::: DTCONSTR:def 1 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "d")))  ($#r2_hidden :::"in"::: )  (Set (Var "b2")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "b2"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))))  ")" ) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "d")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))  ")" )) "holds"  (Bool (Set (Var "b2"))  ($#r1_tarski :::"c="::: )  (Set (Var "F")))  ")" )  ")" )  ")" ))); 
 scheme  :: DTCONSTR:sch 7 DTConstrInd{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" )))) "holds"  (Bool P1[(Set (Var "t"))]))
 provided
(Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F1 "("  ")" )))) "holds"  (Bool P1[(Set   ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")))]))
 and  
(Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")))) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "ts"))))) "holds"  (Bool P1[(Set (Var "t"))])  ")" )) "holds"  (Bool P1[(Set (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")))])))
 proof 


end; scheme  :: DTCONSTR:sch 8 DTConstrIndDef{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ), F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ) ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "t")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "nt")) "," (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ) ")" )))  ")" )  ")" ))
 proof 


end; scheme  :: DTCONSTR:sch 9 DTConstrUniqDef{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ), F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ), F5() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ) ")" ) "," (Set F2 "("  ")" ), F6() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ) ")" ) "," (Set F2 "("  ")" ) } : 
(Bool (Set F5 "("  ")" )  ($#r2_funct_2 :::"="::: )  (Set F6 "("  ")" ))
 provided
(Bool  "("  (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "t")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "nt")) "," (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")) ")" ) "," (Set  "(" (Set F5 "("  ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ) ")" )))  ")" )  ")" )
 and  
(Bool  "("  (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set F6 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "t")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set F1 "("  ")" ))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set F6 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "nt")) "," (Set  "("  ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")) ")" ) "," (Set  "(" (Set F6 "("  ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ) ")" )))  ")" )  ")" )
 proof 


end; begin  definitionfunc  :::"PeanoNat":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )     ($#l1_lang1 :::"DTConstrStr"::: )   means :: DTCONSTR:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" it  (Bool  "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Num 1) ($#k3_pre_poly :::"*>"::: ) ))  ")" )  ")" )  ")" ))  ")" )  ")" ); end; 




:: deftheorem    defines :::"PeanoNat"::: DTCONSTR:def 2 :  (Bool  "for" (Set (Var "b1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )     ($#l1_lang1 :::"DTConstrStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_dtconstr :::"PeanoNat"::: )  )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "b1"))  (Bool  "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b1"))) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Num 1) ($#k3_pre_poly :::"*>"::: ) ))  ")" )  ")" )  ")" ))  ")" )  ")" )  ")" )); 
 begin  definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; attr "G" is  :::"with_terminals":::  means :: DTCONSTR:def 3 (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  "G")  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); attr "G" is  :::"with_nonterminals":::  means :: DTCONSTR:def 4 (Bool (Set   ($#k2_lang1 :::"NonTerminals"::: )  "G")  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); attr "G" is  :::"with_useful_nonterminals":::  means :: DTCONSTR:def 5 (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  "st" (Bool (Bool (Set (Var "nt"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_lang1 :::"NonTerminals"::: )  "G"))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G") "st" (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p")))))); end; 












:: deftheorem    defines :::"with_terminals"::: DTCONSTR:def 3 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_dtconstr :::"with_terminals"::: )  ) "iff" (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"with_nonterminals"::: DTCONSTR:def 4 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v2_dtconstr :::"with_nonterminals"::: )  ) "iff" (Bool (Set   ($#k2_lang1 :::"NonTerminals"::: )  (Set (Var "G")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"with_useful_nonterminals"::: DTCONSTR:def 5 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v3_dtconstr :::"with_useful_nonterminals"::: )  ) "iff" (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "nt"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_lang1 :::"NonTerminals"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G"))) "st" (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "p"))))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )     ($#v1_dtconstr :::"with_terminals"::: )     ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )    for    ($#l1_lang1 :::"DTConstrStr"::: )  ; 
end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_dtconstr :::"with_terminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; :: original: :::"Terminals"::: redefine func  :::"Terminals"::: "G" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "G"; end; registrationlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_dtconstr :::"with_terminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; 
cluster (Set   ($#k4_dtconstr :::"TS"::: )  "G") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_dtconstr :::"with_useful_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; 
cluster (Set   ($#k4_dtconstr :::"TS"::: )  "G") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; :: original: :::"NonTerminals"::: redefine func  :::"NonTerminals"::: "G" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "G"; end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_dtconstr :::"with_terminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; mode Terminal of "G" is    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k6_dtconstr :::"Terminals"::: )  "G"); end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; mode NonTerminal of "G" is    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_dtconstr :::"NonTerminals"::: )  "G"); end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; let "nt" be   ($#m2_subset_1 :::"NonTerminal":::) "of" (Set (Const "G")); mode  :::"SubtreeSeq":::  "of" "nt" ->    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G") means :: DTCONSTR:def 6 (Bool "nt"  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  it)); end; 






:: deftheorem    defines :::"SubtreeSeq"::: DTCONSTR:def 6 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "nt")) "being"   ($#m2_subset_1 :::"NonTerminal":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m2_dtconstr :::"SubtreeSeq"::: )   "of" (Set (Var "nt"))) "iff" (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "b3"))))  ")" )))); 
 definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_dtconstr :::"with_terminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; let "t" be   ($#m2_subset_1 :::"Terminal":::) "of" (Set (Const "G")); :: original: :::"root-tree"::: redefine func  :::"root-tree"::: "t" ->    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G"); end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; let "nt" be   ($#m2_subset_1 :::"NonTerminal":::) "of" (Set (Const "G")); let "p" be    ($#m2_dtconstr :::"SubtreeSeq"::: )   "of" (Set (Const "nt")); :: original: :::"-tree"::: redefine func "nt" :::"-tree"::: "p" ->    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G"); end; 
theorem :: DTCONSTR:9 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_dtconstr :::"with_terminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "tsg")) "being"    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "s")) "being"   ($#m2_subset_1 :::"Terminal":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) "holds"  (Bool (Set (Var "tsg"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_dtconstr :::"root-tree"::: )  (Set (Var "s"))))))) ; 
 
theorem :: DTCONSTR:10 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_dtconstr :::"with_terminals"::: )     ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "tsg")) "being"    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "nt")) "being"   ($#m2_subset_1 :::"NonTerminal":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "nt")))) "holds"  (Bool  "ex" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "tsg"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")))) & (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))  ")" ))))) ; 
 begin  registration
cluster (Set   ($#k5_dtconstr :::"PeanoNat"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )     ($#v1_dtconstr :::"with_terminals"::: )     ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )   ; 
end; definitionlet "nt" be   ($#m2_subset_1 :::"NonTerminal":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ); let "t" be    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )); :: original: :::"-tree"::: redefine func "nt" :::"-tree"::: "t" ->    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )); end; definitionlet "x" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"plus-one"::: "x" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: DTCONSTR:def 7 (Set (Set  "(" "x"  ($#k1_funct_1 :::"."::: )  (Num 1) ")" )  ($#k1_nat_1 :::"+"::: )  (Num 1)); end; 





:: deftheorem    defines :::"plus-one"::: DTCONSTR:def 7 :  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k11_dtconstr :::"plus-one"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_funct_1 :::"."::: )  (Num 1) ")" )  ($#k1_nat_1 :::"+"::: )  (Num 1)))); 
 definitionfunc  :::"PN-to-NAT":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) means :: DTCONSTR:def 8 (Bool  "("  (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_dtconstr :::"Terminals"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_dtconstr :::"plus-one"::: )  (Set  "(" it  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ))))  ")" )  ")" ); end; 




:: deftheorem    defines :::"PN-to-NAT"::: DTCONSTR:def 8 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_dtconstr :::"PN-to-NAT"::: )  )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_dtconstr :::"Terminals"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_dtconstr :::"plus-one"::: )  (Set  "(" (Set (Var "b1"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ))))  ")" )  ")" )  ")" )); 
 definitionlet "x" be    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )); func  :::"PNsucc"::: "x" ->    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )) equals :: DTCONSTR:def 9 (Set (Num 1)  ($#k4_trees_4 :::"-tree"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) "x" ($#k3_pre_poly :::"*>"::: ) )); end; 





:: deftheorem    defines :::"PNsucc"::: DTCONSTR:def 9 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )) "holds"  (Bool (Set   ($#k13_dtconstr :::"PNsucc"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k4_trees_4 :::"-tree"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "x")) ($#k3_pre_poly :::"*>"::: ) )))); 
 definitionfunc  :::"NAT-to-PN":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) ")" ) means :: DTCONSTR:def 10 (Bool  "("  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_dtconstr :::"PNsucc"::: )  (Set  "(" it  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" ); end; 




:: deftheorem    defines :::"NAT-to-PN"::: DTCONSTR:def 10 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_dtconstr :::"NAT-to-PN"::: )  )) "iff" (Bool  "("  (Bool (Set (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_4 :::"root-tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_dtconstr :::"PNsucc"::: )  (Set  "(" (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" )  ")" )); 
 
theorem :: DTCONSTR:11 (Bool  "for" (Set (Var "pn")) "being"    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )) "holds"  (Bool (Set (Var "pn"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k14_dtconstr :::"NAT-to-PN"::: ) )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set  ($#k12_dtconstr :::"PN-to-NAT"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "pn")) ")" )))) ; 
 
theorem :: DTCONSTR:12 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_dtconstr :::"PN-to-NAT"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k14_dtconstr :::"NAT-to-PN"::: ) )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))) ; 
 begin  definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; let "tsg" be   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "G"))); assume 
(Bool (Set (Const "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Const "G"))))
 ; func  :::"TerminalString"::: "tsg" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_lang1 :::"Terminals"::: )  "G") means :: DTCONSTR:def 11 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  "G" ")" ) "," (Set  "(" (Set  "("  ($#k1_lang1 :::"Terminals"::: )  "G" ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  "tsg")) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G")  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_pre_poly :::"FlattenSeq"::: )  (Set  "(" (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ))))  ")" )  ")" )); func  :::"PreTraversal"::: "tsg" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") means :: DTCONSTR:def 12 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  "G" ")" ) "," (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  ")" ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  "tsg")) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G")  (Bool  "for" (Set (Var "rts")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "rts"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")))) & (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "rts")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "nt")) ($#k3_pre_poly :::"*>"::: ) )  ($#k1_pre_poly :::"^"::: )  (Set  "("  ($#k5_pre_poly :::"FlattenSeq"::: )  (Set (Var "x")) ")" ))))))  ")" )  ")" )); func  :::"PostTraversal"::: "tsg" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") means :: DTCONSTR:def 13 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  "G" ")" ) "," (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  ")" ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  "tsg")) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G"  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  "G")  (Bool  "for" (Set (Var "rts")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "rts"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")))) & (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "rts")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_pre_poly :::"FlattenSeq"::: )  (Set (Var "x")) ")" )  ($#k1_pre_poly :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "nt")) ($#k3_pre_poly :::"*>"::: ) ))))))  ")" )  ")" )); end; 





















:: deftheorem    defines :::"TerminalString"::: DTCONSTR:def 11 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "tsg")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_dtconstr :::"TerminalString"::: )  (Set (Var "tsg")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")) ")" ) "," (Set  "(" (Set  "("  ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "tsg")))) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))  "st" (Bool (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_pre_poly :::"FlattenSeq"::: )  (Set  "(" (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts")) ")" ))))  ")" )  ")" ))  ")" )))); 
 
:: deftheorem    defines :::"PreTraversal"::: DTCONSTR:def 12 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "tsg")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_dtconstr :::"PreTraversal"::: )  (Set (Var "tsg")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")) ")" ) "," (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#k3_finseq_2 :::"*"::: )  ")" ) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "tsg")))) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "rts")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "rts"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")))) & (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "rts")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#k3_finseq_2 :::"*"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "nt")) ($#k3_pre_poly :::"*>"::: ) )  ($#k1_pre_poly :::"^"::: )  (Set  "("  ($#k5_pre_poly :::"FlattenSeq"::: )  (Set (Var "x")) ")" ))))))  ")" )  ")" ))  ")" )))); 
 
:: deftheorem    defines :::"PostTraversal"::: DTCONSTR:def 13 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "tsg")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_dtconstr :::"PostTraversal"::: )  (Set (Var "tsg")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")) ")" ) "," (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#k3_finseq_2 :::"*"::: )  ")" ) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "tsg")))) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "ts")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "rts")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "rts"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_dtconstr :::"roots"::: )  (Set (Var "ts")))) & (Bool (Set (Var "nt"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "rts")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#k3_finseq_2 :::"*"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "ts"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "nt"))  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "ts")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_pre_poly :::"FlattenSeq"::: )  (Set (Var "x")) ")" )  ($#k1_pre_poly :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "nt")) ($#k3_pre_poly :::"*>"::: ) ))))))  ")" )  ")" ))  ")" )))); 
 definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )  ; let "nt" be   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Const "G")); func  :::"TerminalLanguage"::: "nt" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k1_lang1 :::"Terminals"::: )  "G" ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) equals :: DTCONSTR:def 14  "{"  (Set  "("  ($#k15_dtconstr :::"TerminalString"::: )  (Set (Var "tsg")) ")" ) where tsg "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")) : (Bool  "("  (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  "G")) & (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  "nt")  ")" )  "}"  ; func  :::"PreTraversalLanguage"::: "nt" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  ")" ) equals :: DTCONSTR:def 15  "{"  (Set  "("  ($#k16_dtconstr :::"PreTraversal"::: )  (Set (Var "tsg")) ")" ) where tsg "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")) : (Bool  "("  (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  "G")) & (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  "nt")  ")" )  "}"  ; func  :::"PostTraversalLanguage"::: "nt" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  ")" ) equals :: DTCONSTR:def 16  "{"  (Set  "("  ($#k17_dtconstr :::"PostTraversal"::: )  (Set (Var "tsg")) ")" ) where tsg "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")) : (Bool  "("  (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  "G")) & (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  "nt")  ")" )  "}"  ; end; 


















:: deftheorem    defines :::"TerminalLanguage"::: DTCONSTR:def 14 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k18_dtconstr :::"TerminalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k15_dtconstr :::"TerminalString"::: )  (Set (Var "tsg")) ")" ) where tsg "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) : (Bool  "("  (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "nt")))  ")" )  "}"  ))); 
 
:: deftheorem    defines :::"PreTraversalLanguage"::: DTCONSTR:def 15 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k19_dtconstr :::"PreTraversalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k16_dtconstr :::"PreTraversal"::: )  (Set (Var "tsg")) ")" ) where tsg "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) : (Bool  "("  (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "nt")))  ")" )  "}"  ))); 
 
:: deftheorem    defines :::"PostTraversalLanguage"::: DTCONSTR:def 16 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_dtconstr :::"with_nonterminals"::: )     ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k20_dtconstr :::"PostTraversalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k17_dtconstr :::"PostTraversal"::: )  (Set (Var "tsg")) ")" ) where tsg "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_trees_3 :::"FinTrees"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) : (Bool  "("  (Bool (Set (Var "tsg"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "tsg"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "nt")))  ")" )  "}"  ))); 
 
theorem :: DTCONSTR:13 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )))) "holds"  (Bool (Set   ($#k15_dtconstr :::"TerminalString"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) ))) ; 
 
theorem :: DTCONSTR:14 (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) "holds"  (Bool (Set   ($#k18_dtconstr :::"TerminalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; 
 
theorem :: DTCONSTR:15 (Bool  "for" (Set (Var "t")) "being"    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )) "holds"  (Bool (Set   ($#k16_dtconstr :::"PreTraversal"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_trees_1 :::"height"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t")) ")" ) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Num 1) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) )))) ; 
 
theorem :: DTCONSTR:16 (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "nt"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k19_dtconstr :::"PreTraversalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Set (Var "nt"))  ($#r1_hidden :::"="::: )  (Num 1))) "implies" (Bool (Set   ($#k19_dtconstr :::"PreTraversalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Num 1) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) ) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  "}"  )  ")"   ")" )) ; 
 
theorem :: DTCONSTR:17 (Bool  "for" (Set (Var "t")) "being"    ($#m1_dtconstr :::"Element"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  ($#k5_dtconstr :::"PeanoNat"::: ) )) "holds"  (Bool (Set   ($#k17_dtconstr :::"PostTraversal"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set  "(" (Set  "("  ($#k6_trees_1 :::"height"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t")) ")" ) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Num 1) ")" )))) ; 
 
theorem :: DTCONSTR:18 (Bool  "for" (Set (Var "nt")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  ($#k5_dtconstr :::"PeanoNat"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "nt"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k20_dtconstr :::"PostTraversalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Set (Var "nt"))  ($#r1_hidden :::"="::: )  (Num 1))) "implies" (Bool (Set   ($#k20_dtconstr :::"PostTraversalLanguage"::: )  (Set (Var "nt")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set  ($#k3_pre_poly :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_pre_poly :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Num 1) ")" ) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  "}"  )  ")"   ")" )) ;