Quelle csequence_merge_split.prf
Sprache: unbekannt
|
|
(csequence_merge_split
(merge_split_eta 0
(merge_split_eta-1 nil 3513713060
("" (skolem!)
(("" (lemma "coinduction")
((""
(inst - "LAMBDA cseq1, cseq2: cseq1 = merge(split(cseq2))"
"merge(split(cseq!1))" "cseq!1")
(("" (delete 2)
(("" (expand "bisimulation?")
(("" (skosimp)
(("" (replace -1)
(("" (hide -1)
(("" (smash)
(("1" (lemma "merge_empty")
(("1" (inst - "split(y!1)`1" "split(y!1)`2")
(("1" (ground)
(("1" (rewrite "split_empty_left") nil nil))
nil))
nil))
nil)
("2" (use "split_empty_right")
(("2" (use "split_empty_left")
(("2" (assert)
(("2" (lemma "merge_nonempty")
(("2"
(inst - "split(y!1)`1" "split(y!1)`2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (lemma "merge_rest")
(("3" (inst - "split(y!1)`1" "split(y!1)`2")
(("3" (assert)
(("3" (lift-if)
(("3" (ground)
(("1"
(use "split_rest_swap_left")
(("1"
(use "split_rest_swap_right")
(("1" (assert) nil nil))
nil))
nil)
("2"
(use "split_empty_left")
(("2"
(assert)
(("2"
(use "split_empty_right")
(("2"
(assert)
(("2"
(use "merge_nonempty")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (lemma "merge_first")
(("4" (inst - "split(y!1)`1" "split(y!1)`2")
(("4" (assert)
(("4" (lift-if)
(("4" (ground)
(("1"
(rewrite "split_first_left")
(("1" (assert) nil nil))
nil)
("2"
(use "split_empty_left")
(("2"
(assert)
(("2"
(use "split_empty_right")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil csequence_merge_split nil)
(coinduction formula-decl nil csequence_codt nil)
(merge_first formula-decl nil csequence_merge nil)
(split_first_left formula-decl nil csequence_split nil)
(merge_rest formula-decl nil csequence_merge nil)
(split_rest_swap_right formula-decl nil csequence_split nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(split_rest_swap_left formula-decl nil csequence_split nil)
(split_empty_right formula-decl nil csequence_split nil)
(merge_nonempty formula-decl nil csequence_merge nil)
(merge_empty formula-decl nil csequence_merge nil)
(split_empty_left formula-decl nil csequence_split nil)
(split const-decl "[csequence, csequence]" csequence_split nil)
(merge const-decl "csequence" csequence_merge nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bisimulation? adt-def-decl "boolean" csequence_codt nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil))
shostak))
(split_merge_eta 0
(split_merge_eta-1 nil 3513713264
("" (skosimp)
(("" (decompose-equality)
(("1" (lemma "coinduction")
(("1"
(inst -
"LAMBDA cseq, cseq1: EXISTS cseq2: length_eq(cseq1, cseq2) AND cseq = split(merge(cseq1, cseq2))`1"
"split(merge(cseq1!1, cseq2!1))`1" "cseq1!1")
(("1" (assert) (("1" (inst + "cseq2!1") nil nil)) nil)
("2" (delete -1 2)
(("2" (expand "bisimulation?")
(("2" (skosimp*)
(("2" (replace -2)
(("2" (hide -2)
(("2" (smash)
(("1" (rewrite "split_empty_left")
(("1" (rewrite "merge_empty") nil nil)) nil)
("2" (rewrite "split_nonempty_left")
(("2" (rewrite "merge_nonempty")
(("2" (rewrite "length_nonempty?_rew")
(("2" (rewrite "length_empty?_rew")
(("2"
(expand "length_eq")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst + "rest(cseq2!2)")
(("1" (expand "length_eq")
(("1" (expand "is_finite" -)
(("1" (expand "length" -)
(("1"
(smash)
(("1"
(rewrite "split_nonempty_left")
(("1"
(rewrite "merge_nonempty")
nil
nil))
nil)
("2"
(rewrite "split_nonempty_left")
(("2"
(rewrite "merge_nonempty")
nil
nil))
nil)
("3"
(case
"nonempty?(merge(y!1, cseq2!2))")
(("1"
(rewrite "split_rest_left")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(expand*
"merge"
"merge_struct"
"coreduce"
"coreduce")
nil
nil)
("2"
(lemma "merge_rest")
(("2"
(inst-cp - "y!1" "cseq2!2")
(("2"
(assert)
(("2"
(inst
-
"cseq2!2"
"rest(y!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "split_nonempty_left")
nil
nil))
nil)
("4"
(use "split_nonempty_left")
(("4"
(assert)
(("4"
(rewrite "split_rest_left")
(("4"
(lift-if)
(("4"
(ground)
(("1"
(expand*
"merge"
"merge_struct"
"coreduce"
"coreduce")
nil
nil)
("2"
(lemma "merge_rest")
(("2"
(inst-cp
-
"y!1"
"cseq2!2")
(("2"
(assert)
(("2"
(inst
-
"cseq2!2"
"rest(y!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "split_nonempty_left")
(("2" (rewrite "merge_nonempty")
(("2" (assert)
(("2"
(rewrite "length_nonempty?_rew")
(("2"
(rewrite "length_nonempty?_rew")
(("2"
(expand "length_eq")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (rewrite "split_nonempty_left")
(("4" (rewrite "split_first_left")
(("4" (rewrite "merge_first")
(("4" (lift-if)
(("4"
(ground)
(("4"
(expand "length_eq")
(("4"
(ground)
(("1"
(use
"infinite_csequence_is_nonempty")
nil
nil)
("2"
(expand "length")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "coinduction")
(("2"
(inst -
"LAMBDA cseq, cseq2: EXISTS cseq1: length_eq(cseq1, cseq2) AND cseq = split(merge(cseq1, cseq2))`2"
"split(merge(cseq1!1, cseq2!1))`2" "cseq2!1")
(("1" (assert) (("1" (inst + "cseq1!1") nil nil)) nil)
("2" (delete -1 2)
(("2" (expand "bisimulation?")
(("2" (skosimp*)
(("2" (replace -2)
(("2" (hide -2)
(("2" (smash)
(("1" (rewrite "split_empty_right")
(("1" (rewrite "merge_empty")
(("1"
(expand* "merge" "merge_struct" "coreduce"
"coreduce")
(("1" (reduce)
(("1"
(rewrite "length_empty?_rew")
(("1"
(rewrite "length_empty?_rew")
(("1"
(rewrite "length_nonempty?_rew")
(("1"
(expand "length_eq")
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "split_nonempty_right")
(("2" (flatten)
(("2" (rewrite "merge_nonempty")
(("2" (hide -3)
(("2"
(rewrite "length_nonempty?_rew")
(("2"
(rewrite "length_empty?_rew")
(("2"
(expand "length_eq")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (rewrite "split_nonempty_right")
(("3" (flatten)
(("3" (inst + "rest(cseq1!2)")
(("1" (split)
(("1"
(expand "length_eq")
(("1"
(expand "is_finite" -)
(("1"
(expand "length" -)
(("1" (reduce) nil nil))
nil))
nil))
nil)
("2"
(rewrite "split_rest_right")
(("2"
(lemma "merge_rest")
(("2"
(inst-cp - "cseq1!2" "y!1")
(("2"
(assert)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(replace -2)
(("1"
(inst
-
"y!1"
"rest(cseq1!2)")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(hide
-1
-3
-5
-6
2)
(("1"
(rewrite
"length_nonempty?_rew")
(("1"
(rewrite
"length_nonempty?_rew")
(("1"
(expand
"length_eq")
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"merge_empty_left"
-5)
(("2"
(hide -1 -4 2)
(("2"
(rewrite
"length_nonempty?_rew")
(("2"
(rewrite
"length_nonempty?_rew")
(("2"
(expand
"length_eq")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "merge_nonempty")
(("2"
(assert)
(("2"
(hide -3)
(("2"
(rewrite "length_nonempty?_rew")
(("2"
(rewrite "length_nonempty?_rew")
(("2"
(expand "length_eq")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (rewrite "split_nonempty_right")
(("4" (flatten)
(("4" (rewrite "split_first_right")
(("4" (assert)
(("4"
(rewrite "merge_rest")
(("4"
(rewrite "merge_nonempty")
(("4"
(lift-if)
(("4"
(ground)
(("1"
(rewrite "merge_first")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(hide -2 -3 -4 2)
(("1"
(rewrite
"length_nonempty?_rew")
(("1"
(rewrite
"length_nonempty?_rew")
(("1"
(expand
"length_eq")
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "merge_first")
nil
nil)
("3"
(hide -1 2 3)
(("3"
(rewrite
"length_nonempty?_rew")
(("3"
(rewrite
"length_nonempty?_rew")
(("3"
(expand "length_eq")
(("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((split const-decl "[csequence, csequence]" csequence_split nil)
(merge const-decl "csequence" csequence_merge nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_merge_split nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(length_eq const-decl "bool" csequence_length_comp nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bisimulation? adt-def-decl "boolean" csequence_codt nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(merge_empty formula-decl nil csequence_merge nil)
(split_empty_left formula-decl nil csequence_split nil)
(merge_nonempty formula-decl nil csequence_merge nil)
(length_empty?_rew formula-decl nil csequence_length nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(length_nonempty?_rew formula-decl nil csequence_length nil)
(split_nonempty_left formula-decl nil csequence_split nil)
(length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(merge_rest formula-decl nil csequence_merge nil)
(merge_struct const-decl "csequence_struct" csequence_merge nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(split_rest_left formula-decl nil csequence_split nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(is_finite inductive-decl "bool" csequence_props nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(cseq2!2 skolem-const-decl "csequence[T]" csequence_merge_split
nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(split_first_left formula-decl nil csequence_split nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(infinite_csequence type-eq-decl nil csequence_props nil)
(infinite_csequence_is_nonempty judgement-tcc nil csequence_props
nil)
(merge_first formula-decl nil csequence_merge nil)
(coinduction formula-decl nil csequence_codt nil)
(split_empty_right formula-decl nil csequence_split nil)
(split_nonempty_right formula-decl nil csequence_split nil)
(merge_empty_left formula-decl nil csequence_merge nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(empty_csequence nonempty-type-eq-decl nil csequence_props nil)
(split_rest_right formula-decl nil csequence_split nil)
(cseq1!2 skolem-const-decl "csequence[T]" csequence_merge_split
nil)
(split_first_right formula-decl nil csequence_split nil))
shostak)))
[ zur Elbe Produktseite wechseln0.16Quellennavigators
Analyse erneut starten
]
|
2026-03-28
|
