Quelle save.prf
Sprache: Lisp
(fseq2setnil 3440769713 3440772507"" (lemma "bij_exists" )"" "(LAMBDA (S: finite_set[T]): ") "" (skosimp*)"" (inst?)"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil numbers 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" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil naturalnumbers nil )"bool" functions nil )"bool" sets nil )"(p)" sets nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )nil fseq2set nil ))nil ))nil 3440770452 3440772507"" "(LAMBDA (S: non_empty_finite_set[T]): inverse(bij(S)))" )"" (skosimp*)"" (typepred "S!1" )"" (expand "empty?" )"" (expand "member" )"" (hide -1) (("" (skosimp*) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil fseq2set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil ))nil ))nil 3440771597 3440772897"" (skosimp*)"" (expand "ibij" )"" (lemma "comp_inverse_right[(S!1),below(card(S!1))]" )"" (inst?) nil nil )) nil ))nil ))nil )"{f: [below(card(S)) -> (S)] | bijective?(f)}" nil )"{f: [(S) -> below(card(S))] | bijective?(f)}" nil )"bool" functions nil )nil function_inverse nil )nil fseq2set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )nil numbers 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" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil naturalnumbers nil ))nil 3440771016 3440772897"" (skosimp*)"" (assert )"" (expand "ibij" )"" (assert )"" (lemma "bijective_inverse[(S!1),below(card(S!1))]" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(bijective?[R, D])" function_inverse nil )"{x: D | f(x) = y}" nil )"{f: [(S) -> below(card(S))] | bijective?(f)}" nil )"bool" functions nil )nil function_inverse nil )nil fseq2set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )nil numbers 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" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil naturalnumbers nil )"{f: [below(card(S)) -> (S)] | bijective?(f)}" nil ))nil 3282912778 3440772507"" (skosimp*)"" (assert )"" (lemma "is_finite_surj" )"" (inst?)"" (assert )"" (hide 2)"" "length(fs!1)" "(LAMBDA (ii: below(length(fs!1))): ") "1" (expand "surjective?" )"1" (skosimp*)"1" (typepred "y!1" )"1" (skosimp*)"1" (assert )"1" (inst?)"1" (assert )"1" expand "finseq_appl" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (expand "finseq_appl" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil numbers 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" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )nil nat_types nil )nil finite_sets nil )nil fseq2set nil ))nil 3282915134 3440772897"" (skosimp*)"" (expand "finseq_appl" )"" (assert )"" (expand "seq2set" )"" (expand "finseq_appl" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil fseq2set nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"finite_set[T]" fseq2set nil ))"" 3283086594 3440772898"" (skosimp*)"" (typepred "seq2set(fs!1)" )"" (typepred "length(fs!1)" )"" (expand "seq2set" )"" (expand "finseq_appl" )"" (lemma "seq2set_lem" )"" (inst?)"" (assert )"" (expand "seq2set" )"" (expand "finseq_appl" )"" (lemma "Card_injection" )"" (expand "injective?" )"" "{s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}" "length(fs!1)" )"" (assert )"" "LAMBDA (f: {s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}): min( {kk: below(length(fs!1)) | fs!1`seq(kk) = f})" )"1" "1" (assert ) nil nil ))nil )"2" "2" expand "nonempty?" )"2" "f!1" )"2" "2" expand "empty?" )"2" expand "member" )"2" "kk!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"finite_set[T]" fseq2set nil )nil finite_sets nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil fseq2set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"bool" sets nil )"bool" sets nil )nil nat_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil finite_sets nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil fseq2set nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil ))nil 3282918983 3283085680"" (skosimp*)"" (expand "seq2set" )"" (expand "finseq_appl" )"" (lemma "seq2set_lem" )"" (inst?)"" (assert )"" (expand "seq2set" )"" (expand "finseq_appl" )"" (lemma "Card_injection" )"" (expand "injective?" )"" "{s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}" "length(fs!1)" )"1" (assert )"1" (hide 2)"1" "LAMBDA (s: {s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}): min( {kk: below(length(fs!1)) | fs!1`seq(kk) = s})" )"1" "1" "min({kk: below(length(fs!1)) | fs!1`seq(kk) = x1!1})" )"1" "min({kk: below(length(fs!1)) | fs!1`seq(kk) = x2!1})" )"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "2" "2" "2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil 5068986 8940 t shostak))nil 3282912778 3440772507"" (skosimp*)"" (expand "empty?" )"" (expand "member" )"" (expand "seq2set" )"" (inst - "ne_fs!1`seq(0)" )"" (inst + "0" )"" (assert )"" (expand "finseq_appl" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"finite_set[T]" fseq2set nil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )nil fseq2set nil )"bool" sets nil ))"" 3283271310 3440772898"" (skosimp*)"" (typepred "seq2set(ne_fs!1)" )"" (typepred "ne_fs!1" )"" (split)"1" (typepred "min(ne_fs!1)" )"1" (expand "seq2set" )"1" (assert )"1" (skosimp*)"1" (expand "finseq_appl" )"1" (inst?)"1" (lemma "seq2set_lem" )"1" (inst?)"1" (expand "seq2set" )"1" (expand "finseq_appl" )"1" "1" "min_seq_lem" )"1" "min[T, <=]({s: T | EXISTS (kk: below(length(ne_fs!1))): ne_fs!1`seq(kk) = s})" )"1" replace -1)"1" "mm" )"1" "1" case "mm <= min(ne_fs!1)" )"1" assert )"1" case "min(ne_fs!1) <= mm" )"1" assert )"1" "<=" )"1" expand "total_order?" )"1" "1" expand "dichotomous?" )"1" expand "partial_order?" )"1" expand "antisymmetric?" )"1" "1" "mm" "min(ne_fs!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "<=" )"2" expand "total_order?" )"2" expand "dichotomous?" )"2" expand "partial_order?" )"2" "2" expand "antisymmetric?" )"2" "ne_fs!1" "kk!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "empty?" )"2" expand "member" )"2" "2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "max(ne_fs!1)" )"2" (expand "seq2set" )"2" (assert )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "seq2set_lem" )"2" (inst?)"2" (expand "seq2set" )"2" (expand "finseq_appl" )"2" "2" "max_seq_lem" )"2" " max[T, <=] ") "1" replace -1)"1" "mm" )"1" "1" case "mm <= max(ne_fs!1)" )"1" assert )"1" case "max(ne_fs!1) <= mm" )"1" assert )"1" "<=" )"1" expand "total_order?" )"1" "1" expand "dichotomous?" )"1" expand "partial_order?" )"1" expand "antisymmetric?" )"1" "1" "mm" "max(ne_fs!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "<=" )"2" expand "total_order?" )"2" expand "dichotomous?" )"2" expand "partial_order?" )"2" "2" expand "antisymmetric?" )"2" expand "preorder?" )"2" expand "reflexive?" )"2" expand "transitive?" )"2" "2" "max_lem" )"2" "1" replace "1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" expand "empty?" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ne_fs!1" "kk!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "empty?" )"2" "2" expand "member" )"2" "jj!1" )"2" 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 fseqs "structures/" )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"finite_set[T]" fseq2set nil )nil finite_sets nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil fseq2set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil fseq2set nil )"bool" sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )min const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" "finite_sets/" )"bool" orders nil )"bool" relations nil )"bool" orders nil )"bool" sets nil )nil min_fseq "structures/" )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil defined_types nil )"bool" orders nil )"(total_order?[T])" fseq2set nil )nil min_fseq "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )min const-decl "{t: T | AND " min_fseq "structures/" )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"bool" orders nil )"bool" relations nil )nil finite_sets_minmax "finite_sets/" )"bool" relations nil )nil max_fseq "structures/" )nil max_fseq "structures/" )max const-decl "{t: T | AND " max_fseq "structures/" ))nil 3283098598 3283255060"" (skosimp*)"" (typepred "seq2set(ne_fs!1)" )"" (typepred "ne_fs!1" )"" (split)"1" (typepred "min(ne_fs!1)" )"1" (expand "seq2set" )"1" (assert )"1" (skosimp*)"1" (expand "finseq_appl" )"1" (inst?)"1" (lemma "seq2set_lem" )"1" (inst?)"1" (expand "seq2set" )"1" (expand "finseq_appl" )"1" "1" "min_seq_lem" )"1" "1" "min[T, <=]({s: T | EXISTS (kk: below(length(ne_fs!1))): ne_fs!1`seq(kk) = s})" )"1" replace -1)"1" "mm" )"1" "1" case "mm <= min(ne_fs!1)" )"1" assert )"1" case "min(ne_fs!1) <= mm" )"1" assert )"1" "<=" )"1" expand "total_order?" )"1" "1" expand "dichotomous?" )"1" expand "partial_order?" )"1" expand "antisymmetric?" )"1" "1" "mm" "min(ne_fs!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil )nil 3562301 6490 t shostak))nil 3282912778 3440772507"" (skosimp*)"" (expand "nonempty?" )"" (lemma "minmax_seq2set_TCC1" )"" (inst?) (("" (assert ) (("" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil fseqs "structures/" )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil fseq2set nil )nil naturalnumbers nil )nil fseq2set nil ))nil 3440770694 3440772890"" "(LAMBDA (S: finite_set[T]): AND AND AND ") "" (skosimp*)"" (name "F" "ibij(S!1)" )"1" (typepred "ibij(S!1)" )"1" (replace -2 * lr)"1" (hide -2)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" "(# length := card(S!1), LAMBDA (i: nat): IF i < card(S!1) THEN F(i)") "1" (prop)"1" (ground) nil nil )"2" (skosimp*)"2" (inst + "bij(S!1)(x!1)" )"2" (lift-if)"2" "2" expand "F" )"2" (rewrite "ibij_bij" ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (lift-if)"3" (ground)"3" expand "bijective?" )"3" "3" expand "injective?" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (lemma "empty_card" )"2" (inst?)"2" (assert )"2" (replace -1 * lr)"2" (hide -1)"2" (hide -1)"2" (expand "empty?" )"2" (expand "member" )"2" "(# length := 0, seq := (LAMBDA (i: nat): default) #)" )"2" (prop)"1" (skosimp*) nil nil )"2" "2" assert )"2" "2" expand "empty?" )"2" expand "member" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" fseqs "structures/" )"bool" functions nil )nil fseq2set nil )"(strict_total_order?[real])" real_props nil )"{f: [(S) -> below(card(S))] | bijective?(f)}" nil )"(total_order?[real])" nil )"bool" sets nil )"{f: [below(card(S)) -> (S)] | bijective?(f)}" nil )"bool" functions nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"(p)" sets nil )"bool" sets nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil fseq2set nil ))nil )nil 3280842302 3440770670"" "(LAMBDA (S: finite_set[T]): AND AND AND ") "" (skosimp*)"" (name "F" "bij(S!1)" )"" (typepred "bij(S!1)" )"" (replace -2 * lr)"" (hide -2)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" ) (("" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )) 116 80 tnil 3281098906 3440772898"" (induct "S" 1 "finite_set_induction_rest[T]" )"1" (expand "set2seq" )"1" (expand "fseq1" )"1" (expand "o " )"1" (ground)"1" (case "empty?[T](emptyset[T])" )"1" (assert )"1" (rewrite "card_emptyset[T]" )"1" (assert )"1" (expand "empty_seq" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "set2seq" 1)"2" (expand "o " )"2" (expand "fseq1" )"2" (assert )"2" (rewrite "card_rest" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"finite_set[T]" fseq2set nil )"finite_set" finite_sets nil )"finite_set[T]" fseq2set nil )nil finite_sets_inductions"finite_sets/" )nil fseq2set nil )"{fs: fseq[T] | AND AND AND " fseq2set nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil numbers nil )nil defined_types nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil 3280846807 3440772898"" (skosimp*)"" (assert )"" (skosimp*)"" (typepred "set2seq(S!1)" )"" (inst?) (("" (flatten) nil nil )) nil )) nil ))nil ))nil ))nil )nil 28 20 t shostak))nil 3410632995 3440772939"" (skosimp*)"" (assert )"" (flatten)"" (typepred "set2seq(S!1)" )"" (inst -3 "x!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"{fs: fseq[T] | AND AND AND " fseq2set nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil fseq2set nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil )nil 3281099741 3410632694"" (auto-rewrite!! "finseq_appl" )"" (expand "finseq_appl" )"" (induct "S" 1 "finite_set_induction_rest[T]" )"1" (skosimp*)"1" (hide 1)"1" (expand "emptyset" ) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (expand "set2seq" 1)"2" (expand "o " 1)"2" (expand "#" )"2" (assert )"2" (inst?)"2" (assert )"2" (lemma "choose_rest_or[T]" )"2" (inst?)"2" (inst?)"2" (expand "member" )"2" "1" assert )"1" "1" "ii!1" )"1" "ii!1+1" )"1" (assert ) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "0" )"1" (assert ) nil nil )"2" expand "set2seq" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sets_inductions"finite_sets/" ))nil 3440772982 3440772986"" (skosimp*) (("" (assert ) nil nil )) nil ) unchecked nil 4219 30 tnil 3281118238 3440772508"" (skosimp*) (("" (assert ) nil nil )) nil ) unchecked"(strict_total_order?[real])" real_props nil )nil fseq2set nil ))nil 3281118238 3440772508"" (skosimp*)"" (lemma "card_empty?[T]" )"" (inst?) (("" (assert ) (("" (ground) nil nil )) nil )) nil ))nil ))nil )nil fseq2set nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil 3281118135 3440772899"" (assert )"" (skosimp*)"" (prop)"1" (typepred "min(set2seq(S!1))" )"1" (skosimp*)"1" (replace -2 * rl)"1" (typepred "min[T, <=](S!1)" )"1" (lemma "set2seq_lem" )"1" (inst?)"1" (assert )"1" (inst - "jj!1" )"1" (inst - "set2seq(S!1)`seq(jj!1)" )"1" (assert )"1" (assert )"1" "set2seq_exists" )"1" "S!1" "min[T, <=](S!1)" )"1" assert )"1" "1" "ii!1" )"1" assert )"1" "<=" )"1" expand "total_order?" )"1" expand "partial_order?" )"1" expand "preorder?" )"1" expand "transitive?" )"1" "1" expand "reflexive?" )"1" expand "antisymmetric?" )"1" "min[T, <=](S!1)" "set2seq(S!1)`seq(jj!1)" )"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 ))nil ))nil ))nil ))nil )"2" (typepred "max(set2seq(S!1))" )"2" (skosimp*)"2" (typepred " max[T, <=](S!1)" )"2" (lemma "set2seq_lem" )"2" (inst?)"2" (assert )"2" (inst?)"2" (inst -3 "set2seq(S!1)`seq(jj!1)" )"2" (assert )"2" (lemma "set2seq_exists" )"2" (inst - "S!1" "max[T, <=](S!1)" )"2" assert )"2" "2" "ii!1" )"2" assert )"2" "<=" )"2" expand "total_order?" )"2" expand "partial_order?" )"2" expand "antisymmetric?" )"2" expand "preorder?" )"2" "2" "max[T, <=](S!1)" "set2seq(S!1)`seq(jj!1)" )"2" 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 )max const-decl "{t: T | AND " max_fseq "structures/" )nil max_fseq "structures/" )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )min const-decl "{t: T | AND " min_fseq "structures/" )nil fseqs "structures/" )"bool" reals nil )nil min_fseq "structures/" )"(total_order?[T])" fseq2set nil )"bool" orders nil )nil defined_types nil )"{fs: fseq[T] | AND AND AND " fseq2set nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil fseq2set nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil fseq2set nil )"(strict_total_order?[real])" real_props nil )"bool" orders nil )"bool" relations nil )"bool" relations nil )"bool" relations nil )"bool" orders nil )nil fseq2set nil )min const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" "finite_sets/" )nil finite_sets nil )"bool" sets nil ))nil ))nil 3410633296 3440774017"" (skosimp*) (("" (assert ) nil nil )) nil ) proved nil 5622 30 tnil )nil 3281100425 3410632695"" (induct "S" 1 "finite_set_induction_rest[T]" )"1" (assert ) nil nil )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (auto-rewrite!! "finseq_appl" )"2" (typepred "ii!1" )"2" (typepred "jj!1" )"2" (assert )"2" (rewrite "card_emptyset" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand "finseq_appl" )"3" (typepred "ii!1" )"3" (typepred "jj!1" )"3" (assert )"3" (expand "set2seq" -4)"3" (expand "#" )"3" (expand "o" )"3" (case "ii!1 < 1" )"1" (assert )"1" (lemma "set2seq_lem" )"1" (inst?)"1" (assert )"1" "jj!1-1" )"1" expand "finseq_appl" )"1" assert )"1" "choose_not_member[T]" )"1" expand "member" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "jj!1 < 1" )"1" (assert )"1" (lemma "set2seq_lem" )"1" "1" assert )"1" "ii!1-1" )"1" expand "finseq_appl" )"1" "choose_not_member[T]" )"1" expand "member" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (inst -3 "ii!1-1" "jj!1-1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil finite_sets nil )nil sets_lemmas nil )"bool" sets nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )"fseq" fseqs "structures/" )nil finite_sets nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets_inductions"finite_sets/" )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil fseqs "structures/" )nil nat_types nil )nil naturalnumbers nil )nil defined_types nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.35 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
