(isomorphism_symmetricnil 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" "d1!1" )"1" "1" "1" (ground) nil nil )"2" expand *"bijective?" "surjective?" )"2" "2" "d2!1" )nil nil ))nil ))nil ))nil )"2" expand *"bijective?" "surjective?" )"2" "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" "d1!1" )"2" "1" "1" (ground) nil nil )"2" expand *"bijective?" "surjective?" )"2" "2" "d2!1" )nil nil ))nil ))nil ))nil )"2" expand *"bijective?" "surjective?" )"2" "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 )"[T1 -> T2]" isomorphism_symmetric nil )"(bijective?[T2, T1])" isomorphism_symmetricnil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil isomorphism_symmetric nil )nil isomorphism_symmetric nil )"bool" functions nil )"bool" exists1 nil )"bool" functions nil )"bool" function_inverse_def nil )"[T2 -> T1]" isomorphism_symmetric nil )"(bijective?[T1, T2])" isomorphism_symmetricnil )nil function_inverse_def nil )nil function_inverse_defnil )"bool" isomorphism nil )"bool" isomorphism nil ))quality 100%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
