:: TREES_A semantic presentation begin theorem :: TREES_A:1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Var "p")) "," (Set (Var "s")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )) ; definitionlet "T", "T1" be ($#m1_hidden :::"Tree":::); let "P" be ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Const "T")); assume (Bool (Set (Const "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"tree"::: "(" "T" "," "P" "," "T1" ")" -> ($#m1_hidden :::"Tree":::) means :: TREES_A:def 1 (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "q")))) ")" ) ")" ) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "T1") & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"tree"::: TREES_A:def 1 : (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" )) "iff" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "q")))) ")" ) ")" ) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" )) ")" ) ")" )) ")" )))); theorem :: TREES_A:2 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t1"))))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where p "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "}" )))) ; theorem :: TREES_A:3 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "holds" (Bool "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t1"))))) "}" ($#r1_tarski :::"c="::: ) "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t1"))))) "}" ))) ; theorem :: TREES_A:4 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t1"))))) "}" ))) ; theorem :: TREES_A:5 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "holds" (Bool (Set "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t1"))))) "}" ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t1"))))) "}" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: TREES_A:6 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where p "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "}" ))) ; theorem :: TREES_A:7 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t1"))))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where p "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "}" )))) ; theorem :: TREES_A:8 (Bool "for" (Set (Var "T1")) "," (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "T1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ) ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))))))) ; registrationlet "T" be ($#m1_hidden :::"Tree":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_trees_1 :::"AntiChain_of_Prefixes-like"::: ) for ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" "T"; end; definitionlet "T" be ($#m1_hidden :::"Tree":::); let "t" be ($#m1_trees_1 :::"Element"::: ) "of" (Set (Const "T")); :: original: :::"{"::: redefine func :::"{":::"t":::"}"::: -> ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" "T"; end; theorem :: TREES_A:9 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set ($#k2_trees_a :::"{"::: ) (Set (Var "t")) ($#k2_trees_a :::"}"::: ) ) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "t")) "," (Set (Var "T1")) ")" )))) ; definitionlet "T" be ($#m1_hidden :::"DecoratedTree":::); let "P" be ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "T"))); let "T1" be ($#m1_hidden :::"DecoratedTree":::); assume (Bool (Set (Const "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"tree"::: "(" "T" "," "P" "," "T1" ")" -> ($#m1_hidden :::"DecoratedTree":::) means :: TREES_A:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_a :::"tree"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T" ")" ) "," "P" "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T1" ")" ) ")" )) & (Bool "(" "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_a :::"tree"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T" ")" ) "," "P" "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T1" ")" ) ")" )) "or" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set "T" ($#k1_funct_1 :::"."::: ) (Set (Var "q")))) ")" )) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "T1")) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set "T1" ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"tree"::: TREES_A:def 2 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) (Bool "for" (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_a :::"tree"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) "," (Set (Var "P")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_a :::"tree"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) "," (Set (Var "P")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1")) ")" ) ")" )) "or" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")))) ")" )) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" )) ")" ) ")" ) ")" ) ")" ))))); theorem :: TREES_A:10 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ))) "or" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) & (Bool (Set (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")))) ")" )) "or" (Bool "ex" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" )) ")" )))) ; theorem :: TREES_A:11 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ))) "or" (Bool "(" (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) & (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")))) ")" ) "or" (Bool "ex" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" )) ")" )))) ; theorem :: TREES_A:12 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t1"))))) "}" )) "holds" (Bool (Set (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))))))) ; theorem :: TREES_A:13 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) : (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t1")))) "}" )) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))))))) ; theorem :: TREES_A:14 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where p "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))), s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1"))) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "}" )) "holds" (Bool "ex" (Set (Var "p9")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")))(Bool "ex" (Set (Var "r")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1"))) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p9")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set (Var "p9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" )))))) ; theorem :: TREES_A:15 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1"))) : (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" )) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1"))) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" ))))) ; theorem :: TREES_A:16 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "holds" (Bool (Set ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set ($#k2_trees_a :::"{"::: ) (Set (Var "t")) ($#k2_trees_a :::"}"::: ) ) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "t")) "," (Set (Var "T1")) ")" )))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); let "P" be ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "T"))); let "T1" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); assume (Bool (Set (Const "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"tree"::: "(" "T" "," "P" "," "T1" ")" -> ($#m1_hidden :::"DecoratedTree":::) "of" "D" equals :: TREES_A:def 3 (Set ($#k3_trees_a :::"tree"::: ) "(" "T" "," "P" "," "T1" ")" ); end; :: deftheorem defines :::"tree"::: TREES_A:def 3 : (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")) (Bool "for" (Set (Var "P")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) (Bool "for" (Set (Var "T1")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_trees_a :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "P")) "," (Set (Var "T1")) ")" ))))));