|
(isomorphism_symmetric
(isomorphism_symmetric 0
(isomorphism_symmetric-1 nil 3315073017
("" (expand* "isomorphic?" "isomorphism?" "symmetric?")
(("" (skolem!)
(("" (prop)
(("1" (skolem-typepred)
(("1" (use "bijective_inverse_exists[T1, T2]")
(("1" (expand "exists1")
(("1" (flatten)
(("1" (skolem!)
(("1" (use "bij_inv_is_bij_alt[T1, T2]")
(("1" (inst + "x!1")
(("1" (skolem!)
(("1" (inst - "x!1(d1!1)" "x!1(d2!1)")
(("1" (expand "inverse?")
(("1" (inst-cp - "d2!1")
(("1"
(inst - "d1!1")
(("1"
(split)
(("1"
(split)
(("1" (ground) nil nil)
("2"
(expand*
"bijective?"
"surjective?")
(("2"
(flatten)
(("2"
(inst -6 "d2!1")
nil
nil))
nil))
nil))
nil)
("2"
(expand*
"bijective?"
"surjective?")
(("2"
(flatten)
(("2" (inst -6 "d1!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem-typepred)
(("2" (use "bijective_inverse_exists[T2, T1]")
(("2" (expand "exists1")
(("2" (flatten)
(("2" (skolem!)
(("2" (use "bij_inv_is_bij_alt[T2, T1]")
(("2" (inst + "x!1")
(("2" (skolem!)
(("2" (inst - "x!1(d1!1)" "x!1(d2!1)")
(("2" (expand "inverse?")
(("2" (inst-cp - "d2!1")
(("2"
(inst - "d1!1")
(("2"
(split)
(("1"
(split)
(("1" (ground) nil nil)
("2"
(expand*
"bijective?"
"surjective?")
(("2"
(flatten)
(("2"
(inst -6 "d2!1")
nil
nil))
nil))
nil))
nil)
("2"
(expand*
"bijective?"
"surjective?")
(("2"
(flatten)
(("2" (inst -6 "d1!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((x!1 skolem-const-decl "[T1 -> T2]" isomorphism_symmetric nil)
(f!1 skolem-const-decl "(bijective?[T2, T1])" isomorphism_symmetric
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T1 formal-type-decl nil isomorphism_symmetric nil)
(T2 formal-type-decl nil isomorphism_symmetric nil)
(bijective? const-decl "bool" functions nil)
(exists1 const-decl "bool" exists1 nil)
(surjective? const-decl "bool" functions nil)
(inverse? const-decl "bool" function_inverse_def nil)
(x!1 skolem-const-decl "[T2 -> T1]" isomorphism_symmetric nil)
(f!1 skolem-const-decl "(bijective?[T1, T2])" isomorphism_symmetric
nil)
(bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(isomorphic? const-decl "bool" isomorphism nil)
(isomorphism? const-decl "bool" isomorphism nil))
shostak)))
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
