:: PRELAMB semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"typealg"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"typealg":::(# :::"carrier":::, :::"left_quotient":::, :::"right_quotient":::, :::"inner_product"::: #) -> ($#l1_prelamb :::"typealg"::: ) ; sel :::"left_quotient"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"right_quotient"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"inner_product"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_prelamb :::"strict"::: ) for ($#l1_prelamb :::"typealg"::: ) ; end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; mode type of "s" is ($#m1_subset_1 :::"Element":::) "of" "s"; end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "x", "y" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); func "x" :::"\"::: "y" -> ($#m1_subset_1 :::"type":::) "of" "s" equals :: PRELAMB:def 1 (Set (Set "the" ($#u1_prelamb :::"left_quotient"::: ) "of" "s") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); func "x" :::"/""::: "y" -> ($#m1_subset_1 :::"type":::) "of" "s" equals :: PRELAMB:def 2 (Set (Set "the" ($#u2_prelamb :::"right_quotient"::: ) "of" "s") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); func "x" :::"*"::: "y" -> ($#m1_subset_1 :::"type":::) "of" "s" equals :: PRELAMB:def 3 (Set (Set "the" ($#u3_prelamb :::"inner_product"::: ) "of" "s") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"\"::: PRELAMB:def 1 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_prelamb :::"left_quotient"::: ) "of" (Set (Var "s"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); :: deftheorem defines :::"/""::: PRELAMB:def 2 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_prelamb :::"right_quotient"::: ) "of" (Set (Var "s"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); :: deftheorem defines :::"*"::: PRELAMB:def 3 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_prelamb :::"inner_product"::: ) "of" (Set (Var "s"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; mode PreProof of "s" is ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "Tr" be ($#m1_hidden :::"PreProof":::) "of" (Set (Const "s")); let "v" be ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "Tr"))); attr "v" is :::"correct"::: means :: PRELAMB:def 4 (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "ex" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "ex" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "holds" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "ex" (Set (Var "X")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s"(Bool "ex" (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" )))) ")" )) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)) (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "Y")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)) (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) "v") ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" "v" ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) if (Bool (Set (Set "(" "Tr" ($#k3_trees_2 :::"."::: ) "v" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)) otherwise (Bool contradiction); end; :: deftheorem defines :::"correct"::: PRELAMB:def 4 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "Tr")) "being" ($#m1_hidden :::"PreProof":::) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Tr"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "ex" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "ex" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "ex" (Set (Var "X")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" )))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "Y")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "Tr")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)))) "implies" (Bool "(" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) "iff" (Bool contradiction) ")" ) ")" ")" )))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "IT" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); attr "IT" is :::"left"::: means :: PRELAMB:def 5 (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y"))))); attr "IT" is :::"right"::: means :: PRELAMB:def 6 (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y"))))); attr "IT" is :::"middle"::: means :: PRELAMB:def 7 (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"left"::: PRELAMB:def 5 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_prelamb :::"left"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y"))))) ")" ))); :: deftheorem defines :::"right"::: PRELAMB:def 6 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_prelamb :::"right"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y"))))) ")" ))); :: deftheorem defines :::"middle"::: PRELAMB:def 7 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_prelamb :::"middle"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y"))))) ")" ))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "IT" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); attr "IT" is :::"primitive"::: means :: PRELAMB:def 8 (Bool "(" (Bool (Bool "not" "IT" "is" ($#v3_prelamb :::"left"::: ) )) & (Bool (Bool "not" "IT" "is" ($#v4_prelamb :::"right"::: ) )) & (Bool (Bool "not" "IT" "is" ($#v5_prelamb :::"middle"::: ) )) ")" ); end; :: deftheorem defines :::"primitive"::: PRELAMB:def 8 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_prelamb :::"primitive"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "IT")) "is" ($#v3_prelamb :::"left"::: ) )) & (Bool (Bool "not" (Set (Var "IT")) "is" ($#v4_prelamb :::"right"::: ) )) & (Bool (Bool "not" (Set (Var "IT")) "is" ($#v5_prelamb :::"middle"::: ) )) ")" ) ")" ))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "Tr" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "s"))); let "v" be ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "Tr"))); :: original: :::"."::: redefine func "Tr" :::"."::: "v" -> ($#m1_subset_1 :::"type":::) "of" "s"; end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "Tr" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "s"))); let "x" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); pred "Tr" :::"represents"::: "x" means :: PRELAMB:def 9 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "Tr") "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "Tr") "holds" (Bool "(" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2)) ")" ) & "(" (Bool (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set "Tr" ($#k4_prelamb :::"."::: ) (Set (Var "v"))) "is" ($#v6_prelamb :::"primitive"::: ) ) ")" & "(" (Bool (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool "(" (Bool (Set "Tr" ($#k4_prelamb :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")))) "or" (Bool (Set "Tr" ($#k4_prelamb :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "z")))) "or" (Bool (Set "Tr" ($#k4_prelamb :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_prelamb :::"*"::: ) (Set (Var "z")))) ")" ) & (Bool (Set "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set "Tr" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"represents"::: PRELAMB:def 9 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "Tr")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "Tr")) ($#r1_prelamb :::"represents"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Tr"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Tr"))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2)) ")" ) & "(" (Bool (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "Tr")) ($#k4_prelamb :::"."::: ) (Set (Var "v"))) "is" ($#v6_prelamb :::"primitive"::: ) ) ")" & "(" (Bool (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool "(" (Bool (Set (Set (Var "Tr")) ($#k4_prelamb :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")))) "or" (Bool (Set (Set (Var "Tr")) ($#k4_prelamb :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "z")))) "or" (Bool (Set (Set (Var "Tr")) ($#k4_prelamb :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_prelamb :::"*"::: ) (Set (Var "z")))) ")" ) & (Bool (Set (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "Tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) ")" ")" ) ")" ) ")" ) ")" )))); notationlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "Tr" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "s"))); let "x" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); antonym "Tr" :::"does_not_represent"::: "x" for "Tr" :::"represents"::: "x"; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; attr "IT" is :::"free"::: means :: PRELAMB:def 10 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "holds" (Bool "(" (Bool "not" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_prelamb :::"left"::: ) ) & (Bool (Set (Var "x")) "is" ($#v4_prelamb :::"right"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_prelamb :::"left"::: ) ) & (Bool (Set (Var "x")) "is" ($#v5_prelamb :::"middle"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) "is" ($#v4_prelamb :::"right"::: ) ) & (Bool (Set (Var "x")) "is" ($#v5_prelamb :::"middle"::: ) ) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" (Bool "ex" (Set (Var "Tr")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "st" (Bool "for" (Set (Var "Tr1")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "holds" (Bool "(" (Bool (Set (Var "Tr1")) ($#r1_prelamb :::"represents"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "Tr")) ($#r1_hidden :::"="::: ) (Set (Var "Tr1"))) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"free"::: PRELAMB:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_prelamb :::"free"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool "not" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_prelamb :::"left"::: ) ) & (Bool (Set (Var "x")) "is" ($#v4_prelamb :::"right"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_prelamb :::"left"::: ) ) & (Bool (Set (Var "x")) "is" ($#v5_prelamb :::"middle"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) "is" ($#v4_prelamb :::"right"::: ) ) & (Bool (Set (Var "x")) "is" ($#v5_prelamb :::"middle"::: ) ) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "Tr")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "st" (Bool "for" (Set (Var "Tr1")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "holds" (Bool "(" (Bool (Set (Var "Tr1")) ($#r1_prelamb :::"represents"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "Tr")) ($#r1_hidden :::"="::: ) (Set (Var "Tr1"))) ")" ))) ")" ) ")" ) ")" )); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "x" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); assume (Bool (Set (Const "s")) "is" ($#v7_prelamb :::"free"::: ) ) ; func :::"repr_of"::: "x" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") means :: PRELAMB:def 11 (Bool "for" (Set (Var "Tr")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") "holds" (Bool "(" (Bool (Set (Var "Tr")) ($#r1_prelamb :::"represents"::: ) "x") "iff" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "Tr"))) ")" )); end; :: deftheorem defines :::"repr_of"::: PRELAMB:def 11 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v7_prelamb :::"free"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_prelamb :::"repr_of"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "Tr")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s"))) "holds" (Bool "(" (Bool (Set (Var "Tr")) ($#r1_prelamb :::"represents"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "Tr"))) ")" )) ")" )))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "s")); let "t" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); :: original: :::"["::: redefine func :::"[":::"f" "," "t":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; mode :::"Proof"::: "of" "s" -> ($#m1_hidden :::"PreProof":::) "of" "s" means :: PRELAMB:def 12 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) it) "holds" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"Proof"::: PRELAMB:def 12 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"PreProof":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) "holds" (Bool (Set (Var "v")) "is" ($#v2_prelamb :::"correct"::: ) ) ")" ) ")" ) ")" ))); theorem :: PRELAMB:1 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))))) ; theorem :: PRELAMB:2 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set ($#k8_trees_2 :::"branchdeg"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) ")" )))) ; theorem :: PRELAMB:3 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "x")) ($#k6_prelamb :::"]"::: ) )))))) ; theorem :: PRELAMB:4 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "x")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))) ; theorem :: PRELAMB:5 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) "," (Set (Var "x")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))) ; theorem :: PRELAMB:6 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool "ex" (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "u")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))) ; theorem :: PRELAMB:7 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4))) "holds" (Bool "ex" (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "u")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))) ; theorem :: PRELAMB:8 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "X")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))))) ; theorem :: PRELAMB:9 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6))) "holds" (Bool "ex" (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "X")) "," (Set (Var "x")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "u")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "Y")) "," (Set (Var "y")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))) ; theorem :: PRELAMB:10 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7))) "holds" (Bool "ex" (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))(Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "u")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) ")" ))))))) ; theorem :: PRELAMB:11 (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)) "or" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)) ")" )))) ; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "IT" be ($#m1_hidden :::"PreProof":::) "of" (Set (Const "s")); attr "IT" is :::"cut-free"::: means :: PRELAMB:def 13 (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "IT") "holds" (Bool (Set (Set "(" "IT" ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 7))); end; :: deftheorem defines :::"cut-free"::: PRELAMB:def 13 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"PreProof":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_prelamb :::"cut-free"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))) "holds" (Bool (Set (Set "(" (Set (Var "IT")) ($#k3_trees_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 7))) ")" ))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; func :::"size_w.r.t."::: "s" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: PRELAMB:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k5_prelamb :::"repr_of"::: ) (Set (Var "x")) ")" ) ")" )))); end; :: deftheorem defines :::"size_w.r.t."::: PRELAMB:def 14 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s"))) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_prelamb :::"size_w.r.t."::: ) (Set (Var "s")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k5_prelamb :::"repr_of"::: ) (Set (Var "x")) ")" ) ")" )))) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"(#)"::: redefine func "f" :::"*"::: "T" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "p" be ($#m1_prelamb :::"Proof"::: ) "of" (Set (Const "s")); func :::"cutdeg"::: "p" -> ($#m1_hidden :::"Nat":::) means :: PRELAMB:def 15 (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "s"(Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "st" (Bool "(" (Bool (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k7_prelamb :::"size_w.r.t."::: ) "s" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k7_prelamb :::"size_w.r.t."::: ) "s" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k7_prelamb :::"size_w.r.t."::: ) "s" ")" ) ($#k8_prelamb :::"*"::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ) ")" ))) ")" ))) if (Bool (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"cutdeg"::: PRELAMB:def 15 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prelamb :::"Proof"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_prelamb :::"cutdeg"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set (Var "T")) "," (Set (Var "y")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_prelamb :::"["::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "z")) ($#k6_prelamb :::"]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k7_prelamb :::"size_w.r.t."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k7_prelamb :::"size_w.r.t."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k7_prelamb :::"size_w.r.t."::: ) (Set (Var "s")) ")" ) ($#k8_prelamb :::"*"::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ) ")" ))) ")" ))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_prelamb :::"cutdeg"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" )))); definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"Model"::: "of" "s" "," "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "s") "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) means :: PRELAMB:def 16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "s" "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) "}" ) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "a1")) where a1 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ) : (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "a1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "}" ) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "a2")) where a2 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ) : (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "b")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "a2"))) ($#r2_hidden :::"in"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "}" ) ")" )); end; :: deftheorem defines :::"Model"::: PRELAMB:def 16 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_prelamb :::"typealg"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s"))) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_prelamb :::"Model"::: ) "of" (Set (Var "s")) "," (Set (Var "A"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) "}" ) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "a1")) where a1 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "a1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "}" ) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "a2")) where a2 "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "b")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "a2"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "}" ) ")" )) ")" )))); definitionattr "c1" is :::"strict"::: ; struct :::"typestr"::: -> ($#l1_prelamb :::"typealg"::: ) ; aggr :::"typestr":::(# :::"carrier":::, :::"left_quotient":::, :::"right_quotient":::, :::"inner_product":::, :::"derivability"::: #) -> ($#l2_prelamb :::"typestr"::: ) ; sel :::"derivability"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_prelamb :::"strict"::: ) for ($#l2_prelamb :::"typestr"::: ) ; end; definitionlet "s" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_prelamb :::"typestr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "s")); let "x" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); pred "f" :::"==>."::: "x" means :: PRELAMB:def 17 (Bool (Set ($#k6_prelamb :::"["::: ) "f" "," "x" ($#k6_prelamb :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_prelamb :::"derivability"::: ) "of" "s")); end; :: deftheorem defines :::"==>."::: PRELAMB:def 17 : (Bool "for" (Set (Var "s")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_prelamb :::"typestr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "s")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) "iff" (Bool (Set ($#k6_prelamb :::"["::: ) (Set (Var "f")) "," (Set (Var "x")) ($#k6_prelamb :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_prelamb :::"derivability"::: ) "of" (Set (Var "s")))) ")" )))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_prelamb :::"typestr"::: ) ; attr "IT" is :::"SynTypes_Calculus-like"::: means :: PRELAMB:def 18 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "IT" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "st" (Bool (Bool (Set (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_prelamb :::"==>."::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y"))))) ")" ) & (Bool "(" "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "IT" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "st" (Bool (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "IT" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "st" (Bool (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) & (Bool (Set (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) ")" ) & (Bool "(" "for" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "IT" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "st" (Bool (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) & (Bool (Set (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) ")" ) & (Bool "(" "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "IT" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) ")" ) & (Bool "(" "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "IT" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" "IT" "st" (Bool (Bool (Set (Var "X")) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) & (Bool (Set (Var "Y")) ($#r2_prelamb :::"==>."::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y"))))) ")" ) ")" ); end; :: deftheorem defines :::"SynTypes_Calculus-like"::: PRELAMB:def 18 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_prelamb :::"typestr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_prelamb :::"SynTypes_Calculus-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_prelamb :::"==>."::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y"))))) ")" ) & (Bool "(" "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) & (Bool (Set (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) ")" ) & (Bool "(" "for" (Set (Var "T")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "T")) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) & (Bool (Set (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "T")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) ")" ) & (Bool "(" "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Var "z")))) ")" ) & (Bool "(" "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "X")) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) & (Bool (Set (Var "Y")) ($#r2_prelamb :::"==>."::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "X")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "Y"))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y"))))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_prelamb :::"SynTypes_Calculus-like"::: ) for ($#l2_prelamb :::"typestr"::: ) ; end; definitionmode SynTypes_Calculus is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_prelamb :::"SynTypes_Calculus-like"::: ) ($#l2_prelamb :::"typestr"::: ) ; end; theorem :: PRELAMB:12 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) & (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) ")" ))) ; theorem :: PRELAMB:13 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")) ")" ) ($#k1_prelamb :::"\"::: ) (Set (Var "y")))) ")" ))) ; theorem :: PRELAMB:14 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")) ")" ) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")) ")" ))))) ; theorem :: PRELAMB:15 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "z")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_prelamb :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ))))) ; theorem :: PRELAMB:16 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "z")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "z")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")))) ")" ))) ; theorem :: PRELAMB:17 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "z")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "z")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "z")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "z")))) ")" ))) ; theorem :: PRELAMB:18 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")) ")" ) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")))))) ; theorem :: PRELAMB:19 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")))) & (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")))) ")" ))) ; theorem :: PRELAMB:20 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")))) & (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")))) ")" ))) ; theorem :: PRELAMB:21 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_prelamb :::"/""::: ) (Set (Var "x")))) & (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")) ")" ) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ))) ")" ))) ; theorem :: PRELAMB:22 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")) ")" ) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ))) & (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ($#k1_prelamb :::"\"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_prelamb :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ) ")" ))) ")" ))) ; theorem :: PRELAMB:23 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "st" (Bool (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "x")) ($#k1_prelamb :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_prelamb :::"\"::: ) (Set (Var "y")))) ")" ))) ; theorem :: PRELAMB:24 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))))) ; definitionlet "s" be ($#l2_prelamb :::"SynTypes_Calculus":::); let "x", "y" be ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")); pred "x" :::"<==>."::: "y" means :: PRELAMB:def 19 (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) "x" ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) "y") & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) "y" ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) "x") ")" ); reflexivity (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")) "holds" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) ")" )) ; symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Const "s")) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) ")" )) ; end; :: deftheorem defines :::"<==>."::: PRELAMB:def 19 : (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r3_prelamb :::"<==>."::: ) (Set (Var "y"))) "iff" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "y"))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Var "x"))) ")" ) ")" ))); theorem :: PRELAMB:25 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y"))) ($#r3_prelamb :::"<==>."::: ) (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k1_prelamb :::"\"::: ) (Set (Var "x")) ")" ))))) ; theorem :: PRELAMB:26 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set "(" (Set (Var "z")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" )) ($#r3_prelamb :::"<==>."::: ) (Set (Set "(" (Set (Var "x")) ($#k2_prelamb :::"/""::: ) (Set (Var "y")) ")" ) ($#k2_prelamb :::"/""::: ) (Set (Var "z")))))) ; theorem :: PRELAMB:27 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set "(" (Set (Var "y")) ($#k2_prelamb :::"/""::: ) (Set (Var "z")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k2_prelamb :::"/""::: ) (Set (Var "z")))))) ; theorem :: PRELAMB:28 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k2_prelamb :::"/""::: ) (Set (Var "y")))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_prelamb :::"==>."::: ) (Set (Set (Var "y")) ($#k1_prelamb :::"\"::: ) (Set "(" (Set (Var "y")) ($#k3_prelamb :::"*"::: ) (Set (Var "x")) ")" ))) ")" ))) ; theorem :: PRELAMB:29 (Bool "for" (Set (Var "s")) "being" ($#l2_prelamb :::"SynTypes_Calculus":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"type":::) "of" (Set (Var "s")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_prelamb :::"*"::: ) (Set (Var "z"))) ($#r3_prelamb :::"<==>."::: ) (Set (Set (Var "x")) ($#k3_prelamb :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_prelamb :::"*"::: ) (Set (Var "z")) ")" ))))) ;