|
(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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.74Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
