|
(los_graph
(los_graphic 0
(los_graphic-2 "informal" 3349093821
("" (skosimp*)
(("" (case "NOT P!1(x!2,x!1)")
(("1" (case "NOT P!1(x!1,y!2)")
(("1" (copy -5)
(("1" (inst -1 "x!1" "y!2")
(("1" (copy -6)
(("1" (inst -1 "x!2" "x!1")
(("1" (inst -5 "x!2" "x!1" "y!2")
(("1" (prop) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (case "NOT P!1(y!1,y!2)")
(("1" (copy -6)
(("1" (inst -1 "y!1" "y!2")
(("1" (copy -7)
(("1" (inst -1 "x!2" "x!1")
(("1" (copy -8)
(("1" (inst -1 "x!1" "y!1")
(("1" (prop)
(("1" (copy -7)
(("1" (inst -1 "x!2" "x!1" "y!2")
(("1" (prop)
(("1"
(inst -7 "x!1" "y!1" "y!2")
(("1" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst -4 "y!1" "y!2")
(("2" (prop)
(("2" (inst -4 "x!1" "y!2" "y!1") (("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "NOT P!1(x!2,y!1)")
(("1" (case "NOT P!1(y!1,y!2)")
(("1" (copy -6)
(("1" (inst -1 "x!2" "y!1")
(("1" (inst -7 "y!1" "y!2")
(("1" (prop)
(("1" (inst -6 "x!2" "y!1" "y!2")
(("1" (prop) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (inst -7 "x!2" "y!2")
(("2" (prop)
(("2" (inst -5 "y!1" "y!2")
(("2" (prop)
(("2" (inst -5 "x!2" "y!2" "y!1")
(("2" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst -4 "x!2" "x!1")
(("2" (inst -3 "x!1" "x!2" "y!1") (("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil los_graph nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)
(los_graphic-1 nil 3328254156
("" (skosimp*)
(("" (case "P!1(x!2,x!1)&P!1(x!2,y!1)")
(("1" (inst -3 "x!2" "x!1")
(("1" (inst -2 "x!1" "x!2" "y!1") (("1" (prop) nil nil)) nil))
nil)
("2" (case "P!1(x!1,y!2)&P!1(y!1,y!2)")
(("1" (inst -3 "y!1" "y!2")
(("1" (inst -2 "x!1" "y!2" "y!1") (("1" (prop) nil nil))
nil))
nil)
("2" (inst-cp -5 "x!1" "y!2")
(("2" (inst-cp -5 "y!1" "y!2")
(("2" (inst-cp -5 "y!1" "x!2")
(("2" (inst-cp -5 "x!1" "x!2")
(("2" (bddsimp)
(("1" (hide -6)
(("1" (inst -3 "y!1" "x!2") (("1" (prop) nil nil))
nil))
nil)
("2" (inst -5 "y!1" "x!2")
(("2" (inst -4 "x!2" "y!1" "y!2")
(("2" (prop) nil nil)) nil))
nil)
("3" (inst -3 "y!1" "x!2") (("3" (prop) nil nil))
nil)
("4" (inst -5 "y!1" "x!2")
(("4" (inst -4 "x!2" "y!1" "y!2")
(("4" (prop) nil nil)) nil))
nil)
("5" (inst -3 "y!1" "x!2")
(("5" (inst -2 "x!1" "x!2" "y!1")
(("5" (prop) nil nil)) nil))
nil)
("6" (inst -5 "y!1" "x!2")
(("6" (inst -4 "x!2" "y!1" "y!2")
(("6" (prop) nil nil)) nil))
nil)
("7" (inst -6 "x!2" "y!2")
(("7" (prop)
(("7" (inst -4 "x!1" "y!2")
(("7" (inst -3 "x!2" "y!2" "x!1")
(("7" (prop) nil nil)) nil))
nil))
nil))
nil)
("8" (inst -5 "y!1" "x!2")
(("8" (inst -4 "x!2" "y!1" "y!2")
(("8" (prop) nil nil)) nil))
nil)
("9" (inst -3 "y!1" "x!2")
(("9" (inst -2 "x!1" "x!2" "y!1")
(("9" (prop) nil nil)) nil))
nil)
("10" (inst -6 "x!2" "y!2")
(("10" (prop)
(("10" (inst -3 "x!1" "x!2" "y!2")
(("10" (prop) nil nil)) nil))
nil))
nil)
("11" (inst -5 "x!1" "x!2")
(("11" (inst -4 "x!2" "x!1" "y!2")
(("11" (prop) nil nil)) nil))
nil)
("12" (inst -6 "x!1" "y!2")
(("12" (prop)
(("12" (inst -6 "x!1" "x!2")
(("12" (prop)
(("12" (inst -6 "x!2" "x!1" "y!2")
(("12" (prop) nil nil)) nil))
nil))
nil))
nil))
nil)
("13" (inst -3 "y!1" "x!2")
(("13" (inst -2 "x!1" "x!2" "y!1")
(("13" (prop) nil nil)) nil))
nil)
("14" (inst -3 "x!1" "x!2") (("14" (prop) nil nil))
nil)
("15" (inst -5 "x!1" "x!2")
(("15" (inst -4 "x!2" "x!1" "y!2")
(("15" (prop) nil nil)) nil))
nil)
("16" (inst -5 "x!1" "x!2")
(("16" (inst -4 "x!2" "x!1" "y!2")
(("16" (prop) nil nil)) nil))
nil)
("17" (inst -2 "y!1" "x!2")
(("17" (inst -1 "x!1" "x!2" "y!1")
(("17" (prop) nil nil)) nil))
nil)
("18" (inst -4 "y!1" "x!2")
(("18" (inst -3 "x!2" "y!1" "y!2")
(("18" (prop) nil nil)) nil))
nil)
("19" (inst -4 "x!1" "x!2")
(("19" (inst -3 "x!2" "x!1" "y!2")
(("19" (prop) nil nil)) nil))
nil)
("20" (inst -4 "y!1" "x!2")
(("20" (inst -3 "x!2" "y!1" "y!2")
(("20" (prop) nil nil)) nil))
nil)
("21" (inst -2 "y!1" "x!2")
(("21" (inst -1 "x!1" "x!2" "y!1")
(("21" (prop) nil nil)) nil))
nil)
("22" (inst -2 "x!1" "x!2") (("22" (prop) nil nil))
nil)
("23" (inst -4 "x!1" "x!2")
(("23" (inst -3 "x!2" "x!1" "y!2")
(("23" (prop) nil nil)) nil))
nil)
("24" (inst -4 "x!1" "x!2")
(("24" (inst -3 "x!2" "x!1" "y!2")
(("24" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(Los 0
(Los-1 nil 3328276414
("" (skolem!)
(("" (lemma "los_graphic")
(("" (inst -1 "(lambda x,y:P!1(x,y)&P!1(y,x))" "Q!1")
(("" (skosimp*)
(("" (bddsimp)
(("1" (inst -3 "x!1" "y!1") (("1" (prop) nil nil)) nil)
("2" (inst -3 "x!2" "y!2") nil nil)
("3" (skolem! 1)
(("3" (inst-cp -4 "x!3" "y!3")
(("3" (inst -4 "y!3" "x!3")
(("3" (inst -2 "y!3" "x!3") (("3" (prop) nil nil))
nil))
nil))
nil))
nil)
("4" (skolem! 1) (("4" (prop) nil nil)) nil)
("5" (skolem! 1)
(("5" (prop)
(("1" (inst -7 "x!3" "y!3" "z!1")
(("1" (prop) nil nil)) nil)
("2" (inst -7 "z!1" "y!3" "x!3")
(("2" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((los_graphic formula-decl nil los_graph nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil los_graph nil))
shostak)))
¤ Dauer der Verarbeitung: 0.20 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.
|
