|
(big_ops_nat
(big_ops_nat_TCC1 0
(big_ops_nat_TCC1-1 nil 3544531076 ("" (subtype-tcc) nil nil) nil
nil))
(big_ops_nat_eq 0
(big_ops_nat_eq-1 nil 3544529812
("" (skeep)
(("" (expand "big_ops_nat")
(("" (rewrite "for_eq")
(("" (rewrite "for_eq")
(("" (lemma "for_def_ext")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (expand "ext2int")
(("" (skosimp*)
(("" (inst - "x!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((big_ops_nat const-decl "T" big_ops_nat nil)
(ext2int const-decl "T" for_iterate nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(for_def_ext formula-decl nil for_iterate nil)
(T formal-type-decl nil big_ops_nat nil)
(ForBody type-eq-decl nil for_iterate nil)
(subrange type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(associative? const-decl "bool" operator_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND 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)
(for_eq formula-decl nil for_iterate nil))
shostak))
(big_ops_nat_expand_right_TCC1 0
(big_ops_nat_expand_right_TCC1-1 nil 3544531240
("" (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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(big_ops_nat_expand_right 0
(big_ops_nat_expand_right-1 nil 3544531246
("" (skeep)
(("" (invoke (name "rd" "%1") (! 1 2))
(("1" (replaces -1)
(("1" (expand "big_ops_nat")
(("1" (rewrite "for_eq")
(("1" (expand "for_def")
(("1" (lift-if)
(("1" (ground)
(("1" (expand "rd") (("1" (propax) nil nil)) nil)
("2" (expand "ext2int")
(("2" (lemma "for_eq")
(("2" (expand "ext2int")
(("2"
(inst - "i" "j-1" "id"
"LAMBDA (i_1: subrange(i,j-1), a: T):
a o F(i_1)")
(("2"
(invoke (case "%1 = %2") (! -1 2)
(! 2 1 1))
(("1" (replaces -1)
(("1"
(replace -1 :dir rl)
(("1"
(expand "rd" +)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(expand "big_ops_nat")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "for_def_ext" :dir rl)
(("1"
(skosimp*)
(("1" (assert) nil nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil)
("3" (skosimp*) (("3" (assert) nil nil))
nil)
("4" (skosimp*) (("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(T formal-type-decl nil big_ops_nat nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def 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)
(bool nonempty-type-eq-decl nil booleans 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil)
(for_def def-decl "T" for_iterate nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rd skolem-const-decl "T" big_ops_nat nil)
(for_def_ext formula-decl nil for_iterate nil)
(ext2int const-decl "T" for_iterate nil)
(for_eq formula-decl nil for_iterate nil)
(subrange type-eq-decl nil integers nil)
(ForBody type-eq-decl nil for_iterate nil))
nil))
(big_ops_nat_expand_left 0
(big_ops_nat_expand_left-1 nil 3544527918
(""
(case "FORALL (F: [nat -> T], i: nat, j: int, k:nat):
i<=j AND j-i <= k IMPLIES
big_ops_nat(i, j, F) =
(IF i <= j THEN F(i) o big_ops_nat(i + 1, j, F) ELSE id ENDIF)")
(("1" (skeep)
(("1" (case "i<=j")
(("1" (inst - "F" "i" "j" "j-i")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide -)
(("2" (assert)
(("2" (expand "big_ops_nat")
(("2" (expand "for")
(("2" (expand "for_it") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "k")
(("1" (skeep)
(("1" (case "j = i")
(("1" (replace -1)
(("1" (assert)
(("1" (expand "big_ops_nat")
(("1" (expand "for")
(("1" (expand "for_it")
(("1" (expand "for_it")
(("1" (typepred "id")
(("1" (inst?) (("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (skolem 1 "k")
(("2" (flatten)
(("2" (skeep)
(("2" (assert)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (invoke (name "egre" "%1") (! 1 1))
(("2" (replace -1)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (assert)
(("2" (lift-if)
(("2" (ground)
(("1"
(expand "egre" +)
(("1"
(inst - "F" "i" "j-1")
(("1"
(assert)
(("1"
(replace -3)
(("1"
(typepred "o")
(("1"
(expand "associative?")
(("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "i = j")
(("1"
(replace -)
(("1"
(expand "egre" +)
(("1"
(rewrite
"big_ops_nat_expand_right"
+)
(("1"
(typepred "id")
(("1"
(inst?)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(egre skolem-const-decl "T" big_ops_nat nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(for_it def-decl
"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}"
for_iterate nil)
(for const-decl "T" for_iterate nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(j skolem-const-decl "int" big_ops_nat nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(T formal-type-decl nil big_ops_nat nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil))
shostak))
(big_ops_nat_split 0
(big_ops_nat_split-1 nil 3544527659
(""
(case "FORALL (F: [nat -> T], i, j, z: nat):
i - 1 <= z AND z <= i+j IMPLIES
big_ops_nat(i, i+j, F) =
big_ops_nat(i, z, F) o big_ops_nat(z + 1, i+j, F)")
(("1" (skeep)
(("1" (case "j < i")
(("1" (expand "big_ops_nat" 1 1)
(("1" (expand "for" 1)
(("1" (expand "for_it" 1)
(("1" (assert)
(("1" (expand "big_ops_nat" 1 1)
(("1" (expand "for")
(("1" (expand "for_it")
(("1" (expand "big_ops_nat" 1 1)
(("1" (expand "for")
(("1" (expand "for_it")
(("1" (typepred "id")
(("1"
(inst - "id")
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst - "F" "i" "j-i" "z")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "j")
(("1" (skeep)
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (lift-if)
(("1" (lift-if)
(("1" (lift-if)
(("1"
(assert)
(("1"
(ground)
(("1"
(typepred "id")
(("1"
(inst?)
(("1" (ground) nil nil))
nil))
nil)
("2"
(typepred "id")
(("2"
(inst?)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem 1 "jj")
(("2" (flatten)
(("2" (skeep)
(("2" (assert)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (invoke (name "rd" "%1") (! 1 2 2))
(("2" (replace -1)
(("2" (rewrite "big_ops_nat_expand_right" -1)
(("2" (assert)
(("2" (lift-if)
(("2" (ground)
(("1"
(replace -2 :dir rl)
(("1"
(inst - "F" "i" "z")
(("1"
(assert)
(("1"
(replace -3)
(("1"
(typepred "o")
(("1"
(expand "associative?")
(("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "z = 1+i+jj")
(("1"
(replace -1)
(("1"
(replace -2 :dir rl)
(("1"
(invoke
(name "ed2" "%1")
(! 2 2 1))
(("1"
(replace -1)
(("1"
(rewrite
"big_ops_nat_expand_right"
-1)
(("1"
(assert)
(("1"
(replace -1 :dir rl)
(("1"
(typepred "id")
(("1"
(inst?)
(("1"
(assert)
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))
nil))
nil)
((big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(big_ops_nat_expand_left formula-decl nil big_ops_nat nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(j skolem-const-decl "int" big_ops_nat nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(for_it def-decl
"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}"
for_iterate nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(for const-decl "T" for_iterate nil)
(< const-decl "bool" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(T formal-type-decl nil big_ops_nat nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil))
shostak))
(big_ops_nat_shift 0
(big_ops_nat_shift-1 nil 3544532787
(""
(case "FORALL (F: [nat -> T], i: nat, jn:nat, p: int):
i + p >= 0 IMPLIES
big_ops_nat(i + p, i+jn + p, F) =
big_ops_nat(i, i+jn,
LAMBDA (k: nat):
IF k + p >= 0 THEN F(k + p) ELSE id ENDIF)")
(("1" (skeep)
(("1" (case "j < i")
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_right" +) nil nil))
nil))
nil)
("2" (inst - "F" "i" "j-i" "p")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "jn")
(("1" (skeep)
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left")
(("1" (rewrite "big_ops_nat_expand_left") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (assert)
(("2" (invoke (name "ed2" "%1") (! 1 2))
(("2" (replace -1)
(("2" (rewrite "big_ops_nat_expand_right" -1)
(("2" (replace -1 :dir rl)
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((big_ops_nat_expand_left formula-decl nil big_ops_nat nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
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_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j skolem-const-decl "int" big_ops_nat nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(real_le_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)
(< const-decl "bool" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(T formal-type-decl nil big_ops_nat nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil))
shostak))
(big_ops_nat_reverse 0
(big_ops_nat_reverse-1 nil 3544533459
(""
(case "FORALL (F: [nat -> T], i: nat, j: int,D:nat):
j>=i AND j-i<=D and commutative?[T](o) IMPLIES
big_ops_nat(i, j, F) =
big_ops_nat(i, j,
LAMBDA (k: nat):
IF i + j - k >= 0 THEN F(i + j - k) ELSE id ENDIF)")
(("1" (skeep)
(("1" (case "j)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_right" +) nil nil))
nil))
nil)
("2" (inst - "F" "i" "j" "j-i")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "D")
(("1" (assert)
(("1" (skeep)
(("1" (case "j = i")
(("1" (replace -1)
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (skolem 1 "DD")
(("2" (flatten)
(("2" (assert)
(("2" (skeep)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (invoke (name "ed2" "%1") (! 1 2))
(("2" (replace -1)
(("2" (rewrite "big_ops_nat_expand_left" -1)
(("2" (assert)
(("2" (replace -1 :dir rl)
(("2" (hide -1)
(("2"
(inst?)
(("2"
(assert)
(("2"
(case "j-1>=i")
(("1"
(assert)
(("1"
(replace -2)
(("1"
(lemma "big_ops_nat_shift")
(("1"
(inst - _ "i+1" "j" "-1")
(("1"
(assert)
(("1"
(inst
-
"LAMBDA (k: nat):
IF -1 - k + i + j >= 0 THEN F(-1 - k + i + j)
ELSE id
ENDIF")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(expand
"commutative?")
(("1"
(inst?)
(("1"
(replace -6)
(("1"
(hide -6)
(("1"
(invoke
(case
"%1 = %2")
(!
1
1
2)
(!
1
2
2))
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(assert)
(("2"
(rewrite
"big_ops_nat_eq")
(("2"
(skosimp*)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case "NOT j = i")
(("1" (assert) nil nil)
("2"
(rewrite
"big_ops_nat_expand_right"
+)
(("2"
(rewrite
"big_ops_nat_expand_right"
+)
(("2"
(typepred "id")
(("2"
(inst?)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(big_ops_nat_shift formula-decl nil big_ops_nat nil)
(big_ops_nat_eq formula-decl nil big_ops_nat nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(big_ops_nat_expand_left formula-decl nil big_ops_nat nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(j skolem-const-decl "int" big_ops_nat nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(real_le_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_plus_int_is_int application-judgement "int" integers nil)
(< const-decl "bool" reals nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(T formal-type-decl nil big_ops_nat nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(commutative? const-decl "bool" operator_defs nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil))
shostak))
(big_ops_nat_id 0
(big_ops_nat_id-1 nil 3544535047
("" (skeep)
(("" (case "j < i")
(("1" (rewrite "big_ops_nat_expand_right")
(("1" (assert) nil nil)) nil)
("2"
(case "FORALL (kj:nat): i+kj<=j IMPLIES big_ops_nat(i,i+kj,F) = id")
(("1" (inst - "j-i")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide 3)
(("2" (induct "kj")
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (inst - "i")
(("1" (assert)
(("1" (typepred "id")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem 1 "kj")
(("2" (flatten)
(("2" (assert)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (replace -1)
(("2" (inst?)
(("2" (assert)
(("2" (typepred "id")
(("2" (inst?) (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(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)
(T formal-type-decl nil big_ops_nat nil)
(big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j skolem-const-decl "int" big_ops_nat nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil))
shostak))
(big_ops_nat_comp 0
(big_ops_nat_comp-1 nil 3544536602
(""
(case "FORALL (F, G: [nat -> T], i: nat, D:nat):
commutative?[T](o) IMPLIES
big_ops_nat(i, i+D, F) o big_ops_nat(i, i+D, G) =
big_ops_nat(i, i+D, LAMBDA (k: nat): F(k) o G(k))")
(("1" (skeep)
(("1" (case "j < i")
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (assert)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (typepred "id")
(("1" (inst?) (("1" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (inst - "F" "G" "i" "j-i")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "D")
(("1" (assert)
(("1" (skeep)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (typepred "id")
(("1" (inst?)
(("1" (flatten)
(("1"
(replace -1)
(("1"
(hide (-1 -2))
(("1"
(typepred "id")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(replaces -1)
(("1"
(hide -1)
(("1"
(typepred "id")
(("1"
(inst?)
(("1"
(ground)
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 "DD")
(("2" (flatten)
(("2" (skeep)
(("2" (assert)
(("2" (invoke (name "eg1" "%1") (! 1 1 1))
(("2" (invoke (name "eg2" "%1") (! 1 1 2))
(("2" (invoke (name "eg3" "%1") (! 1 2))
(("2" (replace -1)
(("2" (replace -2)
(("2" (replace -3)
(("2"
(rewrite "big_ops_nat_expand_right" -1)
(("2"
(rewrite "big_ops_nat_expand_right" -2)
(("2"
(rewrite
"big_ops_nat_expand_right"
-3)
(("2"
(replaces -1 :dir rl)
(("2"
(replaces -1 :dir rl)
(("2"
(replaces -1 :dir rl)
(("2"
(inst?)
(("2"
(replace -1 :dir rl)
(("2"
(hide -1)
(("2"
(assert)
(("2"
(typepred "o")
(("2"
(expand
"associative?")
(("2"
(inst?)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(typepred
"o")
(("2"
(expand
"associative?")
(("2"
(inst?)
(("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(typepred
"o")
(("2"
(expand
"associative?")
(("2"
(copy
-1)
(("2"
(inst?)
(("2"
(replace
-1
:dir
rl)
(("2"
(hide
-1)
(("2"
(expand
"commutative?")
(("2"
(inst
-2
"F(1 + DD + i)"
"big_ops_nat(i, DD + i, G)")
(("2"
(replace
-2)
(("2"
(inst?)
(("2"
(replace
-1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j skolem-const-decl "int" big_ops_nat nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(T formal-type-decl nil big_ops_nat nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(commutative? const-decl "bool" operator_defs nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
shostak))
(big_ops_nat_distrib 0
(big_ops_nat_distrib-1 nil 3544537500
(""
(case "FORALL (*: [[T, T] -> T], F: [nat -> T], c: T, i: nat, jp: nat):
(FORALL (t1, t2, t3: T): t1 * (t2 o t3) = (t1 * t2) o (t1 * t3))
IMPLIES
c * big_ops_nat(i, i+jp, F) =
big_ops_nat(i, i+jp, LAMBDA (k: nat): c * F(k))")
(("1" (skeep)
(("1" (inst - "*" "F" "c" "i" "j-i")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (induct "jp")
(("1" (assert)
(("1" (skeep)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (rewrite "big_ops_nat_expand_right" +)
(("1" (typepred "id")
(("1" (inst?)
(("1" (flatten)
(("1" (replace -1)
(("1" (hide (-1 -2))
(("1"
(typepred "id")
(("1"
(inst?)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem 1 "jp")
(("2" (flatten)
(("2" (skeep)
(("2" (inst - "*" "F" "c" "i")
(("2" (assert)
(("2" (replace -2)
(("2" (assert)
(("2" (rewrite "big_ops_nat_expand_right" +)
(("2" (invoke (name "eg3" "%1") (! 1 2))
(("2" (replace -1)
(("2"
(rewrite "big_ops_nat_expand_right" -1)
(("2"
(replace -1 :dir rl)
(("2"
(hide -1)
(("2"
(inst?)
(("2"
(replace -1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(big_ops_nat_expand_right formula-decl nil big_ops_nat nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(id formal-const-decl
"{tid: T | FORALL (t: T): tid o t = t AND t o tid = t}"
big_ops_nat nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(i skolem-const-decl "nat" big_ops_nat nil)
(j skolem-const-decl "int" big_ops_nat nil)
(- const-decl "[numfield, numfield -> numfield]" 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(T formal-type-decl nil big_ops_nat nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(associative? const-decl "bool" operator_defs nil)
(O formal-const-decl "(associative?[T])" big_ops_nat nil)
(big_ops_nat const-decl "T" big_ops_nat nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.86 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
