|
(continuation
(IMP_fixpoints_TCC1 0
(IMP_fixpoints_TCC1-1 nil 3353544462
("" (inst + "I[Cont]")
(("" (assert)
(("" (expand "scott_continuous?")
(("" (split)
(("1" (expand "increasing?")
(("1" (skosimp)
(("1" (expand "I") (("1" (propax) nil nil)) nil)) nil))
nil)
("2" (expand "lub_preserving?")
(("2" (skosimp*)
(("2" (expand "I")
(("2" (expand "image")
(("2"
(case-replace
"{y: Cont | EXISTS (x_1: (D!1)): y = x_1} = D!1")
(("2" (apply-extensionality 1 :hide? t)
(("2" (case-replace "D!1(x!1)")
(("1" (inst + "x!1") nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((I const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(scott_continuous type-eq-decl nil scott_continuity "scott/")
(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 continuation nil)
(I_is_continuous name-judgement "continuous
[Cont, scott_open_sets[Cont, (sq_le)], Cont,
scott_open_sets[Cont, (sq_le)]]" continuation nil))
nil))
(identity_continuous 0
(identity_continuous-1 nil 3353548340
("" (expand "I")
(("" (expand "scott_continuous?")
(("" (split)
(("1" (expand "increasing?") (("1" (skosimp) nil nil)) nil)
("2" (expand "lub_preserving?")
(("2" (skosimp)
(("2" (typepred "D!1")
(("2" (expand "image")
(("2"
(case-replace
"{y: Cont | EXISTS (x_1: (D!1)): y = x_1}=D!1")
(("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("2" (case-replace "D!1(x!1)")
(("1" (inst + "x!1") nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((scott_continuous? const-decl "bool" scott_continuity "scott/")
(lub_preserving? const-decl "bool" scott_continuity "scott/")
(directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(sq_le const-decl "bool" Cont nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets 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)
(number nonempty-type-decl nil numbers nil)
(V formal-nonempty-type-decl nil continuation nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(D!1 skolem-const-decl "directed[Cont[V], (sq_le)]" continuation
nil)
(x!1 skolem-const-decl "[[V -> int] -> lift[State[V]]]"
continuation nil)
(image const-decl "set[R]" function_image nil)
(increasing? const-decl "bool" fun_preds_partial "scott/")
(I const-decl "(bijective?[T, T])" identity nil))
shostak))
(composition_continuous 0
(composition_continuous-1 nil 3353645372
("" (skosimp)
(("" (typepred "f!1")
(("" (typepred "g!1")
(("" (expand "scott_continuous?")
(("" (flatten)
(("" (expand "o ")
(("" (split)
(("1" (expand "increasing?")
(("1" (skosimp)
(("1" (inst - "x!1" "y!1")
(("1" (assert)
(("1" (inst - "g!1(x!1)" "g!1(y!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "lub_preserving?")
(("2" (skosimp)
(("2" (typepred "D!1")
(("2" (inst - "D!1")
(("2"
(lemma "lub_set_image" ("g" "g!1" "D" "D!1"))
(("1" (assert)
(("1" (replace -6)
(("1"
(inst - "image(g!1,D!1)")
(("1"
(split -8)
(("1"
(replace -1)
(("1"
(case-replace
"image(LAMBDA (x: Cont): f!1(g!1(x)), D!1) = image(f!1, image(g!1, D!1))")
(("1"
(hide-all-but 1)
(("1"
(expand "image")
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(case-replace
"(EXISTS (x_1: (D!1)): x!1 = f!1(g!1(x_1)))")
(("1"
(skosimp)
(("1"
(inst + "g!1(x!2)")
(("1"
(inst + "x!2")
nil
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!2")
(("2"
(skosimp)
(("2"
(replace -1)
(("2"
(replace
-2)
(("2"
(hide-all-but
1)
(("2"
(inst
+
"x!3")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"image(LAMBDA (x: Cont): f!1(g!1(x)), D!1) = image(f!1, image(g!1, D!1))")
(("2"
(hide-all-but 1)
(("2"
(expand "image")
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(case-replace
"(EXISTS (x_1: (D!1)): x!1 = f!1(g!1(x_1)))")
(("1"
(skosimp)
(("1"
(inst + "g!1(x!2)")
(("1"
(inst + "x!2")
nil
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!2")
(("2"
(skosimp)
(("2"
(inst + "x!3")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"directed_image"
("g" "g!1" "D" "D!1"))
(("2"
(assert)
(("2"
(hide-all-but (-3 1))
(("2"
(expand "image")
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(skosimp*)
(("2"
(inst - "g!1(x!1)")
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((scott_continuous type-eq-decl nil scott_continuity "scott/")
(scott_continuous? const-decl "bool" scott_continuity "scott/")
(sq_le const-decl "bool" Cont 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)
(number nonempty-type-decl nil numbers nil)
(V formal-nonempty-type-decl nil continuation nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(composition_is_continuous application-judgement "continuous
[Cont, scott_open_sets[Cont, (sq_le)], Cont,
scott_open_sets[Cont, (sq_le)]]" continuation nil)
(O const-decl "T3" function_props nil)
(lub_preserving? const-decl "bool" scott_continuity "scott/")
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(directed? const-decl "bool" directed_order_props "orders/")
(directed type-eq-decl nil directed_order_props "orders/")
(lub_set_image formula-decl nil scott_continuity "scott/")
(directed_image formula-decl nil scott_continuity "scott/")
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "Cont[V]" continuation nil)
(empty? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(x!2 skolem-const-decl "(D!1)" continuation nil)
(x!2 skolem-const-decl "(D!1)" continuation nil)
(D!1 skolem-const-decl "directed[Cont, (sq_le)]" continuation nil)
(g!1 skolem-const-decl
"scott_continuous[Cont, Cont, (sq_le), (sq_le)]" continuation nil)
(image const-decl "set[R]" function_image nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(increasing? const-decl "bool" fun_preds_partial "scott/")
(sq_le_pdcpo name-judgement
"(pointed_directed_complete_partial_order?[Cont])" continuation
nil))
shostak))
(assign_continuous 0
(assign_continuous-1 nil 3354465346
("" (skosimp)
(("" (expand "assign")
(("" (expand "assign")
(("" (lemma "Cont.apply_continuous")
((""
(inst -
"(LAMBDA s: up(lambda (y:V): IF y = x!1 THEN A(a!1)(s) ELSE s(y) ENDIF))")
(("" (expand "o") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((assign const-decl "State" State nil)
(V formal-nonempty-type-decl nil continuation nil)
(apply_continuous formula-decl nil Cont nil)
(O const-decl "LiftPartialFunction[X, Z]"
PartialFunctionComposition nil)
(A def-decl "[State -> int]" AExp nil)
(AExp type-decl nil AExp nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
(up? adt-recognizer-decl "[lift -> boolean]" lift_adt 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)
(assign const-decl "State" State nil))
shostak))
(conditional_continuous 0
(conditional_continuous-1 nil 3354078097
("" (skosimp)
(("" (typepred "f!1")
(("" (typepred "g!1")
(("" (expand "scott_continuous?")
((""
(case-replace
"increasing?(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)))")
(("1" (flatten)
(("1" (expand "lub_preserving?")
(("1" (skosimp)
(("1" (typepred "D!1")
(("1" (inst - "D!1")
(("1" (inst - "D!1")
(("1"
(lemma "lub_set_image" ("g" "f!1" "D" "D!1"))
(("1"
(lemma "lub_set_image"
("g" "g!1" "D" "D!1"))
(("1" (assert)
(("1"
(typepred "lub(image(f!1, D!1))")
(("1"
(typepred "lub(image(g!1, D!1))")
(("1"
(typepred
"lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)), D!1))")
(("1"
(expand "least_upper_bound?")
(("1"
(flatten)
(("1"
(replace -13)
(("1"
(replace -15)
(("1"
(inst
-2
"conditional(B(b!1), lub(image(f!1, D!1)), lub(image(g!1, D!1)))")
(("1"
(split -2)
(("1"
(hide -2)
(("1"
(case
"(sq_le)(conditional(B(b!1), lub(image(f!1, D!1)),
lub(image(g!1, D!1))),lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)),
D!1)))")
(("1"
(typepred
"sq_le")
(("1"
(expand
"pointed_directed_complete_partial_order?")
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(expand
"partial_order?")
(("1"
(flatten)
(("1"
(expand
"antisymmetric?")
(("1"
(inst
-
"conditional(B(b!1), lub(image(f!1, D!1)), lub(image(g!1, D!1)))"
"lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)), D!1))")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(typepred
"lub(image(LAMBDA c: conditional(B(b!1),f!1(c),g!1(c)),D!1))")
(("2"
(name-replace
"LUB_C"
"lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)),
D!1))")
(("2"
(expand
"least_upper_bound?")
(("2"
(flatten)
(("2"
(expand
"upper_bound?"
-1)
(("2"
(replace
-14
1
rl)
(("2"
(replace
-16
1
rl)
(("2"
(replace
-16
-7
rl)
(("2"
(replace
-14
-5
rl)
(("2"
(inst
-5
"conditional(B(b!1), g!1(lub(D!1)), LUB_C)")
(("2"
(split
-5)
(("1"
(inst
-7
"conditional(B(b!1), LUB_C, f!1(lub(D!1)))")
(("1"
(split
-7)
(("1"
(hide-all-but
(-1
-2
1))
(("1"
(expand
"sq_le")
(("1"
(expand
"conditional")
(("1"
(skosimp*)
(("1"
(inst
-
"s1!1"
"s2!1")
(("1"
(inst
-
"s1!1"
"s2!1")
(("1"
(case-replace
"B(b!1)(s1!1)")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(expand
"upper_bound?")
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"image"
-1)
(("2"
(skosimp)
(("2"
(replace
-1)
(("2"
(typepred
"x!1")
(("2"
(hide
-2
-3)
(("2"
(typepred
"lub(D!1)")
(("2"
(expand
"least_upper_bound?")
(("2"
(flatten)
(("2"
(expand
"upper_bound?"
-1)
(("2"
(inst
-
"x!1")
(("2"
(expand
"increasing?")
(("2"
(inst
-14
"x!1"
"lub(D!1)")
(("2"
(inst
-16
"x!1"
"lub(D!1)")
(("2"
(assert)
(("2"
(inst
-4
"conditional(B(b!1), f!1(x!1), g!1(x!1))")
(("1"
(expand
"sq_le")
(("1"
(skosimp)
(("1"
(expand
"conditional")
(("1"
(case-replace
"B(b!1)(s1!1)")
(("1"
(inst
-6
"s1!1"
"s2!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(inst
-17
"s1!1"
"s2!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"image")
(("2"
(inst
+
"x!1")
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"
(expand
"upper_bound?"
1)
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"image"
-1)
(("2"
(skosimp)
(("2"
(typepred
"x!1")
(("2"
(replace
-2)
(("2"
(rewrite
"sq_le"
1)
(("2"
(skosimp)
(("2"
(expand
"conditional"
1)
(("2"
(case-replace
"B(b!1)(s1!1)")
(("1"
(typepred
"lub(D!1)")
(("1"
(expand
"least_upper_bound?")
(("1"
(flatten)
(("1"
(expand
"upper_bound?"
-1)
(("1"
(inst
-
"x!1")
(("1"
(expand
"increasing?"
-18)
(("1"
(inst
-18
"x!1"
"lub(D!1)")
(("1"
(assert)
(("1"
(expand
"sq_le"
-18)
(("1"
(inst
-18
"s1!1"
"s2!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst
-4
"conditional(B(b!1), f!1(x!1), g!1(x!1))")
(("1"
(expand
"sq_le"
-4)
(("1"
(inst
-
"s1!1"
"s2!1")
(("1"
(expand
"conditional"
-4)
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"image")
(("2"
(inst
+
"x!1")
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)
("2"
(hide 2)
(("2"
(expand
"upper_bound?")
(("2"
(skosimp)
(("2"
(typepred
"r!1")
(("2"
(expand
"image"
-1)
(("2"
(skosimp)
(("2"
(typepred
"x!1")
(("2"
(replace
-2)
(("2"
(hide
-2)
(("2"
(expand
"sq_le"
1)
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.136 Sekunden
in einem neuen Tab ansehen
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
