(csequence_map_compositionnil 3513552853"" (skolem!)"" (lemma "coinduction[T3]" )"" "LAMBDA (cseq1, cseq2: csequence[T3]): EXISTS (cseq: csequence[T1]): map[T2, T3](f23!1)(map[T1, T2](f12!1)(cseq)) = cseq1 AND map[T1, T3](f23!1 o f12!1)(cseq) = cseq2" "map[T2, T3](f23!1)(map[T1, T2](f12!1)(cseq!1))" "map[T1, T3](f23!1 o f12!1)(cseq!1)" )"1" (assert ) (("1" (inst + "cseq!1" ) nil nil )) nil )"2" (delete 2)"2" (expand "bisimulation?" )"2" (skosimp*)"2" (expand "map" -)"2" (expand "o" )"2" (smash)"1" (inst + "rest(cseq!2)" )"1" (decompose-equality)"1" (decompose-equality -3)"1" (assert ) nil nil )) nil ))nil ))nil )"2" (decompose-equality)"2" (decompose-equality -3)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil csequence_map_composition nil )nil csequence_codt nil )"[(nonempty?) -> csequence]" csequence_codtnil )"[csequence -> boolean]" nil )"[(nonempty?) -> T]" csequence_codt nil )"[[T, csequence] -> (nonempty?)]" nil )nil csequence_codt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" csequence_codt nil )nil csequence_map_composition nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil csequence_map_composition nil )"csequence[T1]" csequence_codt_map nil )"[T2 -> T3]" csequence_map_compositionnil )"[T1 -> T2]" csequence_map_compositionnil )"T3" function_props nil ))quality 100%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
