Quelle csequence_rest.prf
Sprache: unbekannt
|
|
(csequence_rest
(rest_finite 0
(rest_finite-1 nil 3513477709
("" (skolem-typepred)
(("" (expand "is_finite" -) (("" (propax) nil nil)) nil)) nil)
((nonempty_finite_csequence type-eq-decl nil csequence_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(finite_csequence nonempty-type-eq-decl nil csequence_props nil)
(is_finite inductive-decl "bool" csequence_props nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_rest nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(rest_infinite 0
(rest_infinite-1 nil 3513477709
("" (skolem-typepred)
(("" (expand "is_finite" +) (("" (flatten) nil nil)) nil)) nil)
((infinite_csequence type-eq-decl nil csequence_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(is_finite inductive-decl "bool" csequence_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_rest nil))
nil))
(rest_empty_add 0
(rest_empty_add-1 nil 3513477777
("" (skolem!)
(("" (prop)
(("1" (inst + "first(nseq!1)")
(("1" (decompose-equality) nil nil)) nil)
("2" (skolem!) (("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((csequence_add_extensionality formula-decl nil csequence_codt nil)
(empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
(empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
nil)
(add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
csequence_codt nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_rest nil))
shostak))
(rest_empty 0
(rest_empty-1 nil 3513477823
("" (skolem!)
(("" (expand* "is_finite" "is_finite" "length" "length")
(("" (ground) nil nil)) nil))
nil)
((length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
(is_finite inductive-decl "bool" csequence_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak))
(rest_nonempty 0
(rest_nonempty-1 nil 3513477866
("" (skolem!)
(("" (use "rest_empty")
(("" (lemma "length_empty?_rew" ("cseq" "nseq!1"))
(("" (ground) nil nil)) nil))
nil))
nil)
((rest_empty formula-decl nil csequence_rest nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil)
(T formal-type-decl nil csequence_rest nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(length_empty?_rew formula-decl nil csequence_length nil))
shostak))
(rest_first_TCC1 0
(rest_first_TCC1-1 nil 3513477709
("" (skosimp) (("" (expand* "index?" "index?") nil nil)) nil)
((index? def-decl "bool" csequence_nth nil)) nil))
(rest_first 0
(rest_first-1 nil 3513477945
("" (skosimp) (("" (expand* "nth" "nth") nil nil)) nil)
((nth def-decl "T" csequence_nth nil)) shostak))
(rest_length 0
(rest_length-1 nil 3513477958
("" (expand "length" 1 2) (("" (propax) nil nil)) nil)
((length def-decl "{n | has_length(fseq, n)}" csequence_length nil))
shostak))
(rest_index 0
(rest_index-1 nil 3513477977
("" (expand "index?" 1 2) (("" (propax) nil nil)) nil)
((index? def-decl "bool" csequence_nth nil)) shostak))
(rest_nth_TCC1 0
(rest_nth_TCC1-1 nil 3513477709
("" (expand "index?") (("" (propax) nil nil)) nil)
((index? def-decl "bool" csequence_nth nil)) nil))
(rest_nth 0
(rest_nth-1 nil 3513478014
("" (expand "nth" 1 2) (("" (propax) nil nil)) nil)
((nth def-decl "T" csequence_nth nil)) shostak))
(rest_some 0
(rest_some-1 nil 3513478020
("" (expand "some" 1 1) (("" (propax) nil nil)) nil)
((some inductive-decl "boolean" csequence_codt nil)) shostak))
(rest_every 0
(rest_every-1 nil 3513478028
("" (expand "every" 1 1) (("" (propax) nil nil)) nil)
((every coinductive-decl "boolean" csequence_codt nil)) shostak)))
[ zur Elbe Produktseite wechseln0.22Quellennavigators
Analyse erneut starten
]
|
2026-03-28
|
