(card_comp_propsnil 3316958745"" (expand "card_lt" )"" (prop)"1" (lemma "fun_exists[T2, T1]" )"1" (prop)"1" (skolem!)"1" (inst 2 "f!1" ) (("1" (grind) nil nil )) nil )) nil ))nil ))nil )"2" (skolem!)"2" (use "surjective_inverse_exists[T1, T2]" )"2" (skolem!)"2" (use "inj_inv_alt[T1, T2]" ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil )"3" (skolem! -2)"3" (use "inv_inj_is_surj[T2, T1]" ) (("3" (inst?) nil nil ))nil ))nil ))nil ))nil )"bool" functions nil )nil function_image nil )nil card_comp_props nil )nil card_comp_props nil )nil function_inverse_defnil )nil booleans nil )nil booleans nil )"bool" functions nil )"[T1 -> T2]" card_comp_props nil )nil function_inverse_def nil )"[T2 -> T1]" card_comp_props nil )"bool" function_inverse_def nil )"bool" booleans nil )nil function_inverse nil )"[T2 -> T1]" card_comp_props nil )"D" function_inverse nil )"bool" card_comp nil ))nil 3316958898"" (expand "card_ge" )"" (split)"1" (flatten)"1" (skolem!)"1" (case "EXISTS (t: T2): TRUE" )"1" (use "inv_inj_is_surj[T2, T1]" )"1" (inst?) nil nil )) nil )"2" (split)"1" (lemma "fun_exists[T1, T2]" )"1" (prop)"1" (skolem!)"1" (inst 3 "f!2" ) (("1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (skolem!) (("2" (inst + "t!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (prop)"1" (skolem!)"1" (inst + "LAMBDA (x: T2): t!1" ) (("1" (grind) nil nil ))nil ))nil )"2" (skolem!)"2" (use "surjective_inverse_exists[T1, T2]" )"2" (skolem!)"2" (use "inj_inv_alt[T1, T2]" ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )nil function_image nil )nil card_comp_props nil )nil function_inverse nil )"[T2 -> T1]" card_comp_props nil )"bool" functions nil )"D" function_inverse nil )nil card_comp_props nil )nil booleans nil )nil booleans nil )"bool" booleans nil )"bool" function_inverse_def nil )"[T2 -> T1]" card_comp_props nil )nil function_inverse_def nil )"[T1 -> T2]" card_comp_props nil )nil function_inverse_defnil )"bool" card_comp nil ))nil 3316959024"" (expand * "card_lt" "card_le" )"" (lemma "injective_dichotomous" ) (("" (prop) nil nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_dichotomous "orders/" )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959049"" (expand * "card_gt" "card_ge" )"" (lemma "injective_dichotomous" ) (("" (prop) nil nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_dichotomous "orders/" )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959093"" (expand * "card_lt" "card_gt" ) nil nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959107"" (expand * "card_le" "card_ge" ) nil nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959121"" (expand * "card_gt" "card_lt" ) nil nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959130"" (expand * "card_ge" "card_le" ) nil nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959138"" (expand * "XOR" "card_lt" "card_ge" ) (("" (reduce) nil nil )) nil )"bool" xor_def nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959172"" (expand * "XOR" "card_le" "card_gt" ) (("" (reduce) nil nil )) nil )"bool" xor_def nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959186"" (expand * "card_eq" "card_le" "card_ge" )"" (lemma "inj_inj_bij" )"" (reduce)"1" (use "bijective_inverse_exists[T1, T2]" )"1" (expand "exists1" )"1" (skosimp*)"1" (use "bij_inv_is_bij_alt[T1, T2]" )"1" (expand "bijective?" -1)"1" (flatten) (("1" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "bijective?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_antisymmetric "orders/" )nil function_inverse_defnil )nil booleans nil )nil booleans nil )"bool" functions nil )"bool" function_inverse_def nil )"[T2 -> T1]" card_comp_props nil )"[T1 -> T2]" card_comp_props nil )nil function_inverse_def nil )"bool" exists1 nil )"bool" card_comp nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959272"" (expand * "card_le" "card_lt" "card_eq" )"" (lemma "inj_inj_bij" )"" (lemma "injective_dichotomous" )"" (reduce)"" (expand "bijective?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_antisymmetric "orders/" )"bool" functions nil )nil set_dichotomous "orders/" )"bool" card_comp nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959313"" (lemma "card_eq_le_ge" )"" (lemma "injective_dichotomous" )"" (expand * "card_ge" "card_le" "card_gt" "card_eq" )"" (prop) nil nil )) nil ))nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_dichotomous "orders/" )"bool" card_comp nil )"bool" card_comp nil )"bool" card_comp nil )"bool" card_comp nil )nil card_comp_props nil ))nil 3316959372"" (lemma "card_ge_gt_eq" )"" (lemma "card_lt_ge" )"" (expand "XOR" ) (("" (ground) nil nil )) nil )) nil ))nil )nil card_comp_props nil )"bool" xor_def nil )nil card_comp_props nil ))nil 3316959390"" (expand * "card_gt" "card_eq" "card_lt" )"" (lemma "injective_dichotomous" )"" (expand "bijective?" ) (("" (reduce) nil nil )) nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_dichotomous "orders/" )"bool" functions nil )"bool" card_comp nil )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959443"" (expand "card_lt" )"" (lemma "injective_dichotomous" ) (("" (prop) nil nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_dichotomous "orders/" )"bool" card_comp nil ))nil 3316959455"" (lemma "inj_inj_bij" )"" (expand * "card_le" "card_eq" ) nil nil )) nil )"bool" card_comp nil )"bool" card_comp nil )nil set_antisymmetric "orders/" )nil card_comp_props nil )nil card_comp_props nil ))nil 3316959482"" (expand "card_eq" )"" (iff)"" (prop)"1" (skolem!)"1" (use "bijective_inverse_exists[T1, T2]" )"1" (expand "exists1" )"1" (skosimp*)"1" (use "bij_inv_is_bij_alt[T1, T2]" )"1" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skolem!)"2" (use "bijective_inverse_exists[T2, T1]" )"2" (expand "exists1" )"2" (skosimp*)"2" (use "bij_inv_is_bij_alt[T2, T1]" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T1 -> T2]" card_comp_props nil )"[T2 -> T1]" card_comp_props nil )"bool" exists1 nil )nil function_inverse_def nil )"[T2 -> T1]" card_comp_props nil )"bool" function_inverse_def nil )"[T1 -> T2]" card_comp_props nil )"bool" functions nil )nil booleans nil )nil booleans nil )nil card_comp_props nil )nil card_comp_props nil )nil function_inverse_defnil )"bool" card_comp nil ))nil 3316959532"" (expand * "card_ge" "card_eq" )"" (lemma "inj_inj_bij" ) (("" (prop) nil nil )) nil )) nil )nil card_comp_props nil )nil card_comp_props nil )nil set_antisymmetric "orders/" )"bool" card_comp nil )"bool" card_comp nil ))nil 3316959552"" (expand "card_gt" )"" (lemma "injective_dichotomous" ) (("" (prop) nil nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil set_dichotomous "orders/" )"bool" card_comp nil ))nil 3316959567"" (lemma "card_lt_ge" )"" (lemma "card_gt_lt" )"" (lemma "card_ge_gt_eq" )"" (expand "XOR" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil )nil card_comp_props nil )"bool" xor_def nil )nil card_comp_props nil )nil card_comp_props nil ))nil 3316959601"" (lemma "card_le_gt" )"" (lemma "card_ge_le" )"" (lemma "card_gt_ge" )"" (expand "XOR" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil )nil card_comp_props nil )"bool" xor_def nil )nil card_comp_props nil )nil card_comp_props nil ))nil 3316959625"" (lemma "card_le_dichotomous" )"" (lemma "card_le_ge" )"" (lemma "card_ge_le" ) (("" (ground) nil nil )) nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil card_comp_props nil ))nil 3316959647"" (lemma "card_lt_trichotomous" )"" (lemma "card_lt_gt" )"" (lemma "card_gt_lt" ) (("" (ground) nil nil )) nil )) nil ))nil )nil card_comp_props nil )nil card_comp_props nil )nil card_comp_props nil ))quality 100%
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
