:: BINTREE1 semantic presentation begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); func :::"root-label"::: "t" -> ($#m1_subset_1 :::"Element"::: ) "of" "D" equals :: BINTREE1:def 1 (Set "t" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"root-label"::: BINTREE1:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))); theorem :: BINTREE1:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k14_trees_3 :::"roots"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "t")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t")) ")" ) ($#k3_pre_poly :::"*>"::: ) )))) ; theorem :: BINTREE1:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k14_trees_3 :::"roots"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")) ")" ) "," (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")) ")" ) ($#k4_pre_poly :::"*>"::: ) )))) ; definitionlet "IT" be ($#m1_hidden :::"Tree":::); attr "IT" is :::"binary"::: means :: BINTREE1:def 2 (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) "IT")))) "holds" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Num 1) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k2_tarski :::"}"::: ) ))); end; :: deftheorem defines :::"binary"::: BINTREE1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_bintree1 :::"binary"::: ) ) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "IT")))))) "holds" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Num 1) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k2_tarski :::"}"::: ) ))) ")" )); theorem :: BINTREE1:3 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T")))) ")" ))) ; registration cluster (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v1_bintree1 :::"binary"::: ) ; cluster (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 2)) -> ($#v1_bintree1 :::"binary"::: ) ; end; theorem :: BINTREE1:4 (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) )) "is" ($#v1_bintree1 :::"binary"::: ) ) ; theorem :: BINTREE1:5 (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 2)) "is" ($#v1_bintree1 :::"binary"::: ) ) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_trees_1 :::"Tree-like"::: ) ($#v1_bintree1 :::"binary"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "IT" be ($#m1_hidden :::"DecoratedTree":::); attr "IT" is :::"binary"::: means :: BINTREE1:def 3 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "IT") "is" ($#v1_bintree1 :::"binary"::: ) ); end; :: deftheorem defines :::"binary"::: BINTREE1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_bintree1 :::"binary"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))) "is" ($#v1_bintree1 :::"binary"::: ) ) ")" )); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) ($#v2_bintree1 :::"binary"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) ($#v2_bintree1 :::"binary"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ($#v1_bintree1 :::"binary"::: ) -> ($#v1_trees_2 :::"finite-order"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: BINTREE1:6 (Bool "for" (Set (Var "T0")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T0")) "," (Set (Var "T1")) ")" ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T0")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T0")) "," (Set (Var "T1")) ")" ")" ))) "iff" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T0")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Num 1) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T0")) "," (Set (Var "T1")) ")" ")" ))) "iff" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T1")))) ")" ) ")" ) ")" ))) ; theorem :: BINTREE1:7 (Bool "for" (Set (Var "T0")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T0")) "," (Set (Var "T1")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "t")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Num 1) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T0")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "sp")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "sp")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "p")))) "iff" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "sp"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Num 1) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "sp")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "sp")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "p")))) "iff" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Num 1) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "sp"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t")))) ")" )) ")" ) ")" ))) ; theorem :: BINTREE1:8 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "T1")) "is" ($#v1_bintree1 :::"binary"::: ) ) & (Bool (Set (Var "T2")) "is" ($#v1_bintree1 :::"binary"::: ) ) ")" ) "iff" (Bool (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) "is" ($#v1_bintree1 :::"binary"::: ) ) ")" )) ; theorem :: BINTREE1:9 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "T1")) "is" ($#v2_bintree1 :::"binary"::: ) ) & (Bool (Set (Var "T2")) "is" ($#v2_bintree1 :::"binary"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "x")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) "is" ($#v2_bintree1 :::"binary"::: ) ) ")" ))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "T1", "T2" be ($#v1_finset_1 :::"finite"::: ) ($#v2_bintree1 :::"binary"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); cluster (Set "x" ($#k6_trees_4 :::"-tree"::: ) "(" "T1" "," "T2" ")" ) -> "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v2_bintree1 :::"binary"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lang1 :::"DTConstrStr"::: ) ; attr "IT" is :::"binary"::: means :: BINTREE1:def 4 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Symbol":::) "of" "IT" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_lang1 :::"==>"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Symbol":::) "of" "IT" "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_pre_poly :::"*>"::: ) ))))); end; :: deftheorem defines :::"binary"::: BINTREE1:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lang1 :::"DTConstrStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_bintree1 :::"binary"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_lang1 :::"==>"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_pre_poly :::"*>"::: ) ))))) ")" )); 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"::: ) ($#v3_bintree1 :::"binary"::: ) for ($#l1_lang1 :::"DTConstrStr"::: ) ; end; scheme :: BINTREE1:sch 1 BinDTConstrStrEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lang1 :::"strict"::: ) ($#v3_bintree1 :::"binary"::: ) ($#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")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_pre_poly :::"*>"::: ) )) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))]) ")" ) ")" ) ")" )) proof end; theorem :: BINTREE1:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool "(" (Bool (Set (Var "nt")) "is" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set (Var "G"))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "ts"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) )) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "ts")))) & (Bool (Num 2) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "ts")))) & (Bool "ex" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))) ($#r1_hidden :::"="::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")) ")" ) "," (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")) ")" ) ($#k4_pre_poly :::"*>"::: ) )) & (Bool (Set (Var "tl")) ($#r1_hidden :::"="::: ) (Set (Set (Var "ts")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "tr")) ($#r1_hidden :::"="::: ) (Set (Set (Var "ts")) ($#k1_funct_1 :::"."::: ) (Num 2))) & (Bool (Set (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" )) & (Bool (Set (Var "tl")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "ts")))) & (Bool (Set (Var "tr")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "ts")))) ")" )) ")" )))) ; scheme :: BINTREE1:sch 2 BinDTConstrInd{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "t"))])) provided (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "s")))])) and (Bool "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")) ")" ) "," (Set "(" ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")) ")" ) ($#k4_pre_poly :::"*>"::: ) )) & (Bool P1[(Set (Var "tl"))]) & (Bool P1[(Set (Var "tr"))])) "holds" (Bool P1[(Set (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" )]))) proof end; scheme :: BINTREE1:sch 3 BinDTConstrIndDef{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#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_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" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "t")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "nt")) "," (Set (Var "rtl")) "," (Set (Var "rtr")) "," (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" )) proof end; scheme :: BINTREE1:sch 4 BinDTConstrUniqDef{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F4 "(" ")" )) provided (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "t")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "nt")) "," (Set (Var "rtl")) "," (Set (Var "rtr")) "," (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" ) and (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "t")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "nt")) "," (Set (Var "rtl")) "," (Set (Var "rtr")) "," (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" ) proof end; definitionlet "A", "B", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "B")); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")); :: original: :::"["::: redefine func :::"[":::"a" "," "b" "," "c":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) "A" "," "B" "," "C" ($#k3_zfmisc_1 :::":]"::: ) ); end; scheme :: BINTREE1:sch 5 BinDTCDefLambda{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "t")) ")" ))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "t")) "," (Set (Var "a")) ")" )) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "nt")) "," (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "a")) ")" )) ")" ) ")" )))) ")" ) ")" )) proof end; scheme :: BINTREE1:sch 6 BinDTCDefLambdaUniq{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool (Set F4 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F5 "(" ")" )) provided (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "t")) ")" ))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "t")) "," (Set (Var "a")) ")" )) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "nt")) "," (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "a")) ")" )) ")" ) ")" )))) ")" ) ")" ) and (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_dtconstr :::"root-tree"::: ) (Set (Var "t")) ")" ))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "t")) "," (Set (Var "a")) ")" )) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "nt")) "," (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "a")) ")" )) ")" ) ")" )))) ")" ) ")" ) proof end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) ; cluster -> ($#v2_bintree1 :::"binary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) "G"); end;