| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 239 kB |
|
Quelle cantor_bernstein_schroeder.prfSprache: Lisp |
|||||||||||||||
|
(cantor_bernstein_schroeder (Afun_TCC1 0 (Afun_TCC1-1 nil 3543567590 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (Afun_TCC2 0 (Afun_TCC2-1 nil 3543567590 ("" (termination-tcc) nil nil) nil nil)) (Afundef 0 (Afundef-1 nil 3543569773 ("" (induct "i") (("1" (skeep) (("1" (inst - "f" "g" "aa") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (expand "Afun") (("2" (propax) nil nil)) nil)) nil) ("3" (skeep) (("3" (skeep) (("3" (inst - "f" "g" "aa") (("3" (expand "Afun" +) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((nat_induction formula-decl nil naturalnumbers nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (Afundef2 0 (Afundef2-1 nil 3543650214 ("" (skeep) (("" (expand "Afun" + 2) (("" (propax) nil nil)) nil)) nil) ((Afun def-decl "[A, B]" cantor_bernstein_schroeder nil)) shostak)) (Afuncomp 0 (Afuncomp-1 nil 3543575943 ("" (induct "i") (("1" (skeep) (("1" (assert) (("1" (expand "Afun" + 2) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skolem 1 "ii") (("2" (flatten) (("2" (induct "j") (("1" (skeep) (("1" (expand "Afun" + 1) (("1" (assert) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "ii+1" "a") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "jj") (("2" (flatten) (("2" (skeep) (("2" (assert) (("2" (expand "Afun" + 1) (("2" (inst - "f" "g" "a") (("2" (assert) (("2" (replace -1) (("2" (expand "Afun" + 3) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (Afuneq_TCC1 0 (Afuneq_TCC1-1 nil 3543650947 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil)) nil)) (Afuneq_TCC2 0 (Afuneq_TCC2-1 nil 3543650947 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil)) nil)) (Afuneq 0 (Afuneq-1 nil 3543650949 ("" (skeep) (("" (induct "k") (("1" (assert) (("1" (ground) (("1" (lemma "Afundef") (("1" (inst-cp - "f" "g" "i" "a1") (("1" (inst - "f" "g" "j" "a2") (("1" (assert) (("1" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "Afundef") (("2" (inst-cp - "f" "g" "i" "a1") (("2" (inst - "f" "g" "j" "a2") (("2" (assert) (("2" (replace -1 :dir rl) (("2" (replace -2 :dir rl) (("2" (expand "injective?") (("2" (inst?) (("2" (assert) (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "k") (("2" (flatten) (("2" (assert) (("2" (case "Afun(f, g)(a1)(-1 - k + i)`2 = Afun(f, g)(a2)(-1 - k + j)`2") (("1" (hide -7) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "-1-k+i" "a1") (("1" (lemma "Afundef") (("1" (inst - "f" "g" "-1-k+j" "a2") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -2 :dir rl) (("1" (expand "injective?") (("1" (inst?) (("1" (assert) (("1" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -6) (("2" (lemma "Afundef2") (("2" (inst-cp - "f" "g" "-1-k+i" "a1") (("2" (inst - "f" "g" "-1-k+j" "a2") (("2" (assert) (("2" (expand "injective?" -7) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (j skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (pred type-eq-decl nil defined_types nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (nat_induction formula-decl nil naturalnumbers nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (injective? const-decl "bool" functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Afundef2 formula-decl nil cantor_bernstein_schroeder nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (Bfun_TCC1 0 (Bfun_TCC1-1 nil 3543569291 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil)) nil)) (Bfun_TCC2 0 (Bfun_TCC2-1 nil 3569777912 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (Bfun_TCC3 0 (Bfun_TCC3-1 nil 3569777912 ("" (termination-tcc) nil nil) nil nil)) (Bfundef 0 (Bfundef-1 nil 3543578460 ("" (grind) nil nil) ((Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil)) shostak)) (Bfundef2 0 (Bfundef2-1 nil 3543651608 ("" (skeep) (("" (expand "Bfun" +) (("" (propax) nil nil)) nil)) nil) ((Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil)) shostak)) (Bfuneq_TCC1 0 (Bfuneq_TCC1-1 nil 3543651413 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil)) nil)) (Bfuneq_TCC2 0 (Bfuneq_TCC2-1 nil 3543651413 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil)) nil)) (Bfuneq 0 (Bfuneq-1 nil 3543651420 ("" (skeep) (("" (case "NOT Bfun(f, g)(b)(i) = Bfun(f, g)(b)(j)") (("1" (split -) (("1" (decompose-equality +) (("1" (lemma "Bfundef2") (("1" (inst-cp - "f" "g" "b" "i") (("1" (inst - "f" "g" "b" "j") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "Bfundef2") (("2" (decompose-equality +) (("2" (inst-cp - "f" "g" "b" "i") (("1" (inst - "f" "g" "b" "j") (("1" (expand "injective?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4) (("2" (induct "k") (("1" (assert) nil nil) ("2" (skolem 1 "k") (("2" (flatten) (("2" (assert) (("2" (case "Bfun(f, g)(b)(-1 - k + i)`2 = Bfun(f, g)(b)(-1 - k + j)`2") (("1" (lemma "Bfundef2") (("1" (inst - "f" "g" "b" "-1-k+i") (("1" (lemma "Bfundef2") (("1" (inst - "f" "g" "b" "-1-k+j") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -2 :dir rl) (("1" (expand "injective?") (("1" (inst?) (("1" (assert) (("1" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "Bfundef") (("2" (inst-cp - "f" "g" "b" "-1-k+i") (("2" (inst - "f" "g" "b" "-1-k+j") (("2" (assert) (("2" (expand "injective?" -8) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (injective? const-decl "bool" functions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (j skolem-const-decl "nat" cantor_bernstein_schroeder nil) (Bfundef2 formula-decl nil cantor_bernstein_schroeder nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Bfundef formula-decl nil cantor_bernstein_schroeder nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (ABfun 0 (ABfun-1 nil 3543568460 ("" (case "FORALL (f: [A -> B], g: [B -> A], a: A, i: nat): Afun(f, g)(a)(i+1) = Bfun(f, g)(f(a))(i+1)") (("1" (skeep) (("1" (inst - "f" "g" "a" "i-1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "i") (("1" (assert) (("1" (skeep) (("1" (expand "Afun") (("1" (expand "Bfun") (("1" (expand "Afun") (("1" (expand "Bfun") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (skeep) (("2" (expand "Afun" +) (("2" (expand "Bfun" +) (("2" (inst - "f" "g" "a") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil)) shostak)) (BAfun 0 (BAfun-1 nil 3543568614 ("" (induct "i") (("1" (skeep) (("1" (assert) (("1" (expand "Bfun") (("1" (expand "Afun") (("1" (expand "Bfun") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (assert) (("2" (inst - "f" "g" "b") (("2" (expand "Bfun" +) (("2" (expand "Afun" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (ABfuneq_TCC1 0 (ABfuneq_TCC1-1 nil 3543653011 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil)) nil)) (ABfuneq_TCC2 0 (ABfuneq_TCC2-1 nil 3543653011 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil)) nil)) (ABfuneq 0 (ABfuneq-1 nil 3543653015 ("" (skeep) (("" (case "NOT Bfun(f, g)(b)(i) = Afun(f, g)(a)(j)") (("1" (split -) (("1" (decompose-equality +) (("1" (lemma "Bfundef2") (("1" (inst - "f" "g" "b" "i") (("1" (lemma "Afundef") (("1" (assert) (("1" (inst - "f" "g" "j" "a") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality +) (("2" (lemma "Bfundef2") (("2" (inst - "f" "g" "b" "i") (("1" (lemma "Afundef") (("1" (inst - "f" "g" "j" "a") (("1" (assert) (("1" (expand "injective?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4) (("2" (induct "k") (("1" (assert) nil nil) ("2" (skolem 1 "k") (("2" (flatten) (("2" (assert) (("2" (case "Bfun(f, g)(b)(-1 - k + i)`2 = Afun(f, g)(a)(-1 - k + j)`2") (("1" (lemma "Bfundef2") (("1" (inst - "f" "g" "b" "-1-k+i") (("1" (lemma "Afundef") (("1" (inst - "f" "g" "-1-k+j" "a") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -2 :dir rl) (("1" (expand "injective?") (("1" (inst?) (("1" (assert) (("1" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "Bfundef") (("2" (inst - "f" "g" "b" "-1-k+i") (("2" (lemma "Afundef2") (("2" (inst - "f" "g" "-1-k+j" "a") (("2" (assert) (("2" (expand "injective?" -8) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (injective? const-decl "bool" functions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Bfundef2 formula-decl nil cantor_bernstein_schroeder nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (j skolem-const-decl "nat" cantor_bernstein_schroeder nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Bfundef formula-decl nil cantor_bernstein_schroeder nil) (Afundef2 formula-decl nil cantor_bernstein_schroeder nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (ABrel_Arel_equiv 0 (ABrel_Arel_equiv-1 nil 3543649822 ("" (skeep) (("" (expand "ABrel") (("" (flatten) (("" (expand "Arel") (("" (split -1) (("1" (hide -2) (("1" (skeep -1) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "i" "a") (("1" (assert) (("1" (expand "preim_B?") (("1" (inst? 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem -1 "ia") (("2" (case "ia = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (expand "preim_B?") (("1" (replace 1) (("1" (split -) (("1" (skolem -1 "iaa") (("1" (replace -3 -1) (("1" (case "iaa = 0") (("1" (replace -1) (("1" (expand "Afun" -2) (("1" (inst 3 "0") (("1" (expand "Bfun" 3) (("1" (replace 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Afundef2") (("2" (inst - "f" "g" "iaa-1" "aa") (("1" (replace -2 -1 :dir rl) (("1" (expand "injective?" -6) (("1" (inst? -6) (("1" (assert) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "iaa-1" "aa") (("1" (assert) (("1" (replace -7) (("1" (replace -1 2 :dir rl) (("1" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem -1 "ii") (("2" (replace -3 -1) (("2" (rewrite "BAfun" -1 :dir rl) (("2" (replace -1 3) (("2" (inst? 3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -) (("1" (skolem -1 "iaa") (("1" (lemma "ABfuneq") (("1" (inst - "f" "g" "ia" "iaa" "b" "aa") (("1" (assert) (("1" (case "ia > iaa") (("1" (inst - "iaa") (("1" (assert) (("1" (case "NOT Bfun(f, g)(b)(ia - iaa)`1 = Afun(f, g)(aa)(0)`1") (("1" (assert) nil nil) ("2" (expand "Afun" -1) (("2" (replace -1 4 :dir rl) (("2" (inst? 4) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "ia-1") (("2" (assert) (("2" (expand "Bfun" -1) (("2" (decompose-equality -1) (("2" (lemma "Afundef2") (("2" (inst - "f" "g" "-ia+iaa" "aa") (("2" (assert) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (expand "injective?" -6) (("2" (inst - "Bfun(f, g)(b)(0)`2" "Afun(f, g)(aa)(-ia + iaa)`2") (("2" (assert) (("2" (expand "Bfun" -6) (("2" (expand "preim_B?") (("2" (replace 3) (("2" (lemma "Afundef") (("2" (inst - "f" "g" "-ia+iaa" "aa") (("2" (assert) (("2" (replace -1 :dir rl) (("2" (replace -7 3) (("2" (inst? 3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem -1 "iaa") (("2" (lemma "BAfun") (("2" (inst - "f" "g" "b" "ia-1") (("1" (assert) (("1" (replace -1 -3) (("1" (hide -1) (("1" (replace -2 -1) (("1" (rewrite "Afuncomp") (("1" (rewrite "BAfun" -1 :dir rl) (("1" (replace -1 4) (("1" (inst? 4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ABrel const-decl "bool" cantor_bernstein_schroeder nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil) (ABfuneq formula-decl nil cantor_bernstein_schroeder nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (Afuncomp formula-decl nil cantor_bernstein_schroeder nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (ia skolem-const-decl "nat" cantor_bernstein_schroeder nil) (Afundef2 formula-decl nil cantor_bernstein_schroeder nil) (injective? const-decl "bool" functions nil) (iaa skolem-const-decl "nat" cantor_bernstein_schroeder nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (BAfun formula-decl nil cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (preim_B? const-decl "bool" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil)) shostak)) (ABrel_Brel_equiv 0 (ABrel_Brel_equiv-1 nil 3543654002 ("" (skeep) (("" (expand "BArel") (("" (expand "Brel") (("" (expand "ABrel") (("" (flatten) (("" (ground) (("1" (skolem -1 "ibb") (("1" (case "NOT ibb = 0") (("1" (lemma "Bfundef2") (("1" (inst - "f" "g" "bb" "ibb") (("1" (expand "preim_B?") (("1" (replace -2 :dir rl) (("1" (replace -1 + :dir rl) (("1" (inst? 2) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (expand "preim_B?") (("2" (expand "Bfun" -2) (("2" (case "NOT b = bb") (("1" (assert) nil nil) ("2" (hide -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem -1 "ibb") (("2" (skolem - "ia") (("2" (case "ibb = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (case "NOT bb = b") (("1" (assert) nil nil) ("2" (hide -3) (("2" (replace -1) (("2" (replace -3 +) (("2" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "BAfun") (("2" (inst - "f" "g" "b" "ibb-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (replace -2 -1) (("1" (case "ia = 0") (("1" (replace -1) (("1" (expand "Afun" -3) (("1" (expand "preim_B?") (("1" (inst + "a") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "Afundef2") (("2" (rewrite "Afuncomp") (("2" (replace -1 +) (("2" (inst? 4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem -1 "ibb") (("3" (skolem - "ib") (("3" (case "ibb = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (case "NOT b = bb") (("1" (assert) nil nil) ("2" (hide -3) (("2" (replace -1 :dir rl) (("2" (replace -3 +) (("2" (inst? 3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ib = 0") (("1" (replace -1) (("1" (expand "Bfun" -3) (("1" (expand "preim_B?") (("1" (replace 2) (("1" (lemma "Bfundef") (("1" (inst - "f" "g" "bb" "ibb") (("1" (replace -3 :dir rl) (("1" (replace -1) (("1" (replace -4 4) (("1" (inst? 4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "BAfun") (("2" (inst - "f" "g" "bb" "ibb-1") (("1" (assert) (("1" (replace -1 -2) (("1" (hide -1) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "ibb-1" "g(bb)") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (replace -1 3 :dir rl) (("1" (expand "preim_B?") (("1" (inst? 3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skolem -1 "ibb") (("4" (skolem -2 "ia") (("4" (case "ibb = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (case "NOT bb = b") (("1" (assert) nil nil) ("2" (hide -3) (("2" (replace -1) (("2" (replace -3) (("2" (inst? 3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ia = 0") (("1" (replace -1) (("1" (expand "Bfun" -3) (("1" (expand "preim_B?") (("1" (replace 2) (("1" (lemma "BAfun") (("1" (inst - "f" "g" "b" "ibb-1") (("1" (assert) (("1" (replace -1) (("1" (replace -4 :dir rl) (("1" (replace -3) (("1" (inst? 3) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ibb >= ia") (("1" (lemma "BAfun") (("1" (inst - "f" "g" "b" "ibb-1") (("1" (assert) (("1" (replaces -1) (("1" (lemma "BAfun") (("1" (inst - "f" "g" "b" "ia-1") (("1" (assert) (("1" (replaces -1) (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "ia-1" "ibb-ia" "g(b)") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -4 :dir rl) (("1" (replace -3) (("1" (inst? 4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "BAfun") (("2" (inst - "f" "g" "b" "ibb-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "ibb-1" "g(b)") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (lemma "BAfun") (("1" (inst - "f" "g" "b" "ia-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "ibb-1" "ia-ibb" "g(b)") (("1" (assert) (("1" (lemma "ABfun") (("1" (inst - "f" "g" "Afun(f, g)(g(b))(ibb - 1)`1" "ia-ibb") (("1" (replace -1) (("1" (hide -1) (("1" (replace -2) (("1" (decompose-equality -1) (("1" (replace -5 :dir rl) (("1" (replace -1 :dir rl) (("1" (inst? 6) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((BArel const-decl "bool" cantor_bernstein_schroeder nil) (ABrel const-decl "bool" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (ibb skolem-const-decl "nat" cantor_bernstein_schroeder nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (preim_B? const-decl "bool" cantor_bernstein_schroeder nil) (Bfundef2 formula-decl nil cantor_bernstein_schroeder nil) (BAfun formula-decl nil cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Afuncomp formula-decl nil cantor_bernstein_schroeder nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (Afundef2 formula-decl nil cantor_bernstein_schroeder nil) (ibb skolem-const-decl "nat" cantor_bernstein_schroeder nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Bfundef formula-decl nil cantor_bernstein_schroeder nil) (ibb skolem-const-decl "nat" cantor_bernstein_schroeder nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (ibb skolem-const-decl "nat" cantor_bernstein_schroeder nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ABfun formula-decl nil cantor_bernstein_schroeder nil) (Brel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (Brel_Arel 0 (Brel_Arel-1 nil 3543668450 ("" (skeep) (("" (expand "Arel") (("" (expand "Brel") (("" (split) (("1" (flatten) (("1" (hide -2) (("1" (split) (("1" (skosimp*) (("1" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (case "b = bb") (("1" (hide -3) (("1" (replace -1 :dir rl) (("1" (inst + "0") (("1" (expand "Afun" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "BAfun") (("2" (inst - "f" "g" "bb" "i!1-1") (("1" (assert) (("1" (replace -1) (("1" (inst + "i!1") (("1" (expand "Afun" 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (case "bb = b") (("1" (replace -1) (("1" (inst 2 "0") (("1" (expand "Afun" 2) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "BAfun") (("2" (inst - "f" "g" "b" "i!1-1") (("1" (assert) (("1" (replace -1) (("1" (inst 3 "i!1") (("1" (expand "Afun" 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split) (("1" (skosimp*) (("1" (rewrite "BAfun" :dir rl) (("1" (lemma "Bfundef") (("1" (inst - "f" "g" "bb" "i!1") (("1" (replace -2 :dir rl) (("1" (expand "injective?") (("1" (inst? -3) (("1" (assert) (("1" (replace -3 1 :dir rl) (("1" (inst? 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "BAfun" :dir rl) (("2" (lemma "Bfundef") (("2" (inst - "f" "g" "b" "i!1") (("2" (replace -2 :dir rl) (("2" (expand "injective?") (("2" (inst? -3) (("2" (assert) (("2" (replace -3 + :dir rl) (("2" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Arel const-decl "bool" cantor_bernstein_schroeder nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (BAfun formula-decl nil cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (injective? const-decl "bool" functions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Bfundef formula-decl nil cantor_bernstein_schroeder nil) (Brel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (Arel_Brel 0 (Arel_Brel-1 nil 3543674748 ("" (skeep) (("" (iff) (("" (expand "Arel") (("" (expand "Brel") (("" (split) (("1" (flatten) (("1" (split) (("1" (skosimp*) (("1" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Afun" -2) (("1" (replace -2 :dir rl) (("1" (inst + "0") (("1" (expand "Bfun" 1) (("1" (lift-if) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun" -1) (("2" (lemma "Bfundef2") (("2" (inst - "f" "g" "f(aa)" "i!1") (("1" (replace -2 :dir rl) (("1" (inst + "i!1") nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Afun" -2) (("1" (replace -2) (("1" (inst 2 "0") (("1" (expand "Bfun" 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun" -1) (("2" (lemma "Bfundef2") (("2" (inst - "f" "g" "f(a)" "i!1") (("1" (replace -2 :dir rl) (("1" (inst 3 "i!1") nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split) (("1" (skosimp*) (("1" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (assert) (("1" (expand "injective?") (("1" (inst - "a" "aa") (("1" (assert) (("1" (inst + "0") (("1" (expand "Afun" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun" :dir rl) (("2" (lemma "Afundef") (("2" (inst - "f" "g" "i!1" "aa") (("2" (assert) (("2" (replace -2 :dir rl) (("2" (expand "injective?") (("2" (inst - "Afun(f,g)(aa)(i!1)`1" "a") (("2" (assert) (("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (assert) (("1" (expand "injective?") (("1" (inst - "aa" "a") (("1" (assert) (("1" (inst + "0") (("1" (expand "Afun" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun" :dir rl) (("2" (lemma "Afundef") (("2" (inst - "f" "g" "i!1" "a") (("2" (assert) (("2" (replace -2 :dir rl) (("2" (expand "injective?") (("2" (inst - "Afun(f,g)(a)(i!1)`1" "aa") (("2" (assert) (("2" (inst 3 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Brel const-decl "bool" cantor_bernstein_schroeder nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (injective? const-decl "bool" functions nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ABfun formula-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (Bfundef2 formula-decl nil cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (ABrel_Brel 0 (ABrel_Brel-1 nil 3543669377 ("" (skeep) (("" (expand "ABrel") (("" (expand "Brel") (("" (split) (("1" (flatten) (("1" (split) (("1" (skosimp*) (("1" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Afun" -2) (("1" (inst 2 "0") (("1" (expand "Bfun" 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun") (("2" (replace -1 +) (("2" (inst? 3) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "a = g(b)") (("1" (inst + "1") (("1" (expand "Bfun" 1) (("1" (expand "Bfun" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "f(a) = b") (("1" (inst + "0") (("1" (expand "Bfun" 2) (("1" (assert) nil nil)) nil)) nil) ("2" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + "i!1") (("2" (lemma "Bfundef") (("2" (inst - "f" "g" "b" "i!1-1") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (expand "Bfun" 4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (skosimp*) (("1" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (assert) (("1" (inst + "0") (("1" (expand "Afun" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 3 "i!1") (("2" (expand "injective?" -2) (("2" (inst - "a" "Bfun(f,g)(b)(i!1)`1") (("2" (assert) (("2" (lemma "Bfundef2") (("2" (inst - "f" "g" "b" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!1 = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (assert) (("1" (inst + "0") (("1" (expand "Afun" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun" :dir rl) (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ABrel const-decl "bool" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (ABfun formula-decl nil cantor_bernstein_schroeder nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Bfundef formula-decl nil cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (injective? const-decl "bool" functions nil) (Bfundef2 formula-decl nil cantor_bernstein_schroeder nil) (Brel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (Afununique 0 (Afununique-1 nil 3543584042 ("" (case "FORALL (f: [A -> B], g: [B -> A], a1, a2: A, i, j: nat): injective?(f) AND injective?(g) AND Afun(f, g)(a1)(i) = Afun(f, g)(a2)(j+i) IMPLIES Arel(f, g)(a1)(a2)") (("1" (skeep) (("1" (case "i >=j") (("1" (inst - "f" "g" "a2" "a1" "j" "i-j") (("1" (assert) (("1" (expand "Arel") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst - "f" "g" "a1" "a2" "i" "j-i") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (assert) (("1" (case "FORALL (f: [A -> B], g: [B -> A], a1, a2: A, i: nat): injective?(f) AND injective?(g) AND Afun(f, g)(a1)(i) = Afun(f, g)(a2)(i) IMPLIES a1=a2") (("1" (skeep) (("1" (inst - "f" "g" "a1" "a2" "i") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (expand "Arel") (("1" (flatten) (("1" (inst + "0") (("1" (expand "Afun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "i") (("1" (skeep) (("1" (expand "Afun") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (expand "Afun" -4) (("2" (flatten) (("2" (inst - "f" "g" "a1" "a2") (("2" (assert) (("2" (expand "injective?" -2) (("2" (inst - "Afun(f, g)(a1)(j)`2" "Afun(f, g)(a2)(j)`2") (("2" (assert) (("2" (decompose-equality +) (("2" (lemma "Afundef") (("2" (inst-cp - "f" "g" "j" "a1") (("2" (inst - "f" "g" "j" "a2") (("2" (assert) (("2" (expand "injective?") (("2" (inst - "Afun(f, g)(a1)(j)`1" "Afun(f, g)(a2)(j)`1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skolem 1 "ii") (("2" (flatten) (("2" (induct "i") (("1" (assert) (("1" (skeep) (("1" (expand "Afun" -3 1) (("1" (expand "Arel" 1) (("1" (flatten) (("1" (inst + "1+ii") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skolem 1 "jj") (("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (expand "Afun" -4) (("2" (flatten) (("2" (case "Afun(f, g)(a1)(jj) = Afun(f, g)(a2)(1 + ii + jj)") (("1" (inst - "f" "g" "a1" "a2") (("1" (assert) nil nil)) nil) ("2" (case "Afun(f, g)(a1)(jj)`2 = Afun(f, g)(a2)(1 + ii + jj)`2") (("1" (lemma "Afundef") (("1" (inst - "f" "g" "jj" "a1") (("1" (lemma "Afundef") (("1" (inst - "f" "g" "1+ii+jj" "a2") (("1" (assert) (("1" (copy -5) (("1" (expand "injective?" -1) (("1" (replace -4 :dir rl) (("1" (replace -3 :dir rl) (("1" (inst?) (("1" (assert) (("1" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (copy -3) (("2" (expand "injective?" -1) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (j skolem-const-decl "nat" cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (= const-decl "[T, T -> boolean]" equalities nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (af_fun_TCC1 0 (af_fun_TCC1-1 nil 3543571589 ("" (skeep) (("" (typepred "an") (("" (expand "Arel") (("" (expand "ABrel") (("" (flatten) (("" (split -) (("1" (skeep -1) (("1" (case "i = 0") (("1" (replace -1) (("1" (inst + "0") (("1" (expand "Afun") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "ABfun") (("2" (inst - "f" "g" "an" "i") (("1" (inst 3 "i") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst + "i") (("2" (lemma "Afundef") (("2" (inst - "f" "g" "i" "a") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Arel const-decl "bool" cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (ABrel const-decl "bool" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (ABfun formula-decl nil cantor_bernstein_schroeder nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil)) nil)) (ag_fun_TCC1 0 (ag_fun_TCC1-1 nil 3543573646 ("" (skeep) (("" (typepred "bn") (("" (expand "ABrel") (("" (expand "Arel") (("" (flatten) (("" (split -) (("1" (skeep -1) (("1" (inst 2 "i+1") (("1" (expand "Afun" 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (case "i = 0") (("1" (replace -1) (("1" (expand "Bfun" -) (("1" (lift-if) (("1" (ground) (("1" (inst 2 "1") (("1" (expand "Afun" 2) (("1" (expand "Afun" 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 2 "0") (("2" (expand "Afun" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "BAfun") (("2" (inst - "f" "g" "bn" "i-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (inst + "i-1") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ABrel const-decl "bool" cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (BAfun formula-decl nil cantor_bernstein_schroeder nil)) nil)) (aginj 0 (aginj-1 nil 3543574727 ("" (skeep) (("" (expand "bijective?") (("" (case "injective?(ag_fun(f, g)(a)) AND injective?(af_fun(f, g)(a))") (("1" (flatten) (("1" (assert) (("1" (expand "surjective?") (("1" (skolem 1 "aa") (("1" (skolem 2 "bb") (("1" (typepred "aa") (("1" (typepred "bb") (("1" (case "EXISTS (az:A): f(az) = bb") (("1" (expand "ABrel") (("1" (expand "Arel") (("1" (skeep -1) (("1" (ground) (("1" (expand "ag_fun" +) (("1" (expand "af_fun" +) (("1" (inst 2 "az") (("1" (lemma "Afununique") (("1" (skosimp*) (("1" (inst - "f" "g" "az" "a" "0" "i!2") (("1" (assert) (("1" (split -) (("1" (expand "Arel" (-1 1)) (("1" (ground) nil nil)) nil) ("2" (expand "Afun" + 1) (("2" (copy -7) (("2" (expand "injective?" -1) (("2" (inst - "az" "Afun(f,g)(a)(i!2)`1") (("2" (assert) (("2" (split -) (("1" (decompose-equality +) nil nil) ("2" (lemma "Afundef") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ag_fun" +) (("2" (expand "af_fun" +) (("2" (lemma "Afundef") (("2" (inst - "f" "g" "i!2" "a") (("2" (assert) (("2" (replace -3 :dir rl) (("2" (inst 2 "Afun(f,g)(a)(i!2)`1") (("2" (assert) (("2" (expand "Arel" +) (("2" (flatten) (("2" (inst 2 "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "ABfun") (("3" (inst - "f" "g" "az" "i!2") (("1" (replace -4 -3 :dir rl) (("1" (replace -1 :dir rl) (("1" (inst 2 "az") (("1" (expand "af_fun" +) (("1" (propax) nil nil)) nil) ("2" (expand "Arel" +) (("2" (flatten) (("2" (inst? 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "i!2 = 0") (("1" (replace -1) (("1" (assert) (("1" (expand "Bfun" -3) (("1" (lift-if) (("1" (ground) (("1" (inst 3 "a") (("1" (expand "af_fun" +) (("1" (assert) nil nil)) nil) ("2" (expand "Arel" +) (("2" (flatten) (("2" (inst + "0") (("2" (expand "Afun" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "az") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (replace -3 -2 :dir rl) (("4" (case "i!2 = 0") (("1" (replace -1) (("1" (expand "Bfun" -3) (("1" (lift-if) (("1" (ground) (("1" (inst 2 "a") (("1" (expand "af_fun" +) (("1" (assert) nil nil)) nil) ("2" (expand "Arel" 1) (("2" (flatten) (("2" (inst + "0") (("2" (hide-all-but 1) (("2" (expand "Afun") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "az") nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ABfun" -2 :dir rl) (("2" (inst 3 "az") (("1" (expand "af_fun" 3) (("1" (propax) nil nil)) nil) ("2" (expand "Arel" +) (("2" (flatten) (("2" (inst 1 "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "ABrel_Arel_equiv") (("2" (inst - "f" "g" "bb" "a" "aa") (("2" (assert) (("2" (split -) (("1" (expand "ABrel" -1) (("1" (case "NOT EXISTS (i: nat): aa = Bfun(f, g)(bb)(i)`1") (("1" (assert) (("1" (replace 1) (("1" (skeep -1) (("1" (expand "ag_fun" +) (("1" (lemma "Afundef") (("1" (inst - "f" "g" "i" "aa") (("1" (assert) (("1" (inst 2 "Afun(f,g)(aa)(i)`1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (skeep -1) (("2" (case "i = 0") (("1" (replace -1) (("1" (expand "Bfun" -2) (("1" (assert) (("1" (replace 1) (("1" (inst 2 "bb") (("1" (expand "ag_fun" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Bfundef") (("2" (inst - "f" "g" "bb" "i-1") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (replace -1 3 :dir rl) (("1" (expand "ag_fun" +) (("1" (inst? 3) (("1" (lemma "ABrel_Brel_equiv") (("1" (inst - "f" "g" "bb" "Bfun(f, g)(bb)(i - 1)`2" "a") (("1" (assert) (("1" (split -) (("1" (expand "BArel") (("1" (propax) nil nil)) nil) ("2" (expand "preim_B?") (("2" (propax) nil nil)) nil) ("3" (expand "Brel" 1) (("3" (flatten) (("3" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "preim_B?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (expand "injective?") (("2" (ground) (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1") (("1" (expand "ag_fun") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -2) (("2" (inst - "x1!1" "x2!1") (("2" (expand "af_fun") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i skolem-const-decl "nat" cantor_bernstein_schroeder nil) (ABrel_Brel_equiv formula-decl nil cantor_bernstein_schroeder nil) (Brel const-decl "bool" cantor_bernstein_schroeder nil) (preim_B? const-decl "bool" cantor_bernstein_schroeder nil) (BArel const-decl "bool" cantor_bernstein_schroeder nil) (bb skolem-const-decl "(ABrel(f, g)(a))" cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (Bfundef formula-decl nil cantor_bernstein_schroeder nil) (ABrel_Arel_equiv formula-decl nil cantor_bernstein_schroeder nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (i!2 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (ABfun formula-decl nil cantor_bernstein_schroeder nil) (i!2 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (f skolem-const-decl "[A -> B]" cantor_bernstein_schroeder nil) (g skolem-const-decl "[B -> A]" cantor_bernstein_schroeder nil) (a skolem-const-decl "A" cantor_bernstein_schroeder nil) (az skolem-const-decl "A" cantor_bernstein_schroeder nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Afununique formula-decl nil cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (ABrel const-decl "bool" cantor_bernstein_schroeder nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil) (injective? const-decl "bool" functions nil) (ag_fun const-decl "[(ABrel(f, g)(a)) -> (Arel(f, g)(a))]" cantor_bernstein_schroeder nil) (af_fun const-decl "[(Arel(f, g)(a)) -> (ABrel(f, g)(a))]" cantor_bernstein_schroeder nil)) shostak)) (Arel_union 0 (Arel_union-1 nil 3543662140 ("" (skeep) (("" (inst + "a") (("" (expand "Arel") (("" (flatten) (("" (inst + "0") (("" (expand "Afun" 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((A formal-type-decl nil cantor_bernstein_schroeder nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (Arel_disjoint 0 (Arel_disjoint-1 nil 3543662349 ("" (case "FORALL (f: [A -> B], g: [B -> A], a1, a2, a, aa: A): Arel(f, g)(a1)(a) AND Arel(f, g)(a2)(a) AND Arel(f,g)(a1)(aa) AND injective?(g) AND inject Arel(f, g)(a2)(aa)") (("1" (skeep) (("1" (decompose-equality +) (("1" (inst-cp - "f" "g" "a1" "a2" "a" "x!1") (("1" (inst - "f" "g" "a2" "a1" "a" "x!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "Arel") (("2" (flatten) (("2" (ground) (("1" (skosimp*) (("1" (case "i!3 >= i!2") (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "i!2" "i!3-i!2" "a") (("1" (replace -4 :dir rl) (("1" (assert) (("1" (replace -1 :dir rl) (("1" (lemma "Afuneq") (("1" (inst - "f" "g" "i!1" "i!3-i!2" "aa" "a2") (("1" (assert) (("1" (case "i!3-i!2 >= i!1") (("1" (inst - "i!1") (("1" (assert) (("1" (expand "Afun" -2 1) (("1" (decompose-equality -2) (("1" (replace -1 +) (("1" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "i!3-i!2") (("2" (assert) (("2" (expand "Afun" - 2) (("2" (decompose-equality -1) (("2" (replace -1 + :dir rl) (("2" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "Afuncomp") (("2" (inst - "f" "g" "i!3" "i!2-i!3" "a") (("1" (replace -4 :dir rl) (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -2 -3) (("1" (rewrite "Afuncomp") (("1" (replace -3 +) (("1" (inst 2 "i!1+i!2-i!3") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!2>=i!3") (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "i!3" "i!2-i!3" "a") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -5 :dir rl) (("1" (case "i!2-i!3 >= i!1") (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "i!1" "i!2-i!3-i!1" "a1") (("1" (assert) (("1" (replace -5 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -6 +) (("1" (inst? 1) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "Afuncomp") (("2" (inst - "f" "g" "i!2-i!3" "i!1-i!2+i!3" "a1") (("1" (assert) (("1" (replace -5 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -4 +) (("1" (inst? 3) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "Afuncomp") (("2" (inst - "f" "g" "i!2" "i!3-i!2" "a") (("1" (assert) (("1" (replace -3 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -4 -2) (("1" (rewrite "Afuncomp") (("1" (replace -2 +) (("1" (hide-all-but (1 3)) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (replace -2 -3) (("3" (rewrite "Afuncomp") (("3" (replace -3 -1) (("3" (lemma "Afununique") (("3" (inst - "f" "g" "a2" "aa" "i!2+i!3" "i!1") (("3" (assert) (("3" (split -) (("1" (expand "Arel") (("1" (ground) nil nil)) nil) ("2" (decompose-equality +) (("2" (lemma "Afundef") (("2" (inst - "f" "g" "i!2+i!3" "a2") (("2" (lemma "Afundef") (("2" (inst - "f" "g" "i!1" "aa") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (replace -3 -1) (("4" (rewrite "Afuncomp") (("4" (replace -2 -1) (("4" (rewrite "Afuncomp") (("4" (replace -1 +) (("4" (inst? 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (replace -1 -3) (("5" (rewrite "Afuncomp") (("5" (replace -3 -2) (("5" (rewrite "Afuncomp") (("5" (replace -2 +) (("5" (hide-all-but 1) (("5" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (replace -3 -2) (("6" (rewrite "Afuncomp") (("6" (case "i!1 >= i!2 + i!3") (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "i!2+i!3" "i!1-i!2-i!3" "a1") (("1" (assert) (("1" (replace -4 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -3 +) (("1" (inst? 2) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "Afuncomp") (("2" (inst - "f" "g" "i!1" "i!2+i!3-i!1" "a1") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -3 +) (("1" (inst? 2) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (skosimp*) (("7" (replace -1 -3) (("7" (rewrite "Afuncomp") (("7" (replace -3 -2) (("7" (lemma "Afununique") (("7" (inst - "f" "g" "aa" "a2" "i!1+i!3" "i!2") (("7" (assert) (("7" (split -) (("1" (expand "Arel") (("1" (ground) nil nil)) nil) ("2" (decompose-equality +) (("2" (lemma "Afundef") (("2" (inst-cp - "f" "g" "i!1+i!3" "aa") (("2" (inst - "f" "g" "i!2" "a2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("8" (skosimp*) (("8" (replace -3 -2) (("8" (lemma "Afununique") (("8" (inst - "f" "g" "a1" "a2" "i!3" "i!2") (("8" (assert) (("8" (split -) (("1" (expand "Arel") (("1" (split -) (("1" (skosimp*) (("1" (replace -1 -2) (("1" (rewrite "Afuncomp") (("1" (replace -2 +) (("1" (hide-all-but 2) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!1 >= i!4") (("1" (lemma "Afuncomp") (("1" (inst - "f" "g" "i!4" "i!1-i!4" "a1") (("1" (assert) (("1" (replace -3 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -4 +) (("1" (inst? 2) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "Afuncomp") (("2" (inst - "f" "g" "i!1" "i!4-i!1" "a1") (("1" (assert) (("1" (replace -3 :dir rl) (("1" (replace -1 :dir rl) (("1" (replace -2 +) (("1" (inst? 2) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Afundef") (("2" (inst-cp - "f" "g" "i!3" "a1") (("2" (inst - "f" "g" "i!2" "a2") (("2" (assert) (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!3 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!2 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (int_plus_int_is_int application-judgement "int" integers nil) (Afuneq formula-decl nil cantor_bernstein_schroeder nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Afuncomp formula-decl nil cantor_bernstein_schroeder nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (i!2 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!3 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (Afundef formula-decl nil cantor_bernstein_schroeder nil) (Afununique formula-decl nil cantor_bernstein_schroeder nil) (i!2 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!3 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!1 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (i!4 skolem-const-decl "nat" cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil) (injective? const-decl "bool" functions nil)) shostak)) (Brel_disjoint 0 (Brel_disjoint-1 nil 3543675465 ("" (skeep) (("" (rewrite "Brel_Arel") (("" (rewrite "Brel_Arel") (("" (decompose-equality) (("" (rewrite "Brel_Arel") (("" (rewrite "Brel_Arel") (("" (lemma "Arel_disjoint") (("" (inst - "f" "g" "g(b1)" "g(b2)" "g(b)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Brel_Arel formula-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (bool nonempty-type-eq-decl nil booleans nil) (Brel const-decl "bool" cantor_bernstein_schroeder nil) (boolean nonempty-type-decl nil booleans nil) (Arel_disjoint formula-decl nil cantor_bernstein_schroeder nil)) shostak)) (ABrel_union 0 (ABrel_union-1 nil 3543662225 ("" (skeep) (("" (inst + "g(b)") (("" (expand "ABrel") (("" (flatten) (("" (inst 2 "1") (("" (expand "Bfun" 2) (("" (expand "Bfun" 2) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (Bfun def-decl "[A, B]" cantor_bernstein_schroeder nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (ABrel const-decl "bool" cantor_bernstein_schroeder nil)) shostak)) (ABrel_disjoint 0 (ABrel_disjoint-1 nil 3543666063 ("" (case "FORALL (f: [A -> B], g: [B -> A], a1, a2: A, b,bb: B): ABrel(f, g)(a1)(b) AND ABrel(f, g)(a2)(b) AND ABrel(f, g)(a1)(bb) AND injective?(g) AND injective?(f) IMPLIES ABrel(f, g)(a2)(bb)") (("1" (skeep) (("1" (decompose-equality +) (("1" (inst-cp - "f" "g" "a1" "a2" "b" "x!1") (("1" (inst - "f" "g" "a2" "a1" "b" "x!1") (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (lemma "ABrel_Brel") (("2" (assert) (("2" (inst - "f" "g" _ _) (("2" (inst-cp - "b" "a1") (("2" (inst-cp - "b" "a2") (("2" (inst-cp - "bb" "a1") (("2" (inst - "bb" "a2") (("2" (assert) (("2" (hide (-4 -5 -6 2)) (("2" (rewrite "Brel_Arel") (("2" (rewrite "Brel_Arel") (("2" (rewrite "Brel_Arel") (("2" (rewrite "Brel_Arel") (("2" (lemma "Arel_disjoint") (("2" (inst - "f" "g" "g(f(a1))" "g(f(a2))" "g(b)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ABrel_Brel formula-decl nil cantor_bernstein_schroeder nil) (Arel_disjoint formula-decl nil cantor_bernstein_schroeder nil) (Brel_Arel formula-decl nil cantor_bernstein_schroeder nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ABrel const-decl "bool" cantor_bernstein_schroeder nil) (injective? const-decl "bool" functions nil)) shostak)) (Cantor_Bernstein_Schroeder 0 (Cantor_Bernstein_Schroeder-1 nil 3543232089 ("" (skeep) (("" (case "EXISTS (SS:set[A], FF:[(SS)->[set[A],set[B]]]): (FORALL (a:A): EXISTS (ss:(SS)): F (("1" (skeep -1) (("1" (case "FORALL (ss: (SS)): (EXISTS (hab: [(FF(ss)`1) -> (FF(ss)`2)]): bijective?(hab))") (("1" (hide (-5 -6)) (("1" (name "afun" "LAMBDA (a:A): choose({ss:(SS) | FF(ss)`1(a)})") (("1" (case "FORALL (a:A): FF(afun(a))`1(a)") (("1" (hide -2) (("1" (name "habfun" "LAMBDA (ss:(SS)): choose({hab:[(FF(ss)`1)->(FF(ss)`2)]|bijective?(hab)})") (("1" (inst + "LAMBDA (a:A): habfun(afun(a))(a)") (("1" (expand "bijective?") (("1" (split +) (("1" (expand "injective?" +) (("1" (skeep) (("1" (case "afun(x1) = afun(x2)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (typepred "habfun(afun(x1))") (("1" (expand "bijective?" -1) (("1" (flatten) (("1" (expand "injective?" -1) (("1" (inst - "x1" "x2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "afun(x1)" "afun(x2)") (("2" (assert) (("2" (flatten) (("2" (copy -8) (("2" (expand "disjoint?" -1) (("2" (expand "empty?" -1) (("2" (expand "intersection" -1) (("2" (expand "member" -1) (("2" (inst - "habfun(afun(x1))(x1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?" +) (("2" (skolem 1 "b") (("2" (case "EXISTS (aa:A): FF(afun(aa))`2(b)") (("1" (skeep -1) (("1" (typepred "habfun(afun(aa))") (("1" (expand "bijective?" -1) (("1" (flatten) (("1" (hide -1) (("1" (expand "surjective?" -1) (("1" (inst - "b") (("1" (skeep -1) (("1" (case "afun(aa) = afun(x)") (("1" (inst + "x") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (inst - "afun(aa)" "afun(x)") (("2" (assert) (("2" (flatten) (("2" (copy -9) (("2" (expand "disjoint?" -1) (("2" (expand "empty?" -1) (("2" (expand "member" -1) (("2" (expand "intersection" -1) (("2" (expand "member" -1) (("2" (inst - "b") (("2" (assert) (("2" (typepred "x") (("2" (inst - "x") (("2" (copy -9) (("2" (expand "disjoint?" -1) (("2" (expand "empty?" -1) (("2" (expand "intersection" -1) (("2" (inst - "x") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst -5 "b") (("2" (skosimp*) (("2" (inst -3 "ss!1") (("2" (skosimp*) (("2" (expand "surjective?") (("2" (inst -4 "b") (("2" (skosimp*) (("2" (inst + "x!1") (("2" (case "FF(afun(x!1))`2 = FF(ss!1)`2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (inst - "ss!1" "afun(x!1)") (("2" (assert) (("2" (flatten) (("2" (typepred "x!1") (("2" (inst - "x!1") (("2" (copy -8) (("2" (expand "disjoint?" -1) (("2" (expand "intersection" -1) (("2" (expand "empty?" -1) (("2" (expand "member") (("2" (inst - "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -3 "ss!1") (("2" (skosimp*) (("2" (inst - "hab!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst -3 "a!1") (("2" (skosimp*) (("2" (inst - "ss!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (inst -4 "ss") (("2" (ground) (("2" (skeep -1) (("2" (inst + "inverse(hab)") (("1" (lemma "bij_inv_is_bij[(FF(ss)`2),(FF(ss)`1)]") (("1" (inst - "hab") (("1" (assert) nil nil)) nil) ("2" (inst -5 "ss") (("2" (flatten) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -5 "ss") (("2" (flatten) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "EXISTS (SS: set[A], FF: [(SS) -> [set[A], set[B]]]): (FORALL (a: A): EXISTS (ss: (SS)): FF(ss)`1(a)) AND (FORALL (b: B): EXISTS (ss: (SS)): FF(ss)`2(b)) AND (FORALL (ss1, ss2: (SS)): ss1 /= ss2 AND ((NOT disjoint?(FF(ss1)`1, FF(ss2)`1)) OR (NOT disjoint?(FF(ss1)`2, FF(ss2)`2))) IMPLIES FF(ss1) = FF(ss2)) AND (FORALL (ss: (SS)): (EXISTS (hab: [(FF(ss)`1) -> (FF(ss)`2)]): bijective?(hab)) OR (EXISTS (hab: [(FF(ss)`2) -> (FF(ss)`1)]): bijective?(hab))) AND (FORALL (ss: (SS)): nonempty?(FF(ss)`1) AND nonempty?(FF(ss)`2))") (("1" (skeep -1) (("1" (name "ffim" "{abset:[set[A],set[B]]|EXISTS (ss:(SS)): FF(ss) = abset}") (("1" (case "FORALL (abset:(ffim)): EXISTS (ss:(SS)): FF(ss) = abset") (("1" (name "ssch" "LAMBDA (abset:(ffim)): choose({ss:(SS)|FF(ss) = abset})") (("1" (case "FORALL (abset:(ffim)): FF(ssch(abset)) = abset") (("1" (name "SSset" "LAMBDA (fs:A): SS(fs) AND EXISTS (abset:(ffim)): fs = ssch(abset)") (("1" (name "FFex" "LAMBDA (ssn:(SSset)): FF(ssn)") (("1" (inst + "SSset" "FFex") (("1" (assert) (("1" (split +) (("1" (skosimp*) (("1" (inst -7 "a!1") (("1" (skosimp*) (("1" (inst -3 "FF(ss!1)") (("1" (inst + "ssch(FF(ss!1))") (("1" (expand "FFex" +) (("1" (assert) nil nil)) nil) ("2" (expand "SSset" +) (("2" (inst + "FF(ss!1)") nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "ffim" +) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -8 "b!1") (("2" (skosimp*) (("2" (inst -3 "FF(ss!1)") (("1" (inst + "ssch(FF(ss!1))") (("1" (expand "FFex" +) (("1" (assert) nil nil)) nil) ("2" (expand "SSset" +) (("2" (inst + "FF(ss!1)") nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "ffim" +) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (expand "disjoint?" +) (("3" (expand "FFex" +) (("3" (typepred "ss1") (("3" (typepred "ss2") (("3" (expand "SSset" (-1 -2)) (("3" (flatten) (("3" (inst -13 "ss1" "ss2") (("3" (assert) (("3" (expand "disjoint?") (("3" (case "NOT (((NOT empty?(intersection(FF(ss1)`1, FF(ss2)`1))) OR (NOT empty?(intersection(FF(ss1)`2, FF(ss2)`2)))))") (("1" (hide -) (("1" (ground) nil nil)) nil) ("2" (replace -1) (("2" (skolem -3 "abset2") (("2" (skolem -5 "abset1") (("2" (hide -1) (("2" (copy -7) (("2" (inst-cp - "abset1") (("2" (inst - "abset2") (("2" (replace -4 :dir rl) (("2" (replace -6 :dir rl) (("2" (assert) (("2" (replace -15 :dir rl) (("2" (replace -2 -1) (("2" (replace -1 :dir rl) (("2" (replace -6 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-10 1)) (("4" (skeep) (("4" (typepred "ss") (("4" (expand "SSset") (("4" (flatten) (("4" (hide -2) (("4" (inst - "ss") (("4" (split -) (("1" (skosimp*) (("1" (inst + "hab!1") (("1" (assert) (("1" (expand "bijective?") (("1" (hide 2) (("1" (expand "injective?") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (split) (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -1) (("2" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (expand "FFex") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "y!1") (("2" (expand "FFex") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "FFex") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 1) (("2" (inst + "hab!1") (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (expand "surjective?") (("1" (flatten) (("1" (split +) (("1" (hide -2) (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (skosimp*) (("2" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (expand "FFex") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "y!1") (("2" (expand "FFex") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "FFex") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but (-11 1)) (("5" (skosimp*) (("5" (typepred "ss!1") (("5" (expand "SSset") (("5" (flatten) (("5" (hide -2) (("5" (inst - "ss!1") (("5" (expand "FFex") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (typepred "ssn") (("2" (expand "SSset") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "nonempty?" +) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -2 "abset") (("2" (skosimp*) (("2" (inst - "ss!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "abset!1") (("2" (expand "ffim" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "fullset[A]" "LAMBDA (a:(fullset[A])): (Arel(f,g)(a),ABrel(f,g)(a))") (("2" (assert) (("2" (ground) (("1" (skosimp*) (("1" (lemma "Arel_union") (("1" (inst - "f" "g" "a!1") (("1" (skosimp*) (("1" (inst + "aa!1") (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "ABrel_union") (("2" (inst - "f" "g" "b!1") (("2" (skosimp*) (("2" (inst + "a!1") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem 1 ("a1" "a2")) (("3" (flatten) (("3" (split -) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (expand "intersection") (("1" (expand "member") (("1" (skolem 1 "aa") (("1" (flatten) (("1" (lemma "Arel_disjoint") (("1" (inst - "f" "g" "a1" "a2" "aa") (("1" (assert) (("1" (decompose-equality 2) (("1" (name "bb" "x!1") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "ABrel_Brel") (("1" (rewrite "ABrel_Brel") (("1" (rewrite "Arel_Brel" -) (("1" (rewrite "Arel_Brel" -) (("1" (lemma "Brel_disjoint") (("1" (inst - "f" "g" "f(a1)" "f(a2)" "f(aa)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skolem 1 "b") (("2" (flatten) (("2" (lemma "ABrel_disjoint") (("2" (inst - "f" "g" "a1" "a2" "b") (("2" (assert) (("2" (rewrite "ABrel_Brel") (("2" (rewrite "ABrel_Brel") (("2" (decompose-equality 2) (("2" (rewrite "Arel_Brel") (("2" (rewrite "Arel_Brel") (("2" (lemma "Brel_disjoint") (("2" (inst - "f" "g" "f(a1)" "f(a2)" "b") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (lemma "aginj") (("4" (inst - "f" "g" "ss") (("4" (assert) (("4" (inst + "af_fun(f,g)(ss)") (("4" (inst + "ag_fun(f,g)(ss)") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (expand "member") (("5" (split) (("1" (inst - "ss") (("1" (expand "Arel") (("1" (flatten) (("1" (inst + "0") (("1" (expand "Afun" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "f(ss)") (("2" (expand "ABrel") (("2" (flatten) (("2" (inst + "0") (("2" (expand "Afun" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (bijective? const-decl "bool" functions nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (disjoint? const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (B formal-type-decl nil cantor_bernstein_schroeder nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (A formal-type-decl nil cantor_bernstein_schroeder nil) (= const-decl "[T, T -> boolean]" equalities nil) (choose const-decl "(p)" sets nil) (SS skolem-const-decl "set[A]" cantor_bernstein_schroeder nil) (FF skolem-const-decl "[(SS) -> [set[A], set[B]]]" cantor_bernstein_schroeder nil) (afun skolem-const-decl "[a: A -> ({ss: (SS) | FF(ss)`1(a)})]" cantor_bernstein_schroeder nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (ss!1 skolem-const-decl "(SS)" cantor_bernstein_schroeder nil) (aa skolem-const-decl "A" cantor_bernstein_schroeder nil) (b skolem-const-decl "B" cantor_bernstein_schroeder nil) (surjective? const-decl "bool" functions nil) (ss skolem-const-decl "(SS)" cantor_bernstein_schroeder nil) (TRUE const-decl "bool" booleans nil) (inverse const-decl "D" function_inverse nil) (x!2 skolem-const-decl "B" cantor_bernstein_schroeder nil) (bij_inv_is_bij formula-decl nil function_inverse nil) (x!2 skolem-const-decl "B" cantor_bernstein_schroeder nil) (ffim skolem-const-decl "[[set[A], set[B]] -> boolean]" cantor_bernstein_schroeder nil) (SS skolem-const-decl "set[A]" cantor_bernstein_schroeder nil) (FF skolem-const-decl "[(SS) -> [set[A], set[B]]]" cantor_bernstein_schroeder nil) (ss!1 skolem-const-decl "(SS)" cantor_bernstein_schroeder nil) (FFex skolem-const-decl "[(SSset) -> [set[A], set[B]]]" cantor_bernstein_schroeder nil) (ssch skolem-const-decl "[abset: (ffim) -> ({ss: (SS) | FF(ss) = abset})]" cantor_bernstein_schroeder nil) (SSset skolem-const-decl "[A -> boolean]" cantor_bernstein_schroeder nil) (ss!1 skolem-const-decl "(SS)" cantor_bernstein_schroeder nil) (ss1 skolem-const-decl "(SSset)" cantor_bernstein_schroeder nil) (ss2 skolem-const-decl "(SSset)" cantor_bernstein_schroeder nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (hab!1 skolem-const-decl "[(FF(ss)`1) -> (FF(ss)`2)]" cantor_bernstein_schroeder nil) (y!1 skolem-const-decl "(FFex(ss)`2)" cantor_bernstein_schroeder nil) (x!1 skolem-const-decl "(FF(ss)`1)" cantor_bernstein_schroeder nil) (x!1 skolem-const-decl "(FF(ss)`2)" cantor_bernstein_schroeder nil) (y!1 skolem-const-decl "(FFex(ss)`1)" cantor_bernstein_schroeder nil) (hab!1 skolem-const-decl "[(FF(ss)`2) -> (FF(ss)`1)]" cantor_bernstein_schroeder nil) (ss skolem-const-decl "(SSset)" cantor_bernstein_schroeder nil) (ss!1 skolem-const-decl "(SSset)" cantor_bernstein_schroeder nil) (ABrel const-decl "bool" cantor_bernstein_schroeder nil) (Arel const-decl "bool" cantor_bernstein_schroeder nil) (fullset const-decl "set" sets nil) (Arel_union formula-decl nil cantor_bernstein_schroeder nil) (aa!1 skolem-const-decl "A" cantor_bernstein_schroeder nil) (ABrel_union formula-decl nil cantor_bernstein_schroeder nil) (a!1 skolem-const-decl "A" cantor_bernstein_schroeder nil) (ABrel_disjoint formula-decl nil cantor_bernstein_schroeder nil) (Arel_disjoint formula-decl nil cantor_bernstein_schroeder nil) (Brel_disjoint formula-decl nil cantor_bernstein_schroeder nil) (Arel_Brel formula-decl nil cantor_bernstein_schroeder nil) (ABrel_Brel formula-decl nil cantor_bernstein_schroeder nil) (aginj formula-decl nil cantor_bernstein_schroeder nil) (ag_fun const-decl "[(ABrel(f, g)(a)) -> (Arel(f, g)(a))]" cantor_bernstein_schroeder nil) (af_fun const-decl "[(Arel(f, g)(a)) -> (ABrel(f, g)(a))]" cantor_bernstein_schroeder nil) (Afun def-decl "[A, B]" cantor_bernstein_schroeder nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.288Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26