-
Notifications
You must be signed in to change notification settings - Fork 50
/
Copy pathmixed_sigmas.prf
13 lines (13 loc) · 11.2 KB
/
mixed_sigmas.prf
1
2
3
4
5
6
7
8
9
10
11
12
13
(mixed_sigmas (IMP_sigma_TCC1 0 (IMP_sigma_TCC1-1 nil 3537537618 ("" (lemma "connected_domain1") (("" (propax) nil nil)) nil) ((connected_domain1 formula-decl nil mixed_sigmas nil)) nil (IMP_sigma assuming "sigma[T].sigma" "connected_domain: ASSUMPTION (FORALL (x, y: sigma.T), (z: integers.integer): booleans.IMPLIES(booleans.AND(reals.<=(x, z), reals.<=(z, y)), sigma.T_pred(z)))"))) (IMP_sigma_TCC2 0 (IMP_sigma_TCC2-1 nil 3537537618 ("" (lemma "connected_domain2") (("" (propax) nil nil)) nil) ((connected_domain2 formula-decl nil mixed_sigmas nil)) nil (IMP_sigma assuming "sigma[H].sigma" "connected_domain: ASSUMPTION (FORALL (x, y: sigma.T), (z: integers.integer): booleans.IMPLIES(booleans.AND(reals.<=(x, z), reals.<=(z, y)), sigma.T_pred(z)))"))) (mixed_sigmas_const_eq_TCC1 0 (mixed_sigmas_const_eq_TCC1-1 nil 3537536439 ("" (skeep) (("" (lemma "T_pred_lem[T]") (("" (inst - thigh tlow _) (("" (skeep) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil mixed_sigmas nil) (T_pred const-decl "[int -> boolean]" mixed_sigmas 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) (T_pred_lem formula-decl nil sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil)) nil (mixed_sigmas_const_eq subtype "(number_fields.+)(mixed_sigmas.tlow, mixed_sigmas.i)" "T"))) (mixed_sigmas_const_eq_TCC2 0 (mixed_sigmas_const_eq_TCC2-1 nil 3537536439 ("" (skeep) (("" (skeep) (("" (lemma "T_pred_lem[H]") (("" (inst - "hhigh" "hlow" _) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (T_pred_lem formula-decl nil sigma 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) (H_pred const-decl "[int -> boolean]" mixed_sigmas nil) (H formal-subtype-decl nil mixed_sigmas nil)) nil (mixed_sigmas_const_eq subtype "(number_fields.+)(mixed_sigmas.hlow, mixed_sigmas.i)" "H"))) (mixed_sigmas_const_eq 0 (mixed_sigmas_const_eq-2 "" 3803788400 ("" (case "FORALL (F: [T -> real], G: [H -> real], hhigh: T_high[H],
hlow: T_low[H], thigh: T_high[T], tlow: T_low[T]):
(thigh - tlow = hhigh - hlow AND
(FORALL (i: nat):
i <= thigh - tlow IMPLIES F(tlow + i) = G(hlow + i)))
IMPLIES (FORALL (i: nat):
i <= thigh - tlow IMPLIES sigma[T](tlow, tlow+i, F) = sigma[H](hlow, hlow+i, G))") (("1" (skeep) (("1" (inst - "F" "G" "hhigh" "hlow" "thigh" "tlow") (("1" (assert) (("1" (replace -3) (("1" (inst - "thigh-tlow") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "sigma" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (induct "i") (("1" (assert) (("1" (flatten) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "sigma" +) (("2" (inst - "1+j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lemma "T_pred_lem[H]") (("3" (inst - "hhigh" "hlow" "i+hlow") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skeep) (("4" (lemma "T_pred_lem[T]") (("4" (inst - "thigh" "tlow" "i+tlow") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (skeep) (("3" (lemma "T_pred_lem[H]") (("3" (inst - "hhigh" "hlow" "hlow + i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skeep) (("4" (lemma "T_pred_lem[T]") (("4" (inst - "thigh" "tlow" "i+tlow") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skeep) (("5" (skeep) (("5" (lemma "T_pred_lem[H]") (("5" (inst - "hhigh" "hlow" "hlow + i") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skeep) (("6" (skeep) (("6" (lemma "T_pred_lem[T]") (("6" (inst - "thigh" "tlow" "i+tlow") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (mixed_sigmas_const_eq-1 nil 3537536793 ("" (case "FORALL (F: [T -> real], G: [H -> real], hhigh: T_high[H],
hlow: T_low[H], thigh: T_high[T], tlow: T_low[T]):
(thigh - tlow = hhigh - hlow AND
(FORALL (i: nat):
i <= thigh - tlow IMPLIES F(tlow + i) = G(hlow + i)))
IMPLIES (FORALL (i: nat):
i <= thigh - tlow IMPLIES sigma[T](tlow, tlow+i, F) = sigma[H](hlow, hlow+i, G))") (("1" (skeep) (("1" (inst - "F" "G" "hhigh" "hlow" "thigh" "tlow") (("1" (assert) (("1" (replace -3) (("1" (inst - "thigh-tlow") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "sigma" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (induct "i") (("1" (assert) (("1" (flatten) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "sigma" +) (("2" (inst - "1+j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (lemma "T_pred_lem[H]") (("3" (inst - "hhigh" "hlow" "i+hlow") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skeep) (("4" (lemma "T_pred_lem[T]") (("4" (inst - "thigh" "tlow" "i+tlow") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (skeep) (("3" (lemma "T_pred_lem[H]") (("3" (inst - "hhigh" "hlow" "hlow + i1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skeep) (("4" (lemma "T_pred_lem[T]") (("4" (inst - "thigh" "tlow" "i1+tlow") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skeep) (("5" (skeep) (("5" (lemma "T_pred_lem[H]") (("5" (inst - "hhigh" "hlow" "hlow + i") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skeep) (("6" (skeep) (("6" (lemma "T_pred_lem[T]") (("6" (inst - "thigh" "tlow" "i+tlow") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((thigh skolem-const-decl "T_high[T]" mixed_sigmas nil) (tlow skolem-const-decl "T_low[T]" mixed_sigmas nil) (hlow skolem-const-decl "T_low[H]" mixed_sigmas nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (T_pred_lem formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (thigh skolem-const-decl "T_high[T]" mixed_sigmas nil) (tlow skolem-const-decl "T_low[T]" mixed_sigmas nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers 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) (T_pred const-decl "[int -> boolean]" mixed_sigmas nil) (T formal-subtype-decl nil mixed_sigmas nil) (H_pred const-decl "[int -> boolean]" mixed_sigmas nil) (H formal-subtype-decl nil mixed_sigmas nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma nil)) shostak)) (mixed_sigmas_eq 0 (mixed_sigmas_eq-1 nil 3537537619 ("" (lemma "mixed_sigmas_const_eq") (("" (inst - _ _ _ _ _ _ 1) (("" (assert) (("" (case "FORALL (aa:real): 1*aa = aa") (("1" (rewrite -1) (("1" (rewrite -1) nil nil)) nil) ("2" (hide-all-but 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (mixed_sigmas_const_eq formula-decl nil mixed_sigmas nil)) shostak)))