| products/sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ln_exp_def.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.27 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 |
