|
(for_iterate
(for_def_TCC1 0
(for_def_TCC1-1 nil 3508245294 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs 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))
nil))
(for_def_TCC2 0
(for_def_TCC2-1 nil 3508245294 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_def_inv 0
(for_def_inv-1 nil 3508245867
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "for_def" 1 2)
(("2" (expand "for_def" 1 1)
(("2" (inst? -1) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
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)
(for_def def-decl "T" for_iterate nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil for_iterate 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)
(int_plus_int_is_int application-judgement "int" integers nil))
shostak))
(for_shift 0
(for_shift-1 nil 3508269371
("" (skosimp*)
(("" (case "i!1 > j!1")
(("1" (grind) nil nil)
("2"
(case "FORALL(i:int,n:nat,shift:int,a:T,f:[[int,T]->T]):
for_def(i,n+i,a,f) = for_def(i+shift,n+i+shift,a,LAMBDA (k:int,t:T): f(k-shift,t))")
(("1" (inst -1 "i!1" "j!1-i!1" "shift!1" "a!1" "f!1")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide 2 3)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "for_def" 1 2)
(("2" (inst? -1)
(("2" (replaces -1 :dir rl)
(("2" (expand "for_def" 1 1)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(for_def def-decl "T" for_iterate 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!1 skolem-const-decl "int" for_iterate nil)
(i!1 skolem-const-decl "int" for_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil for_iterate nil)
(= const-decl "[T, T -> boolean]" equalities 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))
shostak))
(for_def_ext 0
(for_def_ext-1 nil 3508368586
("" (skosimp*)
(("" (case "i!1 > j!1")
(("1" (grind) nil nil)
("2"
(case "FORALL(i:int,n:nat,a:T,f,g:[[int,T]->T]) :
(FORALL (x:subrange(i,i+n),t:T) : f(x,t) = g(x,t))
IMPLIES
for_def(i,i+n,a,f) = for_def(i,i+n,a,g)")
(("1" (inst -1 "i!1" "j!1-i!1" "a!1" "f!1" "g!1")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide-all-but 1)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "for_def" 1)
(("2" (inst -1 "i" "a" "f" "g")
(("2" (split -1)
(("1" (inst? -2) (("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (skeep) (("2" (inst? -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(for_def def-decl "T" for_iterate nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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!1 skolem-const-decl "int" for_iterate nil)
(i!1 skolem-const-decl "int" for_iterate nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil for_iterate 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)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(for_def_induction_TCC1 0
(for_def_induction_TCC1-1 nil 3508423656 ("" (subtype-tcc) nil nil)
nil nil))
(for_def_induction_TCC2 0
(for_def_induction_TCC2-1 nil 3508423656 ("" (subtype-tcc) nil nil)
nil nil))
(for_def_induction_TCC3 0
(for_def_induction_TCC3-1 nil 3509187055 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_def_induction 0
(for_def_induction-1 nil 3508423656
("" (skosimp*)
(("" (case "i!1 > j!1")
(("1" (grind) nil nil)
("2"
(case "FORALL (i: int, n: nat, a: T, f: [[int, T] -> T], inv: PRED[[nat,T]]):
(inv(0,a) AND
(FORALL (k:upto(n),ak:T):
inv(k, ak) IMPLIES inv(k + 1,f(i+k,ak))))
IMPLIES inv(n+1, for_def(i,i+n,a,f))")
(("1" (inst -1 "i!1" "j!1-i!1" "a!1" "f!1" "inv!1")
(("1" (assert)
(("1" (expand "max")
(("1" (assert)
(("1" (skeep)
(("1" (inst? -) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (hide-all-but 1)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (copy -3)
(("2" (inst -1 "n+1" _)
(("2" (expand "for_def" 1)
(("2" (inst? -1)
(("2" (assert)
(("2" (hide 2)
(("2"
(inst? -1)
(("2"
(assert)
(("2"
(skeep 2)
(("2"
(inst? -3)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(for_def def-decl "T" for_iterate nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j!1 skolem-const-decl "int" for_iterate nil)
(i!1 skolem-const-decl "int" for_iterate nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(subrange type-eq-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil for_iterate nil)
(PRED type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(ext2int_TCC1 0
(ext2int_TCC1-1 nil 3508335744 ("" (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)
(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))
nil))
(for_it_TCC1 0
(for_it_TCC1-1 nil 3509456106 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(upfrom nonempty-type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs 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))
nil))
(for_it_TCC2 0
(for_it_TCC2-2 nil 3509456480
("" (skeep) (("" (expand "for_def") (("" (assert) nil nil)) nil))
nil)
((for_def def-decl "T" for_iterate nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil)
(for_it_TCC2-1 nil 3509456106 ("" (subtype-tcc) nil nil) nil nil))
(for_it_TCC3 0
(for_it_TCC3-1 nil 3509456106 ("" (subtype-tcc) nil nil) nil nil))
(for_it_TCC4 0
(for_it_TCC4-1 nil 3509456106 ("" (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)
(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)
(upfrom nonempty-type-eq-decl nil integers 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(for_it_TCC5 0
(for_it_TCC5-1 nil 3509456106 ("" (termination-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)
(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)
(upfrom nonempty-type-eq-decl nil integers nil)
(real_ge_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)
(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)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_it_TCC6 0
(for_it_TCC6-2 nil 3509456550
("" (skeep)
(("" (typepred "v(upfrom, i + 1, upto, f(i, a), f)")
(("" (lemma "for_def_inv")
(("" (inst -1 "i" "upto-i" "a" "ext2int(upfrom,upto,f)")
(("1" (assert)
(("1" (expand "ext2int" -1 2) (("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((ext2int const-decl "T" for_iterate nil)
(for_def def-decl "T" for_iterate nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(< const-decl "bool" reals nil)
(ForBody type-eq-decl nil for_iterate nil)
(subrange type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(upfrom nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals 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)
(int nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil for_iterate nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upto skolem-const-decl "int" for_iterate nil)
(upfrom skolem-const-decl "int" for_iterate nil)
(i skolem-const-decl "upfrom(upfrom)" for_iterate nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(for_def_inv formula-decl nil for_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil)
(for_it_TCC6-1 nil 3509456106 ("" (subtype-tcc) nil nil) nil nil))
(for_TCC1 0
(for_TCC1-1 nil 3505588136 ("" (subtype-tcc) nil nil) nil nil))
(for_eq 0
(for_eq-1 nil 3508252057
("" (skeep)
(("" (expand "for")
(("" (typepred "for_it(i,i,j,a,f)") (("" (propax) nil nil)) nil))
nil))
nil)
((for const-decl "T" for_iterate nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil for_iterate nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int nonempty-type-eq-decl nil integers nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(>= const-decl "bool" reals nil)
(upfrom nonempty-type-eq-decl nil integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(subrange type-eq-decl nil integers nil)
(ForBody type-eq-decl nil for_iterate nil)
(for_def def-decl "T" for_iterate nil)
(ext2int const-decl "T" for_iterate nil)
(for_it def-decl
"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}"
for_iterate nil))
shostak))
(for_induction_TCC1 0
(for_induction_TCC1-1 nil 3508423933 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_induction_TCC2 0
(for_induction_TCC2-1 nil 3508423933 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_induction_TCC3 0
(for_induction_TCC3-1 nil 3509180332 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_induction_TCC4 0
(for_induction_TCC4-1 nil 3509180332
("" (subtype-tcc) (("" (grind) nil nil)) nil) nil nil))
(for_induction_TCC5 0
(for_induction_TCC5-1 nil 3522757770 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_induction 0
(for_induction-1 nil 3508424040
("" (skeep)
(("" (case "n >= m")
(("1" (rewrite "for_eq")
(("1" (lemma "for_def_induction")
(("1"
(inst -1 "m" "n" "init" "ext2int(m,n,f)"
"LAMBDA(k:nat,ak:T): k > n-m+1 OR inv(k,ak)")
(("1" (assert)
(("1" (expand "max")
(("1" (expand "ext2int") (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (expand "for")
(("2" (expand "for_it") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(for_def_induction formula-decl nil for_iterate 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(PRED type-eq-decl nil defined_types nil)
(ext2int const-decl "T" for_iterate nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(m skolem-const-decl "int" for_iterate nil)
(n skolem-const-decl "{n: int | n >= m - 1}" for_iterate nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(ForBody type-eq-decl nil for_iterate nil)
(subrange type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil for_iterate nil)
(for_eq formula-decl nil for_iterate 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)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(for_down_def_TCC1 0
(for_down_def_TCC1-1 nil 3508264810 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs 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))
nil))
(for_down_def_TCC2 0
(for_down_def_TCC2-1 nil 3508264810 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs 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))
nil))
(for_down_def_ext 0
(for_down_def_ext-1 nil 3508369533
("" (skosimp*)
(("" (case "i!1 < j!1")
(("1" (grind) nil nil)
("2"
(case "FORALL(i:int,n:nat,a:T,f,g:[[int,T]->T]) :
(FORALL (x:subrange(i-n,i),t:T) : f(x,t) = g(x,t))
IMPLIES
for_down_def(i,i-n,a,f) = for_down_def(i,i-n,a,g)")
(("1" (inst -1 "i!1" "i!1-j!1" "a!1" "f!1" "g!1")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide-all-but 1)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "for_down_def" 1)
(("2" (inst -1 "i" "a" "f" "g")
(("2" (split -1)
(("1" (inst? -2) (("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (skeep) (("2" (inst? -1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(for_down_def def-decl "T" for_iterate nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(i!1 skolem-const-decl "int" for_iterate nil)
(j!1 skolem-const-decl "int" for_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil for_iterate 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)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil))
nil))
(for_down_up 0
(for_down_up-1 nil 3508359211
("" (skosimp*)
(("" (case "i!1 < j!1")
(("1" (grind) nil nil)
("2"
(case "FORALL (i:int, n:nat, a: T, f: [[int, T] -> T]):
for_down_def(i, i-n, a, f) =
for_def(i-n, i, a, LAMBDA (k: int, t: T): f(2*i - k - n, t))")
(("1" (inst -1 "i!1" "i!1-j!1" "a!1" "f!1")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide 2 3)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "for_down_def" 1)
(("2" (inst? -1)
(("2" (replaces -1)
(("2" (expand "for_def" 1 2)
(("2" (lemma "for_shift")
(("2" (inst? -1)
(("2"
(inst -1 "-1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(for_def def-decl "T" for_iterate nil)
(for_down_def def-decl "T" for_iterate nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(for_shift formula-decl nil for_iterate 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)
(i!1 skolem-const-decl "int" for_iterate nil)
(j!1 skolem-const-decl "int" for_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil for_iterate nil)
(= const-decl "[T, T -> boolean]" equalities 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))
shostak))
(for_down_def_induction_TCC1 0
(for_down_def_induction_TCC1-1 nil 3508440158
("" (subtype-tcc) nil nil) nil nil))
(for_down_def_induction_TCC2 0
(for_down_def_induction_TCC2-1 nil 3508440158
("" (subtype-tcc) nil nil) nil nil))
(for_down_def_induction_TCC3 0
(for_down_def_induction_TCC3-1 nil 3509187311
("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers 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)
(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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_down_def_induction 0
(for_down_def_induction-1 nil 3508440185
("" (skeep)
(("" (rewrite "for_down_up")
(("" (lemma "for_def_induction")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((for_down_up formula-decl nil for_iterate 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)
(T formal-type-decl nil for_iterate nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(PRED type-eq-decl nil defined_types nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(for_def_induction formula-decl nil for_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(for_down_TCC1 0
(for_down_TCC1-1 nil 3508265468 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_down_induction_TCC1 0
(for_down_induction_TCC1-1 nil 3508440597 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_down_induction_TCC2 0
(for_down_induction_TCC2-1 nil 3508440597 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_down_induction_TCC3 0
(for_down_induction_TCC3-1 nil 3509181991 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_down_induction_TCC4 0
(for_down_induction_TCC4-1 nil 3509181991
("" (subtype-tcc) (("" (grind) nil nil)) nil) nil nil))
(for_down_induction_TCC5 0
(for_down_induction_TCC5-1 nil 3522761922 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(for_down_induction 0
(for_down_induction-2 nil 3508440626
("" (skeep)
(("" (expand "for_down")
(("" (lemma "for_induction")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((for_down const-decl "T" for_iterate nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T formal-type-decl nil for_iterate nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(ForBody type-eq-decl nil for_iterate nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(PRED type-eq-decl nil defined_types nil)
(for_induction formula-decl nil for_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil)
(for_down_induction-1 nil 3508440598 ("" (postpone) nil nil) nil
shostak))
(for_down_eq 0
(for_down_eq-1 nil 3508265817
("" (skeep)
(("" (expand "for_down")
(("" (rewrite "for_eq")
(("" (lemma "for_down_up")
(("" (inst?)
((""
(case "(LAMBDA (k: int, t: T): ext2int(j, i, f)(i - k + j, t)) = ext2int(j, i,
LAMBDA (k: subrange(j, i), t: T): f(i - k + j, t))")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (decompose-equality 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((for_down const-decl "T" for_iterate nil)
(for_down_up formula-decl nil for_iterate nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ext2int const-decl "T" for_iterate nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(ForBody type-eq-decl nil for_iterate nil)
(subrange type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-type-decl nil for_iterate 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(iterate_left_def_TCC1 0
(iterate_left_def_TCC1-1 nil 3508252462 ("" (subtype-tcc) nil nil)
nil nil))
(iterate_left_def_TCC2 0
(iterate_left_def_TCC2-1 nil 3508252462 ("" (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)
(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)
(upfrom 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))
nil))
(iterate_left_def_TCC3 0
(iterate_left_def_TCC3-1 nil 3508252462 ("" (subtype-tcc) nil nil)
((int_minus_int_is_int application-judgement "int" integers nil))
nil))
(iterate_left_def_ext 0
(iterate_left_def_ext-1 nil 3508370001
("" (skosimp*)
((""
(case "FORALL(i:int,n:nat,f,g:[int->T],o:[[T,T]->T]) :
(FORALL (x:subrange(i,i+n)) : f(x) = g(x))
IMPLIES
iterate_left_def(i,i+n,f,o) = iterate_left_def(i,i+n,g,o)")
(("1" (inst -1 "i!1" "j!1-i!1" "f!1" "g!1" "oh!1")
(("1" (assert) nil nil)) nil)
("2" (hide-all-but 1)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "iterate_left_def" 1)
(("2" (inst -1 "i" "f" "g" "o")
(("2" (split -1)
(("1" (inst? -2) (("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (skeep) (("2" (inst? -1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((iterate_left_def def-decl "T" for_iterate nil)
(upfrom nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(subrange type-eq-decl nil 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)
(T formal-type-decl nil for_iterate 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)
(int_plus_int_is_int application-judgement "int" integers 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)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(ext2int_TCC2 0
(ext2int_TCC2-1 nil 3558204382 ("" (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)
(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))
nil))
(iterate_left_TCC1 0
(iterate_left_TCC1-1 nil 3508332707 ("" (subtype-tcc) nil nil) nil
nil))
(iterate_left_TCC2 0
(iterate_left_TCC2-1 nil 3508362054 ("" (subtype-tcc) nil nil) nil
nil))
(iterate_left_eq 0
(iterate_left_eq-1 nil 3508252515
(""
(case "FORALL (i:int, n: nat, f:IterateBody(i,i+n), o: [[T, T] -> T]):
iterate_left(i,i+n,f,o) =
iterate_left_def(i,i+n,ext2int(i,i+n,f(i),f),o)")
(("1" (skosimp)
(("1" (inst -1 "i!1" "j!1-i!1" "f!1" "oh!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skolem 1 "n")
(("2" (flatten)
(("2" (skeep)
(("2" (expand "iterate_left_def" 1)
(("2"
(inst -1 "i" "LAMBDA(k:subrange(i,i+n)):f(k)" "o")
(("2" (expand "ext2int" 1 2)
(("2" (lemma "iterate_left_def_ext")
(("2" (inst? -1)
(("2"
(inst -1 "ext2int(i, 1 + i + n, f(i), f)")
(("2" (split -1)
(("1" (replaces -1)
(("1"
(replaces -1 :dir rl)
(("1"
(expand "iterate_left")
(("1"
(rewrite "for_eq")
(("1"
(expand "for_def")
(("1"
(expand "ext2int" 1 1)
(("1"
(rewrite "for_eq")
(("1"
(lemma "for_def_ext")
(("1"
(inst?)
(("1"
(inst
-1
"ext2int(1 + i, i + n,
LAMBDA (k_1: subrange(1 + i, i + n), t: T):
t o f(k_1))")
(("1"
(split -1)
(("1"
(assert)
nil
nil)
("2"
(hide 2)
(("2"
(skeep)
(("2"
(expand
"ext2int")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(skeep)
(("2"
(expand "ext2int")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((iterate_left_def_ext formula-decl nil for_iterate nil)
(for_def def-decl "T" for_iterate 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)
(ForBody type-eq-decl nil for_iterate 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)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types 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)
(int_plus_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)
(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)
(subrange type-eq-decl nil integers nil)
(T formal-type-decl nil for_iterate nil)
(IterateBody type-eq-decl nil for_iterate nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upfrom nonempty-type-eq-decl nil integers nil)
(iterate_left const-decl "T" for_iterate nil)
(iterate_left_def def-decl "T" for_iterate nil)
(ext2int const-decl "T" for_iterate nil))
nil))
(iterate_left_induction_TCC1 0
(iterate_left_induction_TCC1-1 nil 3508459075
("" (subtype-tcc) nil nil) nil nil))
(iterate_left_induction_TCC2 0
(iterate_left_induction_TCC2-1 nil 3509182065
("" (subtype-tcc) nil nil) nil nil))
(iterate_left_induction_TCC3 0
(iterate_left_induction_TCC3-1 nil 3509182065
("" (subtype-tcc) nil nil) nil nil))
(iterate_left_induction_TCC4 0
(iterate_left_induction_TCC4-1 nil 3509182065
("" (subtype-tcc) nil nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(iterate_left_induction_TCC5 0
(iterate_left_induction_TCC5-1 nil 3509182065
("" (subtype-tcc) nil nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(iterate_left_induction 0
(iterate_left_induction-1 nil 3508459230
("" (skeep)
(("" (expand "iterate_left")
(("" (lemma "for_induction")
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (case-replace "max(0,n-m) = n-m")
(("1" (hide -1)
(("1" (hide-all-but (-2 1))
(("1" (skeep)
(("1" (inst? -2) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((iterate_left const-decl "T" for_iterate nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(upfrom nonempty-type-eq-decl nil integers nil)
(T formal-type-decl nil for_iterate nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(subrange type-eq-decl nil integers nil)
(IterateBody type-eq-decl nil for_iterate nil)
(ForBody type-eq-decl nil for_iterate nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(< const-decl "bool" reals nil)
(below 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_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(PRED type-eq-decl nil defined_types nil)
(for_induction formula-decl nil for_iterate nil))
shostak))
(iterate_right_def_TCC1 0
(iterate_right_def_TCC1-1 nil 3508253149 ("" (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)
(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)
(upfrom nonempty-type-eq-decl nil integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(iterate_right_def_TCC2 0
(iterate_right_def_TCC2-1 nil 3508253149 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(iterate_right_def_ext 0
(iterate_right_def_ext-1 nil 3508370279
("" (skosimp*)
((""
(case "FORALL(n:nat,j:int,f,g:[int->T],o:[[T,T]->T]) :
(FORALL (x:subrange(j-n,j)) : f(x) = g(x))
IMPLIES
--> --------------------
--> 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.
|
