|
(congruence
(IMP_admissible_TCC1 0
(IMP_admissible_TCC1-1 nil 3354849744
("" (inst + "I[Cont]")
(("" (lemma "identity_continuous") (("" (propax) nil nil)) nil))
nil)
((I const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(scott_continuous? const-decl "bool" scott_continuity "scott/")
(sq_le const-decl "bool" Cont nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Cont nonempty-type-eq-decl nil Cont nil)
(lift type-decl nil lift_adt nil)
(State nonempty-type-eq-decl nil State 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)
(V formal-nonempty-type-decl nil congruence nil)
(I_is_continuous name-judgement "continuous
[Cont, scott_open_sets[Cont, (sq_le)], Cont,
scott_open_sets[Cont, (sq_le)]]" congruence nil))
nil))
(P_bottom_TCC1 0
(P_bottom_TCC1-1 nil 3354849225
("" (expand "scott_continuous?")
((""
(case-replace "increasing?(LAMBDA c: LAMBDA s: bottom[State])")
(("1" (expand "lub_preserving?")
(("1" (skosimp*)
(("1" (expand "image")
(("1"
(case-replace
"{y: Cont | EXISTS (x: (D!1)): y = (LAMBDA s: bottom[State])} = singleton[Cont](LAMBDA s: bottom[State])")
(("1" (hide -1) (("1" (rewrite "lub_singleton") nil nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("2" (expand "singleton")
(("2"
(case-replace "x!1 = (LAMBDA s: bottom[State])")
(("1" (typepred "D!1")
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (skosimp)
(("1"
(expand "member")
(("1" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "increasing?")
(("2" (skosimp)
(("2" (expand "sq_le") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((sq_le_pdcpo name-judgement
"(pointed_directed_complete_partial_order?[Cont])" congruence nil)
(V formal-nonempty-type-decl nil congruence 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)
(State nonempty-type-eq-decl nil State nil)
(lift type-decl nil lift_adt nil)
(Cont nonempty-type-eq-decl nil Cont nil)
(bool nonempty-type-eq-decl nil booleans nil)
(sq_le const-decl "bool" Cont nil)
(increasing? const-decl "bool" fun_preds_partial "scott/")
(bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
(bottom adt-constructor-decl "(bottom?)" lift_adt nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[Cont[V]]" congruence nil)
(singleton_is_compact application-judgement
"compact[Cont[V], scott_open_sets]" congruence nil)
(directed_singleton application-judgement
"directed[Cont[V], (sq_le)]" congruence nil)
(lub_singleton formula-decl nil bounded_order_props "orders/")
(D!1 skolem-const-decl "directed[Cont[V], (sq_le)]" congruence nil)
(x!2 skolem-const-decl "Cont[V]" congruence nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(image const-decl "set[R]" function_image nil)
(lub_preserving? const-decl "bool" scott_continuity "scott/")
(scott_continuous? const-decl "bool" scott_continuity "scott/"))
nil))
(P_bottom 0
(P_bottom-1 nil 3354471613
("" (expand "P")
(("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("1" (expand "o") (("1" (propax) nil nil)) nil)
("2" (skosimp)
(("2" (expand "o") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((sq_le_pdcpo name-judgement
"(pointed_directed_complete_partial_order?[Cont])" congruence nil)
(bottom adt-constructor-decl "(bottom?)" lift_adt nil)
(c!1 skolem-const-decl "Cont[V]" congruence nil)
(Cont nonempty-type-eq-decl nil Cont nil)
(O const-decl "LiftPartialFunction[X, Z]"
PartialFunctionComposition nil)
(LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
nil)
(bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
(lift type-decl nil lift_adt nil)
(State nonempty-type-eq-decl nil State 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)
(V formal-nonempty-type-decl nil congruence nil)
(P const-decl "bool" congruence nil))
shostak))
(IMP_scott_continuity_TCC1 0
(IMP_scott_continuity_TCC1-1 nil 3355192008
("" (expand "directed_complete_partial_order?")
(("" (expand "partial_order?")
(("" (expand "preorder?")
(("" (expand "directed_complete?")
(("" (split)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil)
("4" (skosimp)
(("4" (typepred "D!1")
(("4" (expand "least_bounded_above?")
(("4" (case "D!1(FALSE)")
(("1" (inst + "FALSE")
(("1" (expand "least_upper_bound?")
(("1" (expand "upper_bound?")
(("1" (skosimp*)
(("1" (assert)
(("1" (inst - "FALSE") nil 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"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((partial_order? const-decl "bool" orders nil)
(directed_complete? const-decl "bool" directed_orders "orders/")
(least_bounded_above? const-decl "bool" bounded_orders "orders/")
(TRUE const-decl "bool" booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_orders "orders/")
(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/")
(antisymmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(partial_order_transitive formula-decl nil partial_order_props
"orders/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(WHEN const-decl "[bool, bool -> bool]" booleans nil)
(reflexive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/"))
nil))
(admissible_P 0
(admissible_P-1 nil 3355391729
("" (expand "admissible_pred?")
(("" (skosimp*)
(("" (typepred "sq_le")
((""
(lemma
"continuous_pointwise_preserves_pointed_directed_complete_partial_order"
("p1" "sq_le" "p2" "sq_le"))
((""
(lemma
"product_preserves_pointed_directed_complete_partial_order"
("r1" "(continuous_pointwise(sq_le,sq_le))" "r2" "sq_le"))
(("" (case-replace "nonempty?(D!1)")
(("1" (split -5)
(("1" (expand "nonempty?") (("1" (propax) nil nil))
nil)
("2"
(lemma
"product_lub[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),(Cont)]"
("r1" "(continuous_pointwise(sq_le, sq_le))" "r2"
"sq_le" "D" "D!1"))
(("1" (rewrite "lub_rew" 1)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(case "nonempty?({x: ((scott_continuous?[Cont, Cont, (sq_le), (sq_le)])) |
EXISTS (z: (D!1)): z`1 = x})")
(("1"
(case "directed?(continuous_pointwise(sq_le, sq_le))({x: ((scott_continuous?[Cont, Cont, (sq_le), (sq_le)])) |
EXISTS (z: (D!1)): z`1 = x})")
(("1"
(name-replace "D1"
"{x: ((scott_continuous?[Cont, Cont, (sq_le), (sq_le)])) |
EXISTS (z: (D!1)): z`1 = x}")
(("1"
(case
"nonempty?({y: Cont | EXISTS (z: (D!1)): z`2 = y})")
(("1"
(case
"directed?(sq_le)({y: Cont | EXISTS (z: (D!1)): z`2 = y})")
(("1"
(name-replace
"D2"
"{y: Cont | EXISTS (z: (D!1)): z`2 = y}")
(("1"
(typepred "lub(sq_le)(D2)")
(("1"
(typepred
"lub((continuous_pointwise(sq_le, sq_le)))(D1)")
(("1"
(name-replace
"PHI"
"lub((continuous_pointwise(sq_le, sq_le)))(D1)")
(("1"
(name-replace
"PSI"
"lub(sq_le)(D2)")
(("1"
(expand
"least_upper_bound?")
(("1"
(expand "upper_bound?")
(("1"
(flatten)
(("1"
(expand "P")
(("1"
(skosimp)
(("1"
(inst
-3
"lambda c: c o PSI")
(("1"
(split -3)
(("1"
(expand
"continuous_pointwise"
-1)
(("1"
(expand
"pointwise")
(("1"
(inst
-
"c!1")
(("1"
(case
"sq_le(c!1 o PSI,PHI(c!1))")
(("1"
(expand
"pointed_directed_complete_partial_order?"
-15)
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(expand
"partial_order?")
(("1"
(flatten)
(("1"
(expand
"antisymmetric?")
(("1"
(inst
-16
"PHI(c!1)"
"c!1 o PSI")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(expand
"sq_le"
1)
(("2"
(skosimp)
(("2"
(expand
"o"
-1)
(("2"
(lift-if
-1)
(("2"
(assert)
(("2"
(case-replace
"bottom?(PSI(s1!1))")
(("2"
(assert)
(("2"
(case
"FORALL (s:State,r1,r2:(D2)): (NOT bottom?(r1(s)) & NOT bottom?(r2(s))) => r1(s) = r2(s)")
(("1"
(case
"forall(r:(D2)):r(s1!1)=bottom[State]")
(("1"
(inst
-8
"lambda s: if s = s1!1 then bottom[State] else PSI(s) endif")
(("1"
(split
-8)
(("1"
(expand
"sq_le"
-1)
(("1"
(inst
-
"s1!1"
"_")
(("1"
(assert)
(("1"
(inst
-
"down(PSI(s1!1))")
(("1"
(rewrite
"up_down")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"sq_le"
1)
(("2"
(skosimp)
(("2"
(case-replace
"s1!2=s1!1")
(("1"
(inst
-4
"r!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(inst
-9
"r!1")
(("2"
(expand
"sq_le"
-9)
(("2"
(inst
-9
"s1!2"
"s2!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst
-7
"lambda s: if s = s1!1 then r!1(s) else PSI(s) endif")
(("2"
(split
-7)
(("1"
(expand
"sq_le"
-1)
(("1"
(inst
-
"s1!1"
"down(PSI(s1!1))")
(("1"
(rewrite
"up_down")
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1)
(("1"
(typepred
"r!1")
(("1"
(expand
"D2"
-1)
(("1"
(skosimp)
(("1"
(typepred
"z!1")
(("1"
(inst
-18
"z!1")
(("1"
(replace
-2)
(("1"
(inst
-18
"c!1")
(("1"
(inst
-7
"z!1`1")
(("1"
(expand
"continuous_pointwise"
-7)
(("1"
(expand
"pointwise"
-7)
(("1"
(inst
-7
"c!1")
(("1"
(replace
-18)
(("1"
(expand
"sq_le"
-7)
(("1"
(inst
-7
"s1!1"
"s2!1")
(("1"
(assert)
(("1"
(expand
"o ")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"D1")
(("2"
(inst
+
"z!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"sq_le"
1)
(("2"
(skosimp)
(("2"
(case-replace
"s1!2=s1!1")
(("1"
(inst
-3
"s1!1"
"r!1"
"r!2")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(inst
-7
"r!2")
(("2"
(expand
"sq_le"
-7)
(("2"
(inst
-7
"s1!2"
"s2!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred
"r1!1")
(("2"
(typepred
"r2!1")
(("2"
(expand
"directed?"
-9)
(("2"
(inst
-9
"r1!1"
"r2!1")
(("2"
(replace
-1)
(("2"
(replace
-2)
(("2"
(skolem!
-9)
(("2"
(typepred
"z!1")
(("2"
(flatten
-10)
(("2"
(expand
"sq_le"
(-10
-11))
(("2"
(inst
-10
"s!1"
"_")
(("2"
(inst
-11
"s!1"
"_")
(("2"
(inst
-10
"down(r1!1(s!1))")
(("1"
(inst
-11
"down(r2!1(s!1))")
(("1"
(rewrite
"up_down")
(("1"
(rewrite
"up_down")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
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)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"D1")
(("2"
(skosimp)
(("2"
(expand
"continuous_pointwise")
(("2"
(expand
"pointwise")
(("2"
(skosimp)
(("2"
(inst
-16
"z!1")
(("2"
(inst
-16
"x!1")
(("2"
(replace
-2)
(("2"
(replace
-16)
(("2"
(inst
-5
"z!1`2")
(("1"
(expand
"sq_le")
(("1"
(skosimp)
(("1"
(expand
"o ")
(("1"
(lift-if)
(("1"
(case
"bottom?(z!1`2(s1!1))")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.59 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
