| products/Sources/formale Sprachen/PVS/while/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: direct_sos.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(direct_sos
(sos_le_direct 0 (sos_le_direct-1 nil 3398581278 ("" (case "forall (S:Stm,s,s1:State): step(S,s)=T(s1) => direct.SS(S)(s) = up(s1)") (("1" (case "FORALL (S,S1: Stm, s, s1: State): step(S, s) = I(S1,s1) => direct.SS(S)(s) = direct.SS(S1)(s1)") (("1" (case "forall (n:nat,s,s1:State,S:Stm): tr(n)(I(S,s),T(s1)) => direct.SS(S)(s) = (("1" (hide -2 -3) (("1" (skosimp) (("1" (inst - "_" "_" _ " S!1") (("1" (expand "sq_le") (("1" (skosimp) (("1" (inst - "_" "s1!1" "s2!1") (("1" (name-replace "RHS" "direct.SS(S!1)(s1!1) = up(s2!1)") (("1" (lemma "SS_deterministic" ("S" "S!1" "s" "s1!1" "s1" "s2!1")) (("1" (assert) (("1" (skosimp) (("1" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "tr") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (expand "tr" -2) (("2" (case "T?(step(S!1, s!1))") (("1" (hide -2 -4) (("1" (expand "tr" -2) (("1" (assert) (("1" (prop) (("1" (inst - "S!1" "s!1" "s1!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "I?(step(S!1, s!1))") (("1" (hide 1) (("1" (inst - "s(step(S!1, s!1))" "s1!1" "S(step(S!1, s!1))") (("1" (split -2) (("1" (inst -4 "S!1" "S(step(S!1, s!1))" "s!1" "s(step(S!1, s!1))") (("1" (replace -1) (("1" (split -4) (("1" (propax) nil nil) ("2" (hide -1 -4 -3 2) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (case-replace "I(S(step(S!1, s!1)), s(step(S!1, s!1)))=step(S!1, s!1)") (("2" (hide -2 2) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "S") (("1" (skolem + ("x!1" "a!1")) (("1" (skosimp) (("1" (expand "step") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "SS" 1) (("2" (expand "step" -1) (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skolem + ("S!1" "S!2")) (("3" (flatten) (("3" (skosimp) (("3" (case "T?(step(S!1,s!1))") (("1" (case "S1!1=S!2 & s1(step(S!1, s!1))=s1!1") (("1" (flatten) (("1" (replace -1) (("1" (inst -7 "S!1" "s!1" "s1!1") (("1" (split -7) (("1" (expand "SS" 1 1) (("1" (expand "o") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -2 1 rl) (("2" (hide-all-but (-3 1)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -2 -3 -5) (("2" (expand "step" -2) (("2" (assert) (("2" (decompose-equality) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (case "I?(step(S!1, s!1))") (("1" (hide 1) (("1" (case "S1!1=Sequence(S(step(S!1,s!1)), S!2) & s(step(S!1,s!1))=s1!1") (("1" (flatten) (("1" (replace -1) (("1" (expand "SS" 1) (("1" (inst -4 "S(step(S!1, s!1))" "s!1" "s1!1") (("1" (split -4) (("1" (expand "o") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (replace -2 1 rl) (("2" (hide-all-but (-3 1)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -2 -3 -5) (("2" (expand "step" -2) (("2" (assert) (("2" (decompose-equality) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skolem + ("b!1" "S!1" "S!2")) (("4" (skosimp) (("4" (skosimp) (("4" (expand "step" -3) (("4" (lift-if) (("4" (expand "SS" 1 1) (("4" (expand "conditional") (("4" (lift-if) (("4" (case-replace "B(b!1)(s!1)") (("1" (hide -3 -5) (("1" (hide -1 -2) (("1" (decompose-equality) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -1 -2 -4 1) (("2" (decompose-equality) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skolem + ("b!1" "S!1")) (("5" (flatten) (("5" (skosimp) (("5" (expand "step" -2) (("5" (decompose-equality) (("5" (replace -1 * rl) (("5" (replace -2 * rl) (("5" (hide -1 -2) (("5" (expand "SS" 1) (("5" (rewrite "fix_prop" 1 :dir rl) (("1" (expand "conditional" 1 3) (("1" (expand "conditional" 1 1) (("1" (case-replace "B(b!1)(s!1)") (("1" (expand "SS" 1 3) (("1" (expand "SS" 1 3) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "SS" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -2) (("2" (rewrite "scott_continuous_def") (("2" (lemma "apply_continuous" ("c1" "direct.SS(S!1)")) (("2" (lemma "conditional_continuous" ("b" "b!1" "f" "LAMBDA (c:Cont): c o direct.SS(S!1)" "g" "lambda (c:Cont): LAMBDA (s:State): up[State](s)")) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (expand "scott_continuous?") (("2" (split) (("1" (expand "increasing?") (("1" (skosimp*) (("1" (expand "sq_le") (("1" (skosimp) nil nil)) nil)) nil)) nil) ("2" (expand "lub_preserving?") (("2" (skosimp*) (("2" (case-replace "image[Cont,Cont](LAMBDA (c: Cont): LAMBDA (s: State): up[State](s), D!1) = sing (("1" (hide -1) (("1" (rewrite "lub_singleton") nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "singleton") (("2" (expand "image") (("2" (typepred "D!1") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (case-replace "(LAMBDA (s: State): up[State](s))=x!1") (("1" (inst + "x!2") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) 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" (expand "SS") (("2" (expand "step") (("2" (case "Assign?(S!1)") (("1" (assert) (("1" (decompose-equality) (("1" (assert) nil nil)) nil)) nil) ("2" (case "Skip?(S!1)") (("1" (assert) (("1" (decompose-equality) (("1" (assert) nil nil)) nil)) nil) ("2" (case "Sequence?(S!1)") (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil) ("2" (case "Conditional?(S!1)") (("1" (assert) nil nil) ("2" (case "While?(S!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (a adt-accessor-decl "[(Assign?) -> AExp[V]]" Stm nil) (A def-decl "[State -> int]" AExp nil) (AExp type-decl nil AExp nil) (x adt-accessor-decl "[(Assign?) -> V]" Stm nil) (assign const-decl "State" State nil) (I? adt-recognizer-decl "[Config -> boolean]" sos nil) (I adt-constructor-decl "[[Stm[V], State[V]] -> (I?)]" sos nil) (S!1 skolem-const-decl "Stm[V]" direct_sos nil) (s!1 skolem-const-decl "State[V]" direct_sos nil) (S adt-accessor-decl "[(I?) -> Stm[V]]" sos nil) (s adt-accessor-decl "[(I?) -> State[V]]" sos nil) (Config_I_extensionality formula-decl nil sos nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (SS_deterministic formula-decl nil sos nil) (sq_le const-decl "bool" Cont nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (tr def-decl "bool" sos nil) (Stm_induction formula-decl nil Stm nil) (Config_T_extensionality formula-decl nil sos nil) (O const-decl "LiftPartialFunction[X, Z]" PartialFunctionComposition nil) (s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm nil) (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (BExp type-decl nil BExp nil) (B def-decl "[State -> bool]" BExp nil) (conditional const-decl "Cont" Cont nil) (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (continuous? const-decl "bool" continuity_def "topology/") (scott_open_sets const-decl "setofsets[T]" scott "scott/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (fix_prop formula-decl nil fixpoints "scott/") (apply_continuous formula-decl nil Cont nil) (increasing? const-decl "bool" fun_preds_partial "scott/") (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (sq_le_pdcpo name-judgement "(pointed_directed_complete_partial_order?[Cont])" direct_sos nil) (D!1 skolem-const-decl "directed[Cont[V], (sq_le)]" direct_sos nil) (x!2 skolem-const-decl "Cont[V]" direct_sos nil) (lub_singleton formula-decl nil bounded_order_props "orders/") (directed_singleton application-judgement "directed[Cont[V], (sq_le)]" direct_sos nil) (singleton_is_compact application-judgement "compact[Cont[V], scott_open_sets]" direct_sos nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[Cont[V]]" direct_sos nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (nonempty? const-decl "bool" sets nil) (directed? const-decl "bool" directed_order_props "orders/") (directed type-eq-decl nil directed_order_props "orders/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (lub_preserving? const-decl "bool" scott_continuity "scott/") (scott_continuous type-eq-decl nil scott_continuity "scott/") (scott_continuous? const-decl "bool" scott_continuity "scott/") (conditional_continuous formula-decl nil continuation nil) (scott_continuous_def formula-decl nil scott_continuity "scott/") (Skip adt-constructor-decl "(Skip?)" Stm nil) (Skip? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (While adt-constructor-decl "[[BExp[V], Stm] -> (While?)]" Stm nil) (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Conditional adt-constructor-decl "[[BExp[V], Stm, Stm] -> (Conditional?)]" Stm nil) (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (V formal-nonempty-type-decl nil direct_sos nil) (Stm type-decl nil Stm 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) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Config type-decl nil sos nil) (= const-decl "[T, T -> boolean]" equalities nil) (step def-decl "[Config]" sos nil) (T? adt-recognizer-decl "[Config -> boolean]" sos nil) (T adt-constructor-decl "[State[V] -> (T?)]" sos nil) (lift type-decl nil lift_adt nil) (Cont nonempty-type-eq-decl nil Cont nil) (SS def-decl "Cont" direct nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)) shostak)) (direct_le_sos 0 (direct_le_sos-1 nil 3398735323 ("" (induct "S") (("1" (skolem + ("x!1" "a!1")) (("1" (expand "SS") (("1" (expand "sq_le") (("1" (skolem + ("s!1" "s!2")) (("1" (flatten) (("1" (lift-if) (("1" (assert) (("1" (lemma "SS_deterministic" ("S" "Assign(x!1, a!1)" "s" "s!1" "s1" "s!2")) (("1" (case-replace "EXISTS (n:nat): tr(n)(I(Assign(x!1, a!1), s!1), T(s!2))") (("1" (assert) (("1" (expand "SS" -2) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (inst + "1") (("2" (expand "tr") (("2" (expand "tr") (("2" (expand "step") (("2" (decompose-equality) (("2" (decompose-equality) (("2" (decompose-equality) (("2" (decompose-equality) (("2" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "SS") (("2" (expand "sq_le") (("2" (skosimp) (("2" (decompose-equality) (("2" (lift-if) (("2" (assert) (("2" (lemma "SS_deterministic" ("S" "Skip" "s" "s1!1" "s1" "s2!1")) (("2" (case-replace "EXISTS (n:nat): tr(n)(I(Skip, s1!1), T(s2!1))") (("1" (assert) (("1" (expand "SS") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (inst + "1") (("2" (expand "tr") (("2" (expand "tr") (("2" (expand "step") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem + ("S!1" "S!2")) (("3" (flatten) (("3" (expand "SS" 1 1) (("3" (name-replace "C1" "direct.SS(S!1)") (("3" (name-replace "C2" "direct.SS(S!2)") (("3" (expand "sq_le") (("3" (skosimp) (("3" (expand " o" -3) (("3" (lift-if) (("3" (assert) (("3" (prop) (("3" (inst -3 "down(C1(s1!1))" "s2!1") (("3" (assert) (("3" (inst - "s1!1" "down(C1(s1!1))") (("3" (rewrite "up_down") (("3" (hide -1) (("3" (name-replace "si" "lift_adt[State[V].State].down(C1(s1!1))") (("3" (case-replace "C1(s1!1)= up(si)") (("1" (hide -1 1) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp*) (("1" (lemma "tr_partial" ("k" "n!1" "S1" "S!1" "S2" "S!2" "s0" "s1!1" "s1" "si")) (("1" (assert) (("1" (inst + "n!1+n!2") (("1" (rewrite "tr_add") (("1" (inst + "I(S!2, si)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "si") (("2" (rewrite "up_down") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skolem + ("b!1" "S!1" "S!2")) (("4" (flatten) (("4" (expand "SS" 1 1) (("4" (name-replace "C1" "direct.SS(S!1)") (("4" (name-replace "C2" "direct.SS(S!2)") (("4" (expand "sq_le") (("4" (skolem + ("s!1" "s!2")) (("4" (flatten) (("4" (inst - "s!1" "s!2") (("4" (inst - "s!1" "s!2") (("4" (expand "conditional") (("4" (lift-if) (("4" (case-replace "B(b!1)(s!1)") (("1" (assert) (("1" (hide-all-but (-1 -2 1)) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp) (("1" (inst + "n!1+1") (("1" (expand "tr" 1) (("1" (expand "step") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (hide -1 -3) (("2" (rewrite "SS_deterministic" * :dir rl) (("2" (rewrite "SS_deterministic" * :dir rl) (("2" (skosimp) (("2" (inst + "n!1+1") (("2" (expand "tr" 2) (("2" (expand "step") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skolem + ("b!1" "S!1")) (("5" (flatten) (("5" (expand "SS" 1 1) (("5" (name-replace "C1" "direct.SS(S!1)") (("5" (name-replace "F" "LAMBDA (c:Cont): conditional(B(b!1), c o C1, LAMBDA (s:State): up(s))") (("5" (case "sq_le(F(sos.SS(While(b!1, S!1))),sos.SS(While(b!1, S!1)))") (("1" (lemma "fixpoint_contraction" ("psi" "F" "x" "sos.SS(While(b!1, S!1))")) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (rewrite "scott_continuous_def") (("2" (expand "F") (("2" (lemma "conditional_continuous") (("2" (inst?) (("1" (hide 2) (("1" (expand "scott_continuous?") (("1" (split) (("1" (expand "increasing?") (("1" (expand "sq_le") (("1" (skosimp*) nil nil)) nil)) nil) ("2" (expand "lub_preserving?") (("2" (skosimp) (("2" (case-replace "image[Cont,Cont](LAMBDA (c: Cont): LAMBDA (s: State): up[State](s), D!1)=single (("1" (rewrite "lub_singleton") nil nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (expand "singleton") (("2" (case-replace "(LAMBDA (s: State): up[State](s))=x!1") (("1" (expand "image") (("1" (typepred "D!1") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (inst + "x!2") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "image") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "apply_continuous" ("c1" "C1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "sq_le") (("2" (skolem + ("s!1" "s!2")) (("2" (flatten) (("2" (expand "F" -1) (("2" (expand "conditional") (("2" (lift-if) (("2" (expand "o" -1) (("2" (assert) (("2" (case-replace "B(b!1)(s!1)") (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (inst - "s!1" "down(C1(s!1))") (("1" (rewrite "up_down") (("1" (name-replace "si" "lift_adt[State[V].State].down(C1(s!1))") (("1" (case-replace "C1(s!1)=up(si)") (("1" (hide -1 1) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (rewrite "SS_deterministic" * :dir rl) (("1" (skosimp*) (("1" (expand "tr" 1) (("1" (expand "step" 1) (("1" (expand "tr" 1) (("1" (expand "step" 1) (("1" (inst + "n!1+n!2+2") (("1" (assert) (("1" (lemma "tr_partial" ("k" "n!2" "S1" "S!1" "s0" "s!1" "s1" "si" "S2" "While(b!1, S!1)")) (("1" (assert) (("1" (hide -4) (("1" (lemma "tr_add" ("k1" "n!2" "c0" "sos.I(Sequence(S!1, While(b!1, S!1)), s!1)" "k2" "n!1" "c2" "T(s!2)")) (("1" (replace -1) (("1" (hide -1) (("1" (inst + "sos.I(While(b!1, S!1), si)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "si") (("2" (rewrite "up_down") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2) (("2" (decompose-equality) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (rewrite "SS_deterministic" * :dir rl) (("2" (inst + "3") (("2" (expand "tr") (("2" (expand "tr") (("2" (expand "step") (("2" (expand "tr") (("2" (expand "step") (("2" (expand "tr") (("2" (propax) 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) ((pred type-eq-decl nil defined_types nil) (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (si skolem-const-decl "State[V]" direct_sos nil) (fixpoint_contraction formula-decl nil fixpoints "scott/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (scott_open_sets const-decl "setofsets[T]" scott "scott/") (continuous? const-decl "bool" continuity_def "topology/") (sq_le_pdcpo name-judgement "(pointed_directed_complete_partial_order?[Cont])" direct_sos nil) (scott_continuous_def formula-decl nil scott_continuity "scott/") (conditional_continuous formula-decl nil continuation nil) (apply_continuous formula-decl nil Cont nil) (increasing? const-decl "bool" fun_preds_partial "scott/") (member const-decl "bool" sets nil) (x!2 skolem-const-decl "Cont[V]" direct_sos nil) (D!1 skolem-const-decl "directed[Cont[V], (sq_le)]" direct_sos nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (lub_singleton formula-decl nil bounded_order_props "orders/") (directed_singleton application-judgement "directed[Cont[V], (sq_le)]" direct_sos nil) (singleton_is_compact application-judgement "compact[Cont[V], scott_open_sets]" direct_sos nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[Cont[V]]" direct_sos nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (nonempty? const-decl "bool" sets nil) (directed? const-decl "bool" directed_order_props "orders/") (directed type-eq-decl nil directed_order_props "orders/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (lub_preserving? const-decl "bool" scott_continuity "scott/") (C1 skolem-const-decl "Cont[V]" direct_sos nil) (scott_continuous? const-decl "bool" scott_continuity "scott/") (scott_continuous type-eq-decl nil scott_continuity "scott/") (F skolem-const-decl "[Cont[V] -> Cont[V]]" direct_sos nil) (While adt-constructor-decl "[[BExp[V], Stm] -> (While?)]" Stm nil) (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (conditional const-decl "Cont" Cont nil) (B def-decl "[State -> bool]" BExp nil) (BExp type-decl nil BExp nil) (Conditional adt-constructor-decl "[[BExp[V], Stm, Stm] -> (Conditional?)]" Stm nil) (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (up_down formula-decl nil lift_props "orders/") (si skolem-const-decl "State[V]" direct_sos nil) (tr_add formula-decl nil sos nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (tr_partial formula-decl nil sos nil) (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm nil) (O const-decl "LiftPartialFunction[X, Z]" PartialFunctionComposition nil) (Skip? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (Skip adt-constructor-decl "(Skip?)" Stm nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Config type-decl nil sos nil) (tr def-decl "bool" sos nil) (I? adt-recognizer-decl "[Config -> boolean]" sos nil) (I adt-constructor-decl "[[Stm[V], State[V]] -> (I?)]" sos nil) (T? adt-recognizer-decl "[Config -> boolean]" sos nil) (T adt-constructor-decl "[State[V] -> (T?)]" sos nil) (A def-decl "[State -> int]" AExp nil) (assign const-decl "State" State nil) (Config_T_extensionality formula-decl nil sos nil) (up adt-constructor-decl "[T -> (up?)]" lift_adt nil) (down adt-accessor-decl "[(up?) -> T]" lift_adt nil) (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (step def-decl "[Config]" sos nil) (Assign adt-constructor-decl "[[V, AExp[V]] -> (Assign?)]" Stm nil) (Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil) (AExp type-decl nil AExp nil) (SS_deterministic formula-decl nil sos nil) (Stm_induction formula-decl nil Stm nil) (V formal-nonempty-type-decl nil direct_sos nil) (SS const-decl "Cont" sos nil) (SS def-decl "Cont" direct nil) (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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (Stm type-decl nil Stm nil)) shostak)) (direct_eq_sos 0 (direct_eq_sos-1 nil 3398581185 ("" (skosimp) (("" (lemma "sos_le_direct" ("S" "S!1")) (("" (lemma "direct_le_sos" ("S" "S!1")) (("" (typepred "sq_le") (("" (expand "pointed_directed_complete_partial_order?") (("" (expand "directed_complete_partial_order?") (("" (expand "partial_order?") (("" (flatten) (("" (expand "antisymmetric?") (("" (inst - "direct.SS(S!1)" "sos.SS(S!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Stm type-decl nil Stm nil) (V formal-nonempty-type-decl nil direct_sos nil) (sos_le_direct formula-decl nil direct_sos nil) (sq_le const-decl "bool" Cont nil) (pointed_directed_complete_partial_order? const-decl "bool" directed_orders "orders/") (pred type-eq-decl nil defined_types nil) (Cont nonempty-type-eq-decl nil Cont nil) (lift type-decl nil lift_adt nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.47 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.Bot Zugriff |
