|
(dual_fixpoints
(IMP_scott_continuity_TCC1 0
(IMP_scott_continuity_TCC1-1 nil 3353386539
("" (expand "directed_complete_partial_order?")
(("" (split)
(("1" (grind) nil nil)
("2" (expand "directed_complete?")
(("2" (skosimp)
(("2" (typepred "D!1")
(("2" (expand "least_bounded_above?")
(("2" (case "D!1(FALSE)")
(("1" (inst + "FALSE")
(("1" (expand "least_upper_bound?")
(("1" (expand "upper_bound?")
(("1" (skosimp) (("1" (inst - "FALSE") nil nil))
nil))
nil))
nil))
nil)
("2" (inst + "TRUE")
(("2" (expand "least_upper_bound?")
(("2" (expand "upper_bound?")
(("2" (skosimp)
(("2" (typepred "r!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((reflexive? const-decl "bool" relations nil)
(WHEN const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(partial_order_transitive formula-decl nil partial_order_props
"orders/")
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(least_bounded_above? const-decl "bool" bounded_orders "orders/")
(TRUE const-decl "bool" booleans nil)
(upper_bound? const-decl "bool" bounded_orders "orders/")
(D!1 skolem-const-decl "(directed?(WHEN))" dual_fixpoints nil)
(least_upper_bound? const-decl "bool" bounded_orders "orders/")
(FALSE const-decl "bool" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(pred type-eq-decl nil defined_types nil)
(directed? const-decl "bool" directed_orders "orders/")
(directed_complete? const-decl "bool" directed_orders "orders/")
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/"))
nil))
(dual_fixpoint_induction 0
(dual_fixpoint_induction-1 nil 3353386540
("" (skosimp)
(("" (lemma "fixpoint_induction[[T1,T2],(le1*le2)]" ("p" "p!1"))
(("" (typepred "phi!1")
(("" (typepred "psi!1")
((""
(name "PHI" "LAMBDA (z:[T1,T2]): (phi!1(z`1),psi!1(z`2))")
(("" (case "increasing?(PHI)")
(("1" (inst - "PHI")
(("1" (split -5)
(("1" (hide -3 -6)
(("1" (lemma "fix_approx_nonempty" ("phi" "psi!1"))
(("1"
(lemma "fix_approx_nonempty" ("phi" "phi!1"))
(("1"
(lemma "fix_approx_nonempty" ("phi" "PHI"))
(("1"
(lemma "fix_approx_chain" ("phi" "psi!1"))
(("1"
(lemma "fix_approx_chain"
("phi" "phi!1"))
(("1"
(lemma
"fix_approx_chain"
("phi" "PHI"))
(("1"
(lemma
"ne_chain_is_directed"
("X" "FIX_APPROX(psi!1)"))
(("1"
(lemma
"ne_chain_is_directed"
("X" "FIX_APPROX(phi!1)"))
(("1"
(lemma
"ne_chain_is_directed"
("X" "FIX_APPROX(PHI)"))
(("1"
(assert)
(("1"
(expand "fix")
(("1"
(lemma
"product_lub"
("r1"
"le1"
"r2"
"le2"
"D"
"FIX_APPROX(PHI)"))
(("1"
(case-replace
"{x: T1 | EXISTS (z: (FIX_APPROX(PHI))): z`1 = x} = FIX_APPROX(phi!1)")
(("1"
(case-replace
"{y: T2 | EXISTS (z: (FIX_APPROX(PHI))): z`2 = y} = FIX_APPROX(psi!1)")
(("1"
(hide -1 -2)
(("1"
(rewrite
"lub_rew"
1)
(("1"
(rewrite
"lub_rew"
1)
(("1"
(rewrite
"lub_rew"
-11)
(("1"
(replace -1)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(hide -1)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(case
"forall (n:nat): power(PHI,n)(bottom)`2 = power(psi!1,n)(bottom)")
(("1"
(case-replace
"FIX_APPROX(psi!1)(x!1)")
(("1"
(expand
"FIX_APPROX")
(("1"
(expand
"image")
(("1"
(skosimp)
(("1"
(replace
-1
1)
(("1"
(inst
-2
"x!2")
(("1"
(replace
-2
1
rl)
(("1"
(inst
+
"power(PHI, x!2)(bottom)")
(("1"
(expand
"FIX_APPROX")
(("1"
(expand
"image")
(("1"
(inst
+
"x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred
"z!1")
(("2"
(expand
"FIX_APPROX")
(("2"
(expand
"image")
(("2"
(skosimp)
(("2"
(inst
+
"x!2")
(("2"
(inst
-2
"x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(induct
"n")
(("1"
(expand
"power")
(("1"
(lemma
"fixpoints[T2,le2].bottom_le"
("x"
"bottom`2"))
(("1"
(lemma
"bottom_le[[T1,T2],(le1*le2)]")
(("1"
(expand
"*")
(("1"
(inst
-
"(bottom,bottom)")
(("1"
(flatten)
(("1"
(typepred
"le2")
(("1"
(expand
"pointed_directed_complete_partial_order?")
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(expand
"partial_order?")
(("1"
(flatten)
(("1"
(expand
"antisymmetric?")
(("1"
(inst
-
"bottom`2"
"bottom")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"power"
1)
(("2"
(expand
"o")
(("2"
(replace
-1
1
rl)
(("2"
(hide
-1)
(("2"
(expand
"PHI"
1
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(case
"forall (n:nat): power(PHI,n)(bottom)`1 = power(phi!1,n)(bottom)")
(("1"
(case-replace
"FIX_APPROX(phi!1)(x!1)")
(("1"
(expand
"FIX_APPROX")
(("1"
(expand
"image")
(("1"
(skosimp)
(("1"
(replace
-1
1)
(("1"
(inst
-2
"x!2")
(("1"
(replace
-2
1
rl)
(("1"
(inst
+
"power(PHI, x!2)(bottom)")
(("1"
(expand
"FIX_APPROX")
(("1"
(expand
"image")
(("1"
(inst
+
"x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred
"z!1")
(("2"
(expand
"FIX_APPROX")
(("2"
(expand
"image")
(("2"
(skosimp)
(("2"
(replace
-3
1
rl)
(("2"
(replace
-1
1)
(("2"
(hide-all-but
(-2
1))
(("2"
(inst
+
"x!2")
(("2"
(inst
-
"x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand
"power")
(("1"
(lemma
"fixpoints[T1,le1].bottom_le"
("x"
"bottom`1"))
(("1"
(lemma
"fixpoints[[T1,T2],(le1*le2)].bottom_le")
(("1"
(inst
-
"(bottom,bottom)")
(("1"
(expand
"*")
(("1"
(flatten)
(("1"
(hide
-2)
(("1"
(typepred
"le1")
(("1"
(expand
"pointed_directed_complete_partial_order?")
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(expand
"partial_order?")
(("1"
(flatten)
(("1"
(expand
"antisymmetric?")
(("1"
(inst
-
"bottom`1"
"bottom")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"power"
1)
(("2"
(expand
"o")
(("2"
(replace
-1
1
rl)
(("2"
(hide
-1)
(("2"
(expand
"PHI"
1
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "le2")
(("2"
(expand
"pointed_directed_complete_partial_order?")
(("2"
(flatten)
nil
nil))
nil))
nil)
("3"
(typepred "le1")
(("3"
(expand
"pointed_directed_complete_partial_order?")
(("3"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst - "x!1`1" "x!1`2")
(("2" (expand "PHI") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 -3 1))
(("2" (expand "increasing?")
(("2" (skosimp)
(("2" (expand "*")
(("2" (flatten)
(("2" (expand "PHI")
(("2" (inst - "x!1`2" "y!1`2")
(("2" (inst - "x!1`1" "y!1`1")
(("2"
(assert)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert)
(("3"
(lemma "product_preserves_partial_order"
("r1" "le1" "r2" "le2"))
(("1" (propax) nil nil)
("2" (typepred "le2")
(("2"
(expand "pointed_directed_complete_partial_order?")
(("2" (expand "directed_complete_partial_order?")
(("2" (flatten) nil nil)) nil))
nil))
nil)
("3" (typepred "le1")
(("3"
(expand "pointed_directed_complete_partial_order?")
(("3" (expand "directed_complete_partial_order?")
(("3" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((le2 formal-const-decl
"(pointed_directed_complete_partial_order?[T2])" dual_fixpoints
nil)
(le1 formal-const-decl
"(pointed_directed_complete_partial_order?[T1])" dual_fixpoints
nil)
(pointed_directed_complete_partial_order? const-decl "bool"
directed_orders "orders/")
(* const-decl "bool" product_orders "orders/")
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-nonempty-type-decl nil dual_fixpoints nil)
(T1 formal-nonempty-type-decl nil dual_fixpoints nil)
(admissible_pred nonempty-type-eq-decl nil admissible nil)
(admissible_pred? const-decl "bool" admissible nil)
(fixpoint_induction formula-decl nil admissible nil)
(product_preserves_reflexive application-judgement
"(reflexive?[[T1, T2]])" dual_fixpoints nil)
(product_preserves_transitive application-judgement
"(transitive?[[T1, T2]])" dual_fixpoints nil)
(product_preserves_preorder application-judgement
"(preorder?[[T1, T2]])" dual_fixpoints nil)
(product_preserves_antisymmetric application-judgement
"(antisymmetric?[[T1, T2]])" dual_fixpoints nil)
(product_preserves_partial_order application-judgement
"(partial_order?[[T1, T2]])" dual_fixpoints nil)
(product_preserves_directed_complete_partial_order
application-judgement
"(directed_complete_partial_order?[[T1, T2]])" dual_fixpoints nil)
(product_preserves_pointed_directed_complete_partial_order
application-judgement
"(pointed_directed_complete_partial_order?[[T1, T2]])"
dual_fixpoints nil)
(fix_approx_nonempty formula-decl nil fixpoints nil)
(ne_chain_is_directed formula-decl nil fixpoints nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(FIX_APPROX const-decl "set[T]" fixpoints nil)
(fix const-decl "T" fixpoints nil)
(fullset_is_clopen name-judgement "clopen[T, scott_open_sets]"
dual_fixpoints nil)
(partial_order_antisymmetric formula-decl nil partial_order_props
"orders/")
(antisymmetric? const-decl "bool" relations nil)
(bottom_le formula-decl nil fixpoints nil)
(nat_induction formula-decl nil naturalnumbers nil)
(image const-decl "set[R]" function_image nil)
(x!2 skolem-const-decl "(fullset[nat])" dual_fixpoints nil)
(bottom const-decl "(LAMBDA (t: T): least?(t, fullset[T], <=))"
fixpoints nil)
(fullset const-decl "set" sets nil)
(least? const-decl "bool" minmax_orders "orders/")
(power def-decl "T" monoid_def "algebra/")
(O const-decl "T3" function_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(lub_rew formula-decl nil bounded_order_props "orders/")
(lub_set? const-decl "bool" bounded_order_props "orders/")
(fullset_is_clopen name-judgement "clopen[T, scott_open_sets]"
dual_fixpoints nil)
(x!2 skolem-const-decl "(fullset[nat])" dual_fixpoints nil)
(directed? const-decl "bool" directed_orders "orders/")
(partial_order? const-decl "bool" orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(product_lub formula-decl nil product_orders "orders/")
(fix_approx_chain formula-decl nil fixpoints nil)
(PHI skolem-const-decl "[[T1, T2] -> [T1, T2]]" dual_fixpoints nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(increasing? const-decl "bool" fun_preds_partial nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak)))
¤ Dauer der Verarbeitung: 0.26 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.
|
