(modulo_equivalencenil 3383390315"" (skeep)"" (expand * "diamond_property?" "confluent_m?" )"" (skeep)"" (copy -1)"" (inst -1 "x" "y" "z" )"" (typepred "Eq" )"" (expand "equivalence?" )"" (flatten)"" (prop)"1" (skolem * "u1" )"1" (flatten)"1" (expand "o" (-1 -2))"1" (skolem * "u2" )"1" (skolem * "u" )"1" "1" "1" expand "transitive?" -1)"1" "1" expand "symmetric?" -1)"1" "u" "u1" )"1" "u2" "u1" "u" )"1" assert )"1" "1" "y" "u" "w" )"1" "1" "v2" )"1" "1" expand "o" )"1" "v1" )"1" "v" )"1" "1" "1" expand "transitive?" "1" "1" expand "symmetric?" "1" "v" "v2" )"1" "v1" "v2" "v" )"1" assert )"1" "RTC(R)" )"1" expand "reflexive_transitive?" )"1" "1" expand "transitive?" "1" "z" "u" "v1" )"1" assert )"1" "1" expand "joinable_m?" )"1" "v1" "v" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" )"2" "u2" )"2" assert )nil nil ))nil ))nil )"3" expand "o" )"3" "w" )"3" expand "reflexive?" )"3" "w" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-6 1))"2" (expand "o" 1)"2" (inst 1 "x" )"2" (typepred "RTC(R)" )"2" (expand "reflexive_transitive?" )"2" "2" expand "reflexive?" )"2" "x" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 -5 1))"3" (expand "o" 1)"3" (inst 1 "z" )"3" (expand "reflexive?" )"3" (inst -1 "z" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" modulo_equivalence nil )"bool" ars_terminology nil )nil relations_closure nil )"bool" relations nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" relation_props nil )"bool" relations nil )"bool" modulo_equivalence nil )"reflexive_transitive" relations_closure nil )nil relations_closure nil )"bool" relations_closure nil )nil defined_types nil )"bool" relations nil )"bool" relations nil )nil modulo_equivalence nil ))nil 3383388017"" (skeep)"" (split)"1" (flatten)"1" (lemma "van_oostrom94" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (lemma "noetherian_induction" )"1" (inst?)"1" (expand "diamond_property?" )"1" (skeep)"1" "(LAMBDA (a: T): (FORALL (b, c: T):(RTC(R) o Eq)(a, b) AND (RTC(R) o Eq)(a, c) IMPLIES joinable_m?(R, Eq)(c, b)))" )"1" (split)"1" (inst -1 "x" "y" "z" )"1" assert )"1" expand "joinable_m?" )"1" "u" "v" ))"1" "1" "u" )"1" "1" expand "o" 1)"1" "v" )"1" "Eq" )"1" expand *"equivalence?" "symmetric?" )"1" "1" "u" "v" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" 1)"2" "u" )"2" "Eq" )"2" expand *"equivalence?" "reflexive?" )"2" "2" "u" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "a" )"2" "2" "2" "2" expand "o" (-2 -3))"2" "b2" )"2" "c2" )"2" "2" expand "RTC" (-2 -4))"2" expand "IUnion" "2" "i" )"2" "j" )"2" "i = 0" "1" "j = 0" "1" expand "iterate" )"1" replace "1" replace "1" "1" expand "joinable_m?" )"1" "c" "b" )"1" "RTC(R)" )"1" "Eq" )"1" expand "reflexive_transitive?" )"1" "1" "1" expand *"equivalence?" "transitive?" "reflexive?" "symmetric?" )"1" "1" "a" "c" )"1" "c" "a" "b" )"1" "1" "c" )"1" "b" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "iterate" "2" replace "2" "2" "2" "R" "R" "n" "j - 1" ))"1" assert )"1" "1" "(a, c2)" )"1" "1" expand "o" "1" "c1" )"1" "1" "iterate_RTC" )"1" "R" "j - 1" )"1" expand *"subset?" "member" )"1" "(c1, c2)" )"1" expand "locally_coherent?" )"1" "Eq" )"1" expand "equivalence?" )"1" "1" "a" "c1" "b" )"1" assert )"1" "1" expand "joinable_m?" )"1" "d1" "d2" ))"1" "1" "c1" )"1" "R_subset_TC" )"1" "1" expand *"subset?" "member" )"1" "(a, c1)" )"1" assert )"1" "d2" "c" )"1" "1" "r1" "r2" ))"1" "1" "RTC(R)" )"1" expand "reflexive_transitive?" )"1" "1" expand "transitive?" "1" "b" "d2" "r2" )"1" "r1" "r2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" "2" "d1" )"2" assert )nil nil ))nil ))nil )"3" expand "o" "3" "c2" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "R" "R" "n" "i - 1" ))"1" "1" "(a, b2)" )"1" "1" expand "o" "1" "b3" )"1" "1" "iterate_RTC" )"1" "R" "i - 1" )"1" expand *"subset?" "member" )"1" "(b3, b2)" )"1" assert )"1" "1" "j = 0" "1" expand "iterate" )"1" replace "1" expand "locally_coherent?" )"1" "Eq" )"1" expand "equivalence?" )"1" "1" "a" "b3" "c" )"1" assert )"1" "1" expand "joinable_m?" )"1" "d1" "d2" ))"1" "1" "b3" )"1" "R_subset_TC" )"1" "1" expand *"subset?" "member" )"1" "(a, b3)" )"1" assert )"1" "d2" "b" )"1" "1" "r1" "r2" ))"1" "1" "RTC(R)" )"1" expand "reflexive_transitive?" )"1" "1" expand "transitive?" "1" "c" "d2" "r2" )"1" expand "symmetric?" "1" "r1" "r2" )"1" "r2" "r1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" "2" "d1" )"2" assert )nil nil ))nil ))nil )"3" expand "o" "3" "b2" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "R" "R" "n" "j - 1" ))"1" assert )"1" "1" "(a, c2)" )"1" "1" expand "o" "1" "c1" )"1" "1" "iterate_RTC" )"1" "R" "j - 1" )"1" expand *"subset?" "member" )"1" "(c1, c2)" )"1" assert )"1" "1" expand "local_confluent_m?" )"1" "a" "c1" "b3" )"1" assert )"1" expand "joinable_m?" )"1" "d1" "d2" ))"1" "1" "1" "b3" )"1" "R_subset_TC" )"1" "1" expand *"subset?" "member" )"1" "(a, b3)" )"1" assert )"1" "b" "d1" )"1" "1" "d3" "d4" ))"1" "1" "c1" )"1" "R_subset_TC" )"1" "1" expand *"subset?" "member" )"1" "(a, c1)" )"1" assert )"1" "d4" "c" )"1" "1" "u1" "u2" ))"1" "1" "RTC(R)" )"1" expand "reflexive_transitive?" )"1" "1" expand "transitive?" "1" "b" "d4" "u2" )"1" "u1" "u2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" "2" "d3" )"2" "RTC(R)" )"2" expand "reflexive_transitive?" )"2" "2" expand "transitive?" "2" "c1" "d1" "d3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "o" "3" "c2" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" "2" "b2" )"2" assert )nil nil ))nil ))nil )"3" expand "o" "3" "d2" )"3" "Eq" )"3" expand *"equivalence?" "symmetric?" )"3" "3" "d1" "d2" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" expand *"confluent_m?" "local_confluent_m?" )"3" "R_subset_RTC" )"3" "3" "R_subset_RTC" )"3" "3" expand *"subset?" "member" )"3" "(x, y)" )"3" "(x, z)" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (split)"1" (hide -2)"1" (expand * "confluent_m?" "local_confluent_m?" )"1" (skeep)"1" (inst -3 "x" "x" "y" "z" )"1" (typepred "Eq" )"1" (expand "equivalence?" )"1" (flatten)"1" (expand "reflexive?" )"1" (inst?)"1" (lemma "R_subset_RTC" )"1" "R_subset_RTC" )"1" "1" "1" expand * "subset?" "member" )"1" "(x, y)" )"1" "(x, z)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (expand * "confluent_m?" "locally_coherent?" )"2" (typepred "Eq" )"2" (expand "equivalence?" )"2" (prop)"2" (skeep)"2" (inst -6 "x" "z" "y" "z" )"2" (lemma "R_subset_RTC" )"2" (inst?)"2" (expand * "subset?" "member" )"2" "(x, y)" )"2" assert )"2" "2" expand * "RTC" "IUnion" )"2" "0" )"2" expand "iterate" 1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil modulo_equivalence nil )nil noetherian nil )"bool" ars_terminology nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )"bool" relation_props nil )"bool" relations_closure nil )nil relations_closure nil )"reflexive_transitive" relations_closure nil )"bool" modulo_equivalence nil )"set[T]" indexed_sets nil )nil relations_closure nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )"bool" modulo_equivalence nil )"nat" modulo_equivalence nil )"bool" relations nil )"pred[[T, T]]" relation_iterate "orders/" )nil relation_iterate "orders/" )"int" integers nil )nil relations_closure nil )"bool" modulo_equivalence nil )"bool" sets nil )"bool" sets nil )nil relations_closure nil )"nat" modulo_equivalence nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" relations nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" relations nil )"bool" noetherian nil )nil noetherian nil )nil relations_closure nil )"bool" relations nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil modulo_equivalence nil )"bool" modulo_equivalence nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.52 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
