Quellcode-Bibliothek cantor_bernstein_schroeder.prf
Sprache: Lisp
(cantor_bernstein_schroedernil 3543567590 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3543567590 ("" (termination-tcc) nil nil ) nil nil ))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 )nil naturalnumbers nil )"[A, B]" cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3543650214"" (skeep) (("" (expand "Afun" + 2) (("" (propax) nil nil )) nil ))nil )"[A, B]" cantor_bernstein_schroeder nil )) shostak))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" nil )"posint" nil )nil cantor_bernstein_schroeder nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[A, B]" cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nonneg_int" nil ))nil 3543650947 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"bool" functions nil ))nil ))nil 3543650947 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"bool" functions nil ))nil ))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" "1" assert )"1" 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" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil defined_types nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )"[A, B]" cantor_bernstein_schroeder nil )nil naturalnumbers nil )nil cantor_bernstein_schroeder nil )"bool" functions nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"posint" nil )"odd_int" integers nil )nil cantor_bernstein_schroeder nil )"posint" nil ))nil 3543569291 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil cantor_bernstein_schroeder nil )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )"bool" sets nil ))nil ))nil 3569777912 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3569777912 ("" (termination-tcc) nil nil ) nil nil ))nil 3543578460 ("" (grind) nil nil )"[A, B]" cantor_bernstein_schroeder nil )) shostak))nil 3543651608"" (skeep) (("" (expand "Bfun" +) (("" (propax) nil nil )) nil ))nil )"[A, B]" cantor_bernstein_schroeder nil )) shostak))nil 3543651413 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" functions nil ))nil ))nil 3543651413 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" functions nil ))nil ))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" "1" assert )"1" 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" "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 )"[A, B]" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nat" cantor_bernstein_schroeder nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"odd_int" integers nil )"posint" nil )nil cantor_bernstein_schroeder nil )"posint" nil ))nil ))nil 3543568460"" case "FORALL (f: [A -> B], g: [B -> A], a: A, i: nat): ") "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" nil )nil naturalnumbers nil )nil defined_types nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"[A, B]" cantor_bernstein_schroeder nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[A, B]" cantor_bernstein_schroeder nil ))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" nil )"odd_int" integers nil )nil naturalnumbers nil )"[A, B]" cantor_bernstein_schroeder nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[A, B]" cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil ))nil 3543653011 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"bool" functions nil ))nil ))nil 3543653011 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"bool" functions nil ))nil ))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" "1" assert )"1" 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" "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 )"[A, B]" cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nat" cantor_bernstein_schroeder nil )nil integers nil )nil integers nil )nil cantor_bernstein_schroeder nil )"(strict_total_order?[real])" real_props nil )nil cantor_bernstein_schroeder nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" cantor_bernstein_schroeder nil )"bool" reals nil ) (< const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"odd_int" integers nil )"posint" nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"posint" nil ))nil ))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" "0" )"1" expand "Bfun" 3)"1" replace 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "Afundef2" )"2" "f" "g" "iaa-1" "aa" )"1" replace -2 -1 :dir rl)"1" expand "injective?" -6)"1" "1" assert )"1" "Afundef" )"1" "f" "g" "iaa-1" "aa" )"1" assert )"1" replace -7)"1" replace "1" 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" "2" "Afundef2" )"2" "f" "g" "-ia+iaa" "aa" )"2" assert )"2" replace -1 :dir rl)"2" "2" expand "injective?" "2" "Bfun(f, g)(b)(0)`2" "Afun(f, g)(aa)(-ia + iaa)`2" )"2" assert )"2" expand "Bfun" "2" expand "preim_B?" )"2" replace 3)"2" "Afundef" )"2" "f" "g" "-ia+iaa" "aa" )"2" assert )"2" replace "2" replace "2" 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 )"bool" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )"int" integers nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" reals nil )nil cantor_bernstein_schroeder nil )"nonneg_int" nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"bool" functions nil )"nat" cantor_bernstein_schroeder nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil ))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" "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" "Bfundef" )"1" "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" "1" "Afundef" )"1" "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" "BAfun" )"1" "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" "1" "BAfun" )"1" "f" "g" "b" "ia-1" )"1" assert )"1" "1" "Afuncomp" )"1" "f" "g" "ia-1" "ibb-ia" "g(b)" )"1" assert )"1" replace -1 :dir rl)"1" replace -4 :dir rl)"1" replace -3)"1" 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" "1" "Afundef" )"1" "f" "g" "ibb-1" "g(b)" )"1" assert )"1" replace -2 :dir rl)"1" "BAfun" )"1" "f" "g" "b" "ia-1" )"1" assert )"1" replace -1)"1" "1" "Afuncomp" )"1" "f" "g" "ibb-1" "ia-ibb" "g(b)" )"1" assert )"1" "ABfun" )"1" "f" "g" "Afun(f, g)(g(b))(ibb - 1)`1" "ia-ibb" )"1" replace "1" "1" replace "1" "1" replace "1" replace "1" 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 )"bool" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nat" cantor_bernstein_schroeder nil )nil integers nil )nil integers nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"int" integers nil )"[A, B]" cantor_bernstein_schroeder nil )"[numfield, numfield -> numfield]" number_fields nil )nil cantor_bernstein_schroeder nil )"posint" nil )"nonneg_int" nil )"posint" nil )nil cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil ))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" "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 )"bool" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"int" integers nil )nil cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"posint" nil )"bool" functions nil )"posint" nil )nil cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil ))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" "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" "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" "Afun(f,g)(aa)(i!1)`1" "a" )"2" assert )"2" "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" "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" "Afun(f,g)(a)(i!1)`1" "aa" )"2" assert )"2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"bool" functions nil )"nat" cantor_bernstein_schroeder nil )"(strict_total_order?[real])" real_props nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil integers nil )"bool" reals nil )nil integers nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cantor_bernstein_schroeder nil ))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 )"bool" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"[A, B]" cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil integers nil )"bool" reals nil )nil integers nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"(strict_total_order?[real])" real_props nil )nil cantor_bernstein_schroeder nil )"int" integers nil )"nat" cantor_bernstein_schroeder nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )"bool" functions nil )nil cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil ))nil 3543584042"" case "FORALL (f: [A -> B], g: [B -> A], a1, a2: A, i, j: nat): AND 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): AND 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" "Afun(f, g)(a1)(j)`2" "Afun(f, g)(a2)(j)`2" )"2" assert )"2" "2" "Afundef" )"2" "f" "g" "j" "a1" )"2" "f" "g" "j" "a2" )"2" assert )"2" expand "injective?" )"2" "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" "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" "Afundef" )"1" "f" "g" "jj" "a1" )"1" "Afundef" )"1" "f" "g" "1+ii+jj" "a2" )"1" assert )"1" "1" expand "injective?" "1" replace -4 :dir rl)"1" replace "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "injective?" -1)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )nil cantor_bernstein_schroeder nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"int" integers nil )"nonneg_int" nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" functions nil )"[T, T -> boolean]" equalities nil )"[A, B]" cantor_bernstein_schroeder nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" cantor_bernstein_schroeder nil ))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 )"bool" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[A, B]" cantor_bernstein_schroeder nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nat" cantor_bernstein_schroeder nil )nil integers nil )nil integers nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil ))nil ))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 )"bool" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cantor_bernstein_schroeder nil )"posint" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[A, B]" cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )"[A, B]" cantor_bernstein_schroeder nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" cantor_bernstein_schroeder nil )"int" integers nil )nil cantor_bernstein_schroeder nil ))nil ))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" "1" expand "ag_fun" +)"1" expand "af_fun" +)"1" "az" )"1" "Afununique" )"1" "1" "f" "g" "az" "a" "0" "i!2" )"1" assert )"1" "1" expand "Arel" "1" nil nil ))nil )"2" expand "Afun" + 1)"2" "2" expand "injective?" "2" "az" "Afun(f,g)(a)(i!2)`1" )"2" assert )"2" "1" nil nil )"2" "Afundef" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ag_fun" +)"2" expand "af_fun" +)"2" "Afundef" )"2" "f" "g" "i!2" "a" )"2" assert )"2" replace -3 :dir rl)"2" "Afun(f,g)(a)(i!2)`1" )"2" assert )"2" expand "Arel" +)"2" "2" "i!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "ABfun" )"3" "f" "g" "az" "i!2" )"1" replace -4 -3 :dir rl)"1" replace -1 :dir rl)"1" "az" )"1" expand "af_fun" +)"1" (propax) nil nil ))nil )"2" expand "Arel" +)"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "i!2 = 0" )"1" replace -1)"1" assert )"1" expand "Bfun" -3)"1" "1" "1" "a" )"1" expand "af_fun" "1" assert )nil nil ))nil )"2" expand "Arel" +)"2" "2" "0" )"2" expand "Afun" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "az" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" "4" replace -3 -2 :dir rl)"4" case "i!2 = 0" )"1" replace -1)"1" expand "Bfun" -3)"1" "1" "1" "a" )"1" expand "af_fun" +)"1" assert )nil nil ))nil )"2" expand "Arel" 1)"2" "2" "0" )"2" "2" expand "Afun" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "az" )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "ABfun" -2 :dir rl)"2" "az" )"1" expand "af_fun" 3)"1" (propax) nil nil ))nil )"2" expand "Arel" +)"2" "2" "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" "1" expand "ABrel" -1)"1" case "NOT EXISTS (i: nat): aa = Bfun(f, g)(bb)(i)`1" )"1" assert )"1" replace 1)"1" "1" expand "ag_fun" +)"1" "Afundef" )"1" "f" "g" "i" "aa" )"1" assert )"1" "Afun(f,g)(aa)(i)`1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -1)"2" "2" case "i = 0" )"1" replace -1)"1" expand "Bfun" -2)"1" assert )"1" replace 1)"1" "bb" )"1" expand "ag_fun" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Bfundef" )"2" "f" "g" "bb" "i-1" )"1" assert )"1" replace "1" replace "1" expand "ag_fun" "1" "1" "ABrel_Brel_equiv" )"1" "f" "g" "bb" "Bfun(f, g)(bb)(i - 1)`2" "a" )"1" assert )"1" "1" expand "BArel" )"1" nil nil ))nil )"2" expand "preim_B?" )"2" nil nil ))nil )"3" expand "Brel" "3" "3" 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 )"bool" functions nil )"bool" functions nil )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"(ABrel(f, g)(a))" cantor_bernstein_schroedernil )"int" integers nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nat" cantor_bernstein_schroeder nil )nil integers nil )nil integers nil )"[A, B]" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"[A -> B]" cantor_bernstein_schroeder nil )"[B -> A]" cantor_bernstein_schroeder nil )"A" cantor_bernstein_schroeder nil )"A" cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"bool" functions nil )"[(ABrel(f, g)(a)) -> (Arel(f, g)(a))]" nil )"[(Arel(f, g)(a)) -> (ABrel(f, g)(a))]" nil ))nil 3543662140"" (skeep)"" (inst + "a" )"" (expand "Arel" )"" (flatten)"" (inst + "0" )"" (expand "Afun" 1) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" cantor_bernstein_schroeder nil ))nil 3543662349"" case "FORALL (f: [A -> B], g: [B -> A], a1, a2, a, aa: A): AND Arel(f, g)(a2)(a) AND Arel(f,g)(a1)(aa) AND injective?(g) AND injective?(f) IMPLIES") "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" "f" "g" "i!1" "i!3-i!2" "aa" "a2" )"1" assert )"1" case "i!3-i!2 >= i!1" )"1" "i!1" )"1" assert )"1" expand "Afun" -2 1)"1" "1" replace -1 +)"1" (inst? 2) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!3-i!2" )"2" assert )"2" expand "Afun" - 2)"2" "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" "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" "Afuncomp" )"1" "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" "Afuncomp" )"2" "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" "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" "f" "g" "a2" "aa" "i!2+i!3" "i!1" )"3" (assert )"3" (split -)"1" expand "Arel" )"1" (ground) nil nil ))nil )"2" "2" "Afundef" )"2" "f" "g" "i!2+i!3" "a2" )"2" "Afundef" )"2" "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" "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" "f" "g" "aa" "a2" "i!1+i!3" "i!2" )"7" (assert )"7" (split -)"1" expand "Arel" )"1" (ground) nil nil ))nil )"2" "2" "Afundef" )"2" "f" "g" "i!1+i!3" "aa" )"2" "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" "1" replace -1 -2)"1" rewrite "Afuncomp" )"1" replace -2 +)"1" "1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "i!1 >= i!4" )"1" "Afuncomp" )"1" "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" "Afuncomp" )"2" "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" "f" "g" "i!2" "a2" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"int" integers nil )nil cantor_bernstein_schroeder nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"[A, B]" cantor_bernstein_schroeder nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil cantor_bernstein_schroeder nil )"nonneg_int" nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )"nat" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" cantor_bernstein_schroeder nil )"bool" functions nil ))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 )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil booleans nil )"bool" cantor_bernstein_schroeder nil )nil booleans nil )nil cantor_bernstein_schroeder nil ))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 )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"[A, B]" cantor_bernstein_schroeder nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" cantor_bernstein_schroeder nil ))nil 3543666063"" case "FORALL (f: [A -> B], g: [B -> A], a1, a2: A, b,bb: B): AND AND ABrel(f, g)(a1)(bb) AND injective?(g) AND injective?(f)") "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" "Arel_disjoint" )"2" "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 )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" cantor_bernstein_schroeder nil )"bool" functions nil ))nil 3543232089"" (skeep)"" 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 IMPLIES disjoint?(FF(ss1)`1,FF(ss2)`1) AND disjoint?(FF(ss1)`2,FF(ss2)`2)) 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" case "FORALL (ss: (SS)): ") "1" (hide (-5 -6))"1" "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" "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" "1" "habfun(afun(x1))" )"1" expand "bijective?" -1)"1" "1" expand "injective?" -1)"1" "x1" "x2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "afun(x1)" "afun(x2)" )"2" assert )"2" "2" "2" expand "disjoint?" -1)"2" expand "empty?" -1)"2" expand "intersection" "2" expand "member" -1)"2" "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" "1" "habfun(afun(aa))" )"1" expand "bijective?" -1)"1" "1" "1" expand "surjective?" -1)"1" "b" )"1" "1" case "afun(aa) = afun(x)" )"1" "x" )"1" assert )nil nil ))nil )"2" "2" "afun(aa)" "afun(x)" )"2" assert )"2" "2" "2" expand "disjoint?" "2" expand "empty?" "2" expand "member" "2" expand "intersection" "2" expand "member" "2" "b" )"2" assert )"2" "x" )"2" "x" )"2" "2" expand "disjoint?" "2" expand "empty?" "2" expand "intersection" "2" "x" )"2" expand "member" )"2" 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" "2" "b" )"2" "2" "ss!1" )"2" "2" expand "surjective?" )"2" "b" )"2" "2" "x!1" )"2" case "FF(afun(x!1))`2 = FF(ss!1)`2" )"1" assert )nil nil )"2" "2" "ss!1" "afun(x!1)" )"2" assert )"2" "2" "x!1" )"2" "x!1" )"2" "2" expand "disjoint?" "2" expand "intersection" "2" expand "empty?" "2" expand "member" )"2" "x!1" )"2" 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" "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" "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" "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" "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], set [A], set [B]]]):AND (FORALL (b: B): EXISTS (ss: (SS)): FF(ss)`2(b))AND (FORALL (ss1, ss2: (SS)):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)):OR AND (FORALL (ss: (SS)):AND nonempty?(FF(ss)`2))") "1" (skeep -1)"1" "ffim" "{abset:[set[A],set[B]]|EXISTS (ss:(SS)): FF(ss) = abset}" )"1" case "FORALL (abset:(ffim)): EXISTS (ss:(SS)): FF(ss) = abset" )"1" "ssch" "LAMBDA (abset:(ffim)): choose({ss:(SS)|FF(ss) = abset})" )"1" case "FORALL (abset:(ffim)): FF(ssch(abset)) = abset" )"1" "SSset" "LAMBDA (fs:A): SS(fs) AND EXISTS (abset:(ffim)): fs = ssch(abset)" )"1" "FFex" "LAMBDA (ssn:(SSset)): FF(ssn)" )"1" (inst + "SSset" "FFex" )"1" (assert )"1" (split +)"1" "1" "a!1" )"1" "1" "FF(ss!1)" )"1" "ssch(FF(ss!1))" )"1" expand "FFex" +)"1" (assert ) nil nil ))nil )"2" expand "SSset" +)"2" "FF(ss!1)" )nil nil ))nil ))nil )"2" "2" expand "ffim" +)"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "b!1" )"2" "2" "FF(ss!1)" )"1" "ssch(FF(ss!1))" )"1" expand "FFex" +)"1" (assert ) nil nil ))nil )"2" expand "SSset" +)"2" "FF(ss!1)" )nil nil ))nil ))nil )"2" "2" expand "ffim" +)"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "disjoint?" +)"3" expand "FFex" +)"3" "ss1" )"3" "ss2" )"3" expand "SSset" (-1 -2))"3" "3" "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" "1" nil nil ))nil )"2" replace -1)"2" "abset2" )"2" "abset1" )"2" "2" "2" "abset1" )"2" "abset2" )"2" replace "2" replace "2" assert )"2" replace "2" replace "2" replace "2" replace "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" "4" "4" "ss" )"4" expand "SSset" )"4" "4" "4" "ss" )"4" "1" "1" "hab!1" )"1" assert )"1" expand "bijective?" )"1" "1" expand "injective?" )"1" expand "surjective?" )"1" "1" "1" "1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" "y!1" )"1" "1" "x!1" )"1" expand "FFex" )"1" nil nil ))nil ))nil ))nil )"2" "2" "y!1" )"2" expand "FFex" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "FFex" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "hab!1" )"1" expand "bijective?" )"1" expand "injective?" )"1" expand "surjective?" )"1" "1" "1" "1" "1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "y!1" )"1" "1" "x!1" )"1" expand "FFex" )"1" nil nil ))nil ))nil ))nil )"2" "2" "y!1" )"2" expand "FFex" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "FFex" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" "5" "ss!1" )"5" expand "SSset" )"5" "5" "5" "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" "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" "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" "aa" )"1" "1" "Arel_disjoint" )"1" "f" "g" "a1" "a2" "aa" )"1" assert )"1" "1" "bb" "x!1" )"1" replace -1)"1" "1" rewrite "ABrel_Brel" )"1" rewrite "ABrel_Brel" )"1" rewrite "Arel_Brel" "1" rewrite "Arel_Brel" "1" "Brel_disjoint" )"1" "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" "b" )"2" "2" "ABrel_disjoint" )"2" "f" "g" "a1" "a2" "b" )"2" assert )"2" rewrite "ABrel_Brel" )"2" rewrite "ABrel_Brel" )"2" "2" rewrite "Arel_Brel" )"2" rewrite "Arel_Brel" )"2" "Brel_disjoint" )"2" "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" "1" "0" )"1" expand "Afun" 1)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "f(ss)" )"2" expand "ABrel" )"2" "2" "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 )"bool" sets nil )"bool" functions nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil cantor_bernstein_schroeder nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil cantor_bernstein_schroeder nil )"[T, T -> boolean]" equalities nil )"(p)" sets nil )"set[A]" cantor_bernstein_schroeder nil )"[(SS) -> [set[A], set[B]]]" nil )"[a: A -> ({ss: (SS) | FF(ss)`1(a)})]" nil )"set" sets nil )"bool" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"(SS)" cantor_bernstein_schroeder nil )"A" cantor_bernstein_schroeder nil )"B" cantor_bernstein_schroeder nil )"bool" functions nil )"(SS)" cantor_bernstein_schroeder nil )"bool" booleans nil )"D" function_inverse nil )"B" cantor_bernstein_schroeder nil )nil function_inverse nil )"B" cantor_bernstein_schroeder nil )"[[set[A], set[B]] -> boolean]" nil )"set[A]" cantor_bernstein_schroeder nil )"[(SS) -> [set[A], set[B]]]" nil )"(SS)" cantor_bernstein_schroeder nil )"[(SSset) -> [set[A], set[B]]]" nil )"[abset: (ffim) -> ({ss: (SS) | FF(ss) = abset})]" nil )"[A -> boolean]" nil )"(SS)" cantor_bernstein_schroeder nil )"(SSset)" cantor_bernstein_schroeder nil )"(SSset)" cantor_bernstein_schroeder nil )"[bool, bool -> bool]" booleans nil )"[(FF(ss)`1) -> (FF(ss)`2)]" nil )"(FFex(ss)`2)" cantor_bernstein_schroedernil )"(FF(ss)`1)" cantor_bernstein_schroeder nil )"(FF(ss)`2)" cantor_bernstein_schroeder nil )"(FFex(ss)`1)" cantor_bernstein_schroedernil )"[(FF(ss)`2) -> (FF(ss)`1)]" nil )"(SSset)" cantor_bernstein_schroeder nil )"(SSset)" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"bool" cantor_bernstein_schroeder nil )"set" sets nil )nil cantor_bernstein_schroeder nil )"A" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"A" cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )nil cantor_bernstein_schroeder nil )"[(ABrel(f, g)(a)) -> (Arel(f, g)(a))]" nil )"[(Arel(f, g)(a)) -> (ABrel(f, g)(a))]" nil )"[A, B]" cantor_bernstein_schroeder nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.218Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
