Quelle continuation.prf
Sprache: Lisp
(continuationnil 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" "{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 )"(bijective?[T, T])" identity nil )"bool" functions nil )nil scott_continuity "scott/" )"bool" scott_continuity "scott/" )"bool" Cont nil )nil booleans nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil continuation nil )"continuous " continuation nil)) nil ))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" "{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 )"bool" scott_continuity "scott/" )"bool" scott_continuity "scott/" )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"bool" Cont nil )"bool" sets nil )set type-eq-decl nil sets nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil continuation nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"directed[Cont[V], (sq_le)]" continuationnil )"[[V -> int] -> lift[State[V]]]" nil )"set[R]" function_image nil )"bool" fun_preds_partial "scott/" )"(bijective?[T, T])" identity nil ))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" "lub_set_image" ("g" "g!1" "D" "D!1" ))"1" (assert )"1" (replace -6)"1" "image(g!1,D!1)" )"1" "1" replace -1)"1" "image(LAMBDA (x: Cont): f!1(g!1(x)), D!1) = image(f!1, image(g!1, D!1))" )"1" "1" expand "image" )"1" "1" "(EXISTS (x_1: (D!1)): x!1 = f!1(g!1(x_1)))" )"1" "1" "g!1(x!2)" )"1" "x!2" )nil nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "x!2" )"2" "2" replace -1)"2" replace "2" "2" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "image(LAMBDA (x: Cont): f!1(g!1(x)), D!1) = image(f!1, image(g!1, D!1))" )"2" "2" expand "image" )"2" "2" "(EXISTS (x_1: (D!1)): x!1 = f!1(g!1(x_1)))" )"1" "1" "g!1(x!2)" )"1" "x!2" )nil nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "x!2" )"2" "2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "directed_image" "g" "g!1" "D" "D!1" ))"2" assert )"2" "2" expand "image" )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "2" "g!1(x!1)" )"2" "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 )nil scott_continuity "scott/" )"bool" scott_continuity "scott/" )"bool" Cont nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil continuation nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"continuous " continuation nil) "T3" function_props nil )"bool" scott_continuity "scott/" )set type-eq-decl nil sets nil )"bool" sets nil )"bool" directed_order_props "orders/" )nil directed_order_props "orders/" )nil scott_continuity "scott/" )nil scott_continuity "scott/" )"bool" sets nil )"Cont[V]" continuation nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"(D!1)" continuation nil )"(D!1)" continuation nil )"directed[Cont, (sq_le)]" continuation nil )"scott_continuous[Cont, Cont, (sq_le), (sq_le)]" continuation nil )"set[R]" function_image nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" fun_preds_partial "scott/" )"(pointed_directed_complete_partial_order?[Cont])" continuationnil ))nil 3354465346"" (skosimp)"" (expand "assign" )"" (expand "assign" )"" (lemma "Cont.apply_continuous" )"" "(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 )"State" State nil )nil continuation nil )nil Cont nil )"LiftPartialFunction[X, Z]" nil )"[State -> int]" AExp nil )nil AExp nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T -> (up?)]" lift_adt nil )"[lift -> boolean]" lift_adt nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"State" State nil ))nil 3354078097"" (skosimp)"" (typepred "f!1" )"" (typepred "g!1" )"" (expand "scott_continuous?" )"" "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" "lub_set_image" ("g" "f!1" "D" "D!1" ))"1" "lub_set_image" "g" "g!1" "D" "D!1" ))"1" (assert )"1" "lub(image(f!1, D!1))" )"1" "lub(image(g!1, D!1))" )"1" "lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)), D!1))" )"1" expand "least_upper_bound?" )"1" "1" replace -13)"1" replace -15)"1" "conditional(B(b!1), lub(image(f!1, D!1)), lub(image(g!1, D!1)))" )"1" "1" "1" case "(sq_le)(conditional(B(b!1), lub(image(f!1, D!1)), LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)),") "1" "sq_le" )"1" expand "pointed_directed_complete_partial_order?" )"1" expand "directed_complete_partial_order?" )"1" expand "partial_order?" )"1" "1" expand "antisymmetric?" )"1" "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" "2" "lub(image(LAMBDA c: conditional(B(b!1),f!1(c),g!1(c)),D!1))" )"2" "LUB_C" "lub(image(LAMBDA c: conditional(B(b!1), f!1(c), g!1(c)), ") "2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" "2" replace "2" replace "2" replace "2" replace "2" "conditional(B(b!1), g!1(lub(D!1)), LUB_C)" )"2" "1" "conditional(B(b!1), LUB_C, f!1(lub(D!1)))" )"1" "1" "1" expand "sq_le" )"1" expand "conditional" )"1" "1" "s1!1" "s2!1" )"1" "s1!1" "s2!1" )"1" "B(b!1)(s1!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "r!1" )"2" expand "image" "2" "2" replace "2" "x!1" )"2" "2" "lub(D!1)" )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" "2" "x!1" )"2" expand "increasing?" )"2" "x!1" "lub(D!1)" )"2" "x!1" "lub(D!1)" )"2" assert )"2" "conditional(B(b!1), f!1(x!1), g!1(x!1))" )"1" expand "sq_le" )"1" "1" expand "conditional" )"1" "B(b!1)(s1!1)" )"1" "s1!1" "s2!1" )"1" assert )nil nil ))nil )"2" assert )"2" "s1!1" "s2!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "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" "2" expand "upper_bound?" "2" "2" "r!1" )"2" expand "image" "2" "2" "x!1" )"2" replace "2" rewrite "sq_le" "2" "2" expand "conditional" "2" "B(b!1)(s1!1)" )"1" "lub(D!1)" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" "1" "x!1" )"1" expand "increasing?" "1" "x!1" "lub(D!1)" )"1" assert )"1" expand "sq_le" "1" "s1!1" "s2!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "conditional(B(b!1), f!1(x!1), g!1(x!1))" )"1" expand "sq_le" "1" "s1!1" "s2!1" )"1" expand "conditional" "1" nil nil ))nil ))nil ))nil )"2" expand "image" )"2" "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" "2" expand "upper_bound?" )"2" "2" "r!1" )"2" expand "image" "2" "2" "x!1" )"2" replace "2" "2" expand "sq_le" "2" expand "conditional" "2" "2" "B(b!1)(s1!1)" )"1" replace "1" "1" expand "increasing?" )"1" "x!1" "lub(D!1)" )"1" "1" expand "sq_le" )"1" "s1!1" "s2!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "lub(D!1)" )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace "2" "lub(D!1)" )"2" expand "least_upper_bound?" )"2" expand "upper_bound?" "2" "2" "x!1" )"2" expand "increasing?" "2" "x!1" "lub(D!1)" )"2" assert )"2" expand "sq_le" "2" "s1!1" "s2!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (hide -2 -4 2)"2" (expand "increasing?" )"2" (skosimp*)"2" (inst - "x!1" "y!1" )"2" (inst - "x!1" "y!1" )"2" (assert )"2" (expand "sq_le" )"2" (skosimp)"2" expand "conditional" )"2" "s1!1" "s2!1" )"2" "s1!1" "s2!1" )"2" "B(b!1)(s1!1)" )"1" (assert ) 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 scott_continuity "scott/" )"bool" scott_continuity "scott/" )"bool" Cont nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil continuation nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil scott_continuity "scott/" )"[T, T -> boolean]" equalities nil )"(D!1)" continuation nil )"BExp[V]" continuation nil )"scott_continuous[Cont, Cont, (sq_le), (sq_le)]" continuation nil )"scott_continuous[Cont, Cont, (sq_le), (sq_le)]" continuation nil )"directed[Cont, (sq_le)]" continuation nil )"(D!1)" continuation nil )"bool" bounded_orders "orders/" )"bool" "orders/" )"bool" directed_orders"orders/" )"clopen[Cont, scott_open_sets]" nil )nil partial_order_props"orders/" )"bool" relations nil )"bool" orders nil )"set[R]" function_image nil )"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" "orders/" )"bool" bounded_order_props "orders/" )"bool" bounded_orders "orders/" )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"bool" sets nil )set type-eq-decl nil sets nil )"bool" scott_continuity "scott/" )"[State -> bool]" BExp nil )nil BExp nil )"Cont" Cont nil )nil defined_types nil )"bool" fun_preds_partial "scott/" )"(pointed_directed_complete_partial_order?[Cont])" continuationnil ))nil 3382283903"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "conditional" )"" (expand "o " )"" (case-replace "B(b!1)(x!1)" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil continuation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil lift_adt nil )"LiftPartialFunction[X, Z]" nil )nil PartialFunctionDefinitionsnil )"[State -> bool]" BExp nil )nil BExp nil )"Cont" Cont nil )nil Cont nil )nil defined_types nil )nil booleans nil ))nil 3353079331"" (skosimp)"" (lemma "assign_continuous" ("a" "a!1" "x" "x!1" ))"" (propax) nil nil )) nil ))nil )nil AExp nil )nil continuation nil )nil continuation nil ))nil ))nil 3353079331"" (skosimp)"" (expand "<<" )"" (assert )"" (flatten)"" (assert ) (("" (replace -1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(strict_well_founded?[Stm])" Stm nil )) nil ))nil 3353079331 ("" (grind) nil nil )nil continuation nil )"(strict_well_founded?[Stm])" Stm nil ))nil ))nil 3353079331"" (skosimp)"" (replace -1) (("" (expand "<<" ) (("" (propax) nil nil )) nil ))nil ))nil )"(strict_well_founded?[Stm])" Stm nil )) nil ))nil 3353079331"" (skosimp)"" (expand "<<" ) (("" (replace -1) (("" (assert ) nil nil )) nil ))nil ))nil )"(strict_well_founded?[Stm])" Stm nil )) nil ))nil 3353079331"" (skosimp*)"" (typepred "v!1(S1!1)" )"1" (typepred "v!1(S2!1)" )"1" "conditional_continuous" "b" "b!1" "f" "v!1(S1!1)" "g" "v!1(S2!1)" ))"1" (propax) nil nil )) nil )"2" (replace -2)"2" (expand "<<" ) (("2" (propax) nil nil )) nil )) nil ))nil )"2" (replace -1)"2" (expand "<<" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil )"(strict_well_founded?[Stm])" Stm nil )"bool" orders nil )nil defined_types nil )nil Stm nil )"bool" scott_continuity "scott/" )"bool" Cont nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil continuation nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil scott_continuity "scott/" )nil BExp nil )nil continuation nil ))nil ))nil 3353089153 ("" (skosimp) (("" (grind) nil nil )) nil )"(strict_well_founded?[Stm])" Stm nil )nil continuation nil ))nil ))nil 3353545746"" (skosimp*)"" (rewrite "conditional_continuous" )"1" (lemma "identity_continuous" )"1" (expand "I" ) (("1" (propax) nil nil )) nil )) nil )"2" (typepred "v!1(S1!1)" )"1" "composition_continuous" ("f" "v!1(S1!1)" "g" "g!1" ))"1" (expand "o " ) (("1" (propax) nil nil )) nil )) nil )"2" (replace -1)"2" (expand "<<" ) (("2" (propax) nil nil )) nil )) nil ))nil )"3" (replace -1)"3" (expand "<<" ) (("3" (propax) nil nil )) nil )) nil ))nil ))nil )nil continuation nil )nil continuation nil )nil BExp nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil State nil )nil lift_adt nil )nil Cont nil )nil booleans nil )"bool" Cont nil )"bool" scott_continuity "scott/" )nil scott_continuity "scott/" )nil Stm nil )nil defined_types nil )"bool" orders nil )"(strict_well_founded?[Stm])" Stm nil )"(bijective?[T, T])" identity nil )nil continuation nil )nil continuation nil )"T3" function_props nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3353545746"" (skosimp*)"" (typepred "v!1(S1!1)" )"1" (expand "scott_continuous?" )"1" (flatten)"1" (hide -2)"1" (expand "increasing?" )"1" (skolem + ("f!1" "g!1" ))"1" (flatten)"1" (expand "continuous_pointwise" )"1" (expand "pointwise" )"1" (skolem + "c!1" )"1" (inst -3 "c!1" )"1" (inst - "f!1(c!1)" "g!1(c!1)" )"1" (assert )"1" "1" expand "sq_le" )"1" "s!1" "s!2" ))"1" "1" "s!1" "s!2" )"1" expand "conditional" )"1" "B[V](b!1)(s!1)" )"1" (assert ) 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 )"2" (replace -1)"2" (expand "<<" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil )"(strict_well_founded?[Stm])" Stm nil )"bool" orders nil )nil defined_types nil )nil Stm nil )"bool" scott_continuity "scott/" )"bool" Cont nil )nil Cont nil )nil lift_adt nil )nil State nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil continuation nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" fun_preds_partial "scott/" )"bool" pointwise_orders "orders/" )"(pointed_directed_complete_partial_order?[Cont])" continuationnil )"Cont" Cont nil )nil BExp nil )"[State -> bool]" BExp nil )nil scott_continuity "scott/" )"bool" pointwise_orders_aux"scott/" ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.47 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
