|
(relational_choice_properties
(fun_choice_impl_description 0
(fun_choice_impl_description-1 nil 3569913521 ("" (grind) nil nil)
((parametric_definite_description const-decl "bool"
relational_choice nil)
(fun_choice const-decl "bool" relational_choice nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(fun_choice_impl_rel_unique_choice 0
(fun_choice_impl_rel_unique_choice-1 nil 3569913791
("" (flatten)
(("" (expand "fun_choice")
(("" (expand "rel_unique_choice")
(("" (skolem! 1)
(("" (inst -1 "R!1")
(("" (flatten)
(("" (prop)
(("" (skolem-typepred)
(("" (inst 1 "LAMBDA(t:T,u:U):u=f!1(t)")
(("" (skolem-typepred)
(("" (inst 1 "f!1(t!1)")
(("" (split)
(("1" (inst -1 "t!1") nil nil)
("2" (inst?)
(("2" (skolem! 1)
(("2"
(prop)
(("2"
(replace -1 1 rl)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fun_choice const-decl "bool" relational_choice nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil)
(rel_unique_choice const-decl "bool" relational_choice nil))
shostak))
(fun_choice_impl_rel_choice 0
(fun_choice_impl_rel_choice-1 nil 3569913534
("" (flatten)
(("" (auto-rewrite-defs :always? t)
((""
(assert :let-reduce? t :cases-rewrite? nil :ignore-typepreds?
nil)
(("" (skolem-typepred)
(("" (flatten)
((""
(assert :let-reduce? t :quant-simp? nil
:implicit-typepreds? nil :ignore-typepreds? nil
:cases-rewrite? nil)
(("" (inst? :if-match t :polarity? nil)
(("" (replace*)
((""
(assert :let-reduce? t :quant-simp? nil
:implicit-typepreds? nil :ignore-typepreds?
nil :cases-rewrite? nil)
(("" (inst? :if-match t :polarity? nil)
(("" (skolem-typepred)
(("" (replace*)
((""
(assert :let-reduce? t :quant-simp? nil
:implicit-typepreds? nil
:ignore-typepreds? nil
:cases-rewrite? nil)
(("" (skolem-typepred)
(("" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil)
(fun_choice const-decl "bool" relational_choice nil)
(\|- const-decl "bool" relation_implication nil)
(rel_choice const-decl "bool" relational_choice nil))
shostak))
(fun_choice_impl_rel_choice_impl_description_rel_choice 0
(fun_choice_impl_rel_choice_impl_description_rel_choice-1 nil
3569927551
("" (flatten)
(("" (expand "parametric_definite_description")
(("" (expand "rel_choice")
(("" (expand "fun_choice")
(("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((parametric_definite_description const-decl "bool"
relational_choice nil)
(fun_choice const-decl "bool" relational_choice nil)
(\|- const-decl "bool" relation_implication nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(rel_choice const-decl "bool" relational_choice nil))
shostak))
(fun_choice_impl_rel_choice_and_description_rel_choice 0
(fun_choice_impl_rel_choice_and_description_rel_choice-1 nil
3569927629
("" (flatten)
(("" (prop)
(("1" (rewrite "fun_choice_impl_rel_choice") nil nil)
("2" (rewrite "fun_choice_impl_description") nil nil))
nil))
nil)
((fun_choice_impl_rel_choice formula-decl nil
relational_choice_properties nil)
(fun_choice_impl_description formula-decl nil
relational_choice_properties nil))
shostak))
(fun_choice_impl_rel_unique_choice_impl_description_rel_choice 0
(fun_choice_impl_rel_unique_choice_impl_description_rel_choice-1 nil
3569913544 ("" (grind) nil nil)
((parametric_definite_description const-decl "bool"
relational_choice nil)
(rel_unique_choice const-decl "bool" relational_choice nil)
(fun_choice const-decl "bool" relational_choice nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(fun_choice_impl_rel_unique_choice_and_description_rel_choice 0
(fun_choice_impl_rel_unique_choice_and_description_rel_choice-1 nil
3569913565
("" (flatten)
(("" (prop)
(("1" (rewrite "fun_choice_impl_rel_unique_choice") nil nil)
("2" (rewrite "fun_choice_impl_description") nil nil))
nil))
nil)
((fun_choice_impl_rel_unique_choice formula-decl nil
relational_choice_properties nil)
(fun_choice_impl_description formula-decl nil
relational_choice_properties nil))
shostak))
(description_rel_unique_choice_imp_funct_choice 0
(description_rel_unique_choice_imp_funct_choice-1 nil 3569929474
("" (prop)
(("" (expand "fun_choice")
(("" (skosimp*)
(("" (expand "rel_unique_choice")
(("" (inst -2 "R!1")
(("" (prop)
(("" (skolem!)
(("" (expand "parametric_definite_description")
(("" (inst -2 "R1!1")
(("" (prop)
(("1" (skolem! -1)
(("1" (inst 1 "f!1")
(("1" (skolem! 1)
(("1" (inst -1 "t!1")
(("1"
(inst -2 "t!1")
(("1"
(skolem!)
(("1"
(prop)
(("1"
(inst -4 "f!1(t!1)")
(("1"
(prop)
(("1"
(replace -1 1 rl)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst?)
(("2" (skolem!)
(("2" (prop)
(("2"
(inst 1 "u!1")
(("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fun_choice const-decl "bool" relational_choice nil)
(rel_unique_choice const-decl "bool" relational_choice nil)
(parametric_definite_description const-decl "bool"
relational_choice nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil))
shostak))
(description_rel_and_rel_unique_choice_imp_funct_choice 0
(description_rel_and_rel_unique_choice_imp_funct_choice-1 nil
3569927488
("" (flatten)
(("" (rewrite "description_rel_unique_choice_imp_funct_choice") nil
nil))
nil)
((description_rel_unique_choice_imp_funct_choice formula-decl nil
relational_choice_properties nil))
shostak))
(rel_choice_and_proof_irrel_imp_guarded_rel_choice 0
(rel_choice_and_proof_irrel_imp_guarded_rel_choice-1 nil 3570044635
("" (flatten)
(("" (expand "conditional_relational_choice")
(("" (expand "proof_irrelevance")
(("" (expand "rel_unique_choice")
(("" (skolem!)
(("" (skolem!)
(("" (prop)
(("" (inst -1 "R!1")
(("" (prop)
(("1" (skolem!)
(("1" (inst 1 "R1!1")
(("1" (skolem!)
(("1" (inst?) (("1" (flatten) nil nil)) nil))
nil))
nil))
nil)
("2" (inst 2 "R!1")
(("2" (skolem!)
(("2" (skolem!)
(("2" (bddsimp)
(("2" (assert)
(("2"
(inst?)
(("2"
(replace 1 -1 rl)
(("2"
(assert)
(("2"
(inst -1 "P!1(t!2)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((conditional_relational_choice const-decl "bool" relational_choice
nil)
(rel_unique_choice const-decl "bool" relational_choice nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(proof_irrelevance const-decl "bool" relational_choice nil))
shostak))
(relx_choice_indep_of_premises_imp_guarded_rel_choice 0
(relx_choice_indep_of_premises_imp_guarded_rel_choice-1 nil
3570114627
("" (flatten)
(("" (expand "conditional_relational_choice")
(("" (skolem! 1)
(("" (skolem! 1)
(("" (prop)
(("" (expand "rel_unique_choice")
(("" (inst -1 "LAMBDA(t:T,u:U):P!1(t) IMPLIES R!1(t,u)")
(("" (prop)
(("1" (skolem!)
(("1" (inst 1 "R1!1")
(("1" (skolem! 1)
(("1" (prop)
(("1" (inst?)
(("1" (skolem!)
(("1"
(prop)
(("1"
(inst 1 "u!1")
(("1" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "independence_of_premises")
(("2" (inst -1 "P!1")
(("2" (skolem! 1)
(("2" (inst -1 "P!1(t!1)")
(("2" (prop)
(("1" (assert)
(("1"
(inst?)
(("1"
(prop)
(("1"
(inst 2 "R!1")
(("1"
(skolem!)
(("1"
(skolem!)
(("1"
(inst?)
(("1" (prop) nil nil))
nil))
nil))
nil))
nil)
("2"
(inst 3 "R!1")
(("2"
(skolem! 3)
(("2"
(flatten)
(("2"
(skolem!)
(("2"
(prop)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 1 "t!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((conditional_relational_choice const-decl "bool" relational_choice
nil)
(rel_unique_choice const-decl "bool" relational_choice nil)
(independence_of_premises const-decl "bool" relational_choice nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil relational_choice_properties nil)
(T formal-nonempty-type-decl nil relational_choice_properties nil))
shostak))
(fun_choice_equiv_rel_unique_param_desc 0
(fun_choice_equiv_rel_unique_param_desc-1 nil 3569914637
("" (prop)
(("1" (rewrite "fun_choice_impl_rel_unique_choice") nil nil)
("2" (rewrite "fun_choice_impl_description") nil nil)
("3" (rewrite "description_rel_unique_choice_imp_funct_choice")
nil nil))
nil)
((description_rel_unique_choice_imp_funct_choice formula-decl nil
relational_choice_properties nil)
(fun_choice_impl_description formula-decl nil
relational_choice_properties nil)
(fun_choice_impl_rel_unique_choice formula-decl nil
relational_choice_properties nil))
shostak)))
¤ Dauer der Verarbeitung: 0.6 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
