Impressum robinsonunificationEF.prf
Interaktion und
(robinsonunificationEFnil 3522686037"" (lemma var_countable) (("" (propax) nil nil )) nil )nil robinsonunificationEF nil )) nil ))nil 3522686037"" (lemma var_nonempty) (("" (propax) nil nil )) nil )nil robinsonunificationEF nil )) nil ))nil 3522686037"" (lemma symbol_nonempty) (("" (propax) nil nil )) nil )nil robinsonunificationEF nil )) nil ))nil 3506350454"" (skosimp)"" (skosimp)"" (assert )"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers 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 )nil seq_extras "structures/" )nil positions nil )"[symbol -> nat]" robinsonunificationEFnil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"int" integers nil ))nil ))nil 3506350454"" (skosimp*)"" (lemma delete_is_position)"" (inst -1 p!1 s!1)"" (assert )"" (flatten) (("" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil positions nil )"int" integers nil )nil finite_sequences nil )nil seq_extras "structures/" )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3506350454"" (skosimp*)"" (lemma subterm_is_app)"" (inst -1 p!1 s!1)"" (assert )"" (flatten) (("" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil subterm nil )"int" integers nil )nil finite_sequences nil )nil seq_extras "structures/" )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3506350454"" (skosimp*)"" (hide -1 -3 -4)"" (replaces -1)"" (expand delete 2)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"finseq" seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil positions nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil seq_extras "structures/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3506350454"" (skosimp*)"" (lemma positions_of_arg)"" (inst -1 "subtermOF(s!1, p1!1)" "j!1 + i!1" )"1" (lemma pos_o_term)"1" (inst -1 "p1!1" "#(j!1 + i!1 + 1)" "s!1" )"1" (lemma delete_is_position)"1" (inst -1 p!1 s!1)"1" (lemma empty_0[posnat])"1" (inst -1 p!1)"1" (assert )"1" (hide-all-but (-2 3))"1" case "p1!1 o #(1 + i!1 + j!1) = add_last(p1!1, 1 + i!1 + j!1)" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred j!1)"2" (typepred "args(subtermOF(s!1, p1!1))" )"2" (replace -1 1)"2" (replace -6 1 rl)"2" (hide-all-but (-2 1)) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil subterm nil )nil positions nil )nil seq_extras "structures/" )"int" integers nil )"posint" nil )"finseq" finite_sequences nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )"posint" nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" robinsonunificationEF nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" robinsonunificationEF nil )nil naturalnumbers nil )"below(n!1 - i!1)" robinsonunificationEFnil )nil term_adt nil )"[term -> boolean]" term_adt nil )nil nat_types nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )"term[variable, symbol, arity]" nil )"position[variable, symbol, arity]" nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3506350454"" (skosimp*)"" (lemma positions_of_arg)"" (inst -1 "subtermOF(s!1, p1!1)" "j!1 + i!1" )"1" (lemma pos_o_term)"1" (inst -1 "p1!1" "#(j!1 + i!1 + 1)" "s!1" )"1" (lemma delete_is_position)"1" (inst -1 p!1 s!1)"1" (lemma empty_0[posnat])"1" (inst -1 p!1)"1" (assert )"1" (hide-all-but (-2 3))"1" case "p1!1 o #(1 + i!1 + j!1) = add_last(p1!1, 1 + i!1 + j!1)" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred j!1)"2" (typepred "args(subtermOF(s!1, p1!1))" )"2" (replace -1 1)"2" (replace -6 1 rl)"2" (hide-all-but (-2 1)) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil positions nil )nil positions nil )nil seq_extras "structures/" )"int" integers nil )"(total_order?[real])" nil )nil finite_sequences nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil subterm nil ))nil ))nil 3488040223"" (skosimp)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil )nil integers nil )"bool" reals nil )nil integers 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 )nil seq_extras "structures/" )"int" integers nil )"(total_order?[real])" nil )"positions" positions nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"[symbol -> nat]" robinsonunificationEFnil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil ))nil ))nil 3488040223"" (skosimp)"" (rewrite delete_is_position)"" (hide 3)"" (flatten) (("" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil )nil positions nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunificationEFnil )"int" integers nil )nil finite_sequences nil )nil seq_extras "structures/" ))nil ))nil 3488040223"" (skosimp*)"" (lemma "subterm_is_app" )"" (inst -1 p!1 s!1)"" (assert )"" (hide 3)"" (flatten) (("" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil subterm nil )"int" integers nil )nil finite_sequences nil )nil seq_extras "structures/" )"positions" positions nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3488040223"" (skosimp*) (("" (rewrite "empty_0" ) nil nil )) nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3496419653"" (skosimp)"" (name-replace "q!1" "delete(p!1, length(p!1) - 1)" :hide? nil )"1" (lemma empty_0[posnat])"1" (inst -1 p!1)"1" (assert )"1" (typepred "args(subtermOF(s!1, q!1))" )"1" (replace -1 3 rl)"1" (hide -1)"1" (lemma add_last_delete[posnat])"1" (inst -1 p!1)"1" (assert )"1" (replace -2 -1)"1" (lemma add_last_delete_is_o[posnat])"1" (inst -1 p!1)"1" assert )"1" expand finseq_appl)"1" replace -3 -1)"1" replace -2 -1 rl)"1" "1" "q!1" "#(p!1`seq(p!1`length - 1))" "s!1" )"1" assert )"1" expand positionsOF -1)"1" "1" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" expand *"3" "1" "1" nil nil ))nil )"2" "2" expand "2" expand "2" "2" expand "2" "2" expand "2" expand "2" "2" expand "2" expand "#" "2" expand "#" "2" "2" "2" case "p!1`seq(p!1`length - 1) = last(p!1)" )"1" assert )nil nil )"2" "2" 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 ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma empty_0[posnat])"2" (inst -1 p!1) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"finseq" seq_extras "structures/" )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"[term -> boolean]" term_adt nil )nil finite_sequences nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil positions nil )"term" subterm nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finite_sequence[T]" set2seq "structures/" )"posint" nil )"finseq" finite_sequences nil )"positions" positions nil )"bool" reals nil )nil IUnion_extra nil )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"finseq" seq_extras "structures/" )"positions" positions nil )"set" sets nil )"bool" sets nil )"set[T]" indexed_sets nil )nil subterm nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"odd_int" integers nil )nil seq_extras "structures/" ))nil ))nil 3496419653"" (skosimp*)"" (typepred "length(z!1`3)" )"" (case "length(z!1`3)=0" )"1" (rewrite "empty_0" ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"bool" reals 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 )"int" integers nil )"(total_order?[real])" nil )nil seq_extras "structures/" )nil finite_sequences nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3496419653"" (skosimp)"" (rewrite delete_is_position)"" (hide 3)"" (flatten) (("" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil )nil positions nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunificationEFnil )"int" integers nil )nil finite_sequences nil )nil seq_extras "structures/" ))nil ))nil 3496419653"" (skosimp*)"" (lemma "subterm_is_app" )"" (inst?)"" (assert )"" (prop) (("" (rewrite "empty_0" ) nil nil )) nil )) nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil subterm nil )"int" integers nil )nil seq_extras "structures/" )nil finite_sequences nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3496419653"" (skosimp)"" "q!1" "delete(z!1`3, length(z!1`3) - 1)" :hide?nil )"1" (lemma empty_0[posnat])"1" (inst -1 "z!1`3" )"1" (assert )"1" (typepred "args(subtermOF(z!1`1, q!1))" )"1" (replace -1 3 rl)"1" (hide -1)"1" (lemma add_last_delete[posnat])"1" (inst -1 "z!1`3" )"1" (assert )"1" (replace -2 -1)"1" (lemma add_last_delete_is_o[posnat])"1" (inst -1 "z!1`3" )"1" assert )"1" expand finseq_appl)"1" replace -3 -1)"1" replace -2 -1 rl)"1" "1" "q!1" "#(z!1`3`seq(z!1`3`length - 1))" "z!1`1" )"1" assert )"1" expand positionsOF -1)"1" "1" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" expand *"3" "1" "1" nil nil ))nil )"2" "2" expand "2" expand "2" "2" expand "2" "2" expand "2" expand "2" "2" expand "2" expand "#" "2" expand "#" "2" "2" "2" case "z!1`3`seq(z!1`3`length - 1) = last(z!1`3)" )"1" assert )nil nil )"2" "2" 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 ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma empty_0[posnat])"2" (inst -1 "z!1`3" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"finseq" seq_extras "structures/" )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil term_adt nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil seq_extras "structures/" ))nil ))nil 3496419653"" (skosimp)"" "q!1" "delete(z!1`3, length(z!1`3) - 1)" :hide?nil )"1" (lemma empty_0[posnat])"1" (inst -1 "z!1`3" )"1" (assert )"1" (typepred "args(subtermOF(z!1`1, q!1))" )"1" (replace -1 3 rl)"1" (hide -1)"1" (lemma add_last_delete[posnat])"1" (inst -1 "z!1`3" )"1" (assert )"1" (replace -2 -1)"1" (lemma add_last_delete_is_o[posnat])"1" (inst -1 "z!1`3" )"1" assert )"1" expand finseq_appl)"1" replace -3 -1)"1" replace -2 -1 rl)"1" "1" "q!1" "#(z!1`3`seq(z!1`3`length - 1))" "z!1`1" )"1" assert )"1" expand positionsOF -1)"1" "1" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" expand *"3" "1" "1" nil nil ))nil )"2" "2" expand "2" expand "2" "2" expand "2" "2" expand "2" expand "2" "2" expand "2" expand "#" "2" expand "#" "2" "2" "2" case "z!1`3`seq(z!1`3`length - 1) = last(z!1`3)" )"1" assert )nil nil )"2" "2" 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 ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma empty_0[posnat])"2" (inst -1 "z!1`3" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"finseq" seq_extras "structures/" )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil term_adt nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"term" subterm nil )nil positions nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finite_sequence[T]" set2seq "structures/" )"posint" nil )"finseq" finite_sequences nil )"positions" positions nil )"bool" reals nil )nil IUnion_extra nil )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"finseq" seq_extras "structures/" )"positions" positions nil )"set" sets nil )"bool" sets nil )"set[T]" indexed_sets nil )nil subterm nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"odd_int" integers nil )nil seq_extras "structures/" ))nil ))nil 3496419653"" (skosimp*)"" (replaces -1)"" (rewrite "delete_is_position" )"" (prop) (("" (rewrite "empty_0" ) nil nil )) nil )) nil ))nil ))nil )nil finite_sequences nil )nil seq_extras "structures/" )"int" integers nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"positions" positions nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil positions nil ))nil ))nil 3496419653"" (skosimp*)"" (lemma "subterm_is_app" )"" (inst?)"" (inst -1 "s!1" )"" (assert )"" (prop) (("" (rewrite "empty_0" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil subterm nil )nil finite_sequences nil )nil seq_extras "structures/" )"int" integers nil )"positions" positions nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3496419653"" (skosimp*)"" (replaces -1)"" (rewrite delete_is_position)"" (hide 3)"" (flatten) (("" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil ))nil )nil seq_extras "structures/" )nil finite_sequences nil )"int" integers nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"positions" positions nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil positions nil ))nil ))nil 3496419653"" (skosimp*)"" (lemma "subterm_is_app" )"" (inst?)"" (assert )"" (inst -1 "t!1" )"" (assert )"" (prop) (("" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil subterm nil )"int" integers nil )nil seq_extras "structures/" )nil finite_sequences nil )"positions" positions nil )nil positions nil )nil term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3496419653"" (skosimp*)"" (replace -2 -4 rl)"" (case "pi!1 = pi0!1 o #(last(p!1) + 1)" )"1" (lemma pos_o_term)"1" (inst -1 "pi0!1" "#(last(p!1) + 1)" "t!1" )"1" (assert )"1" (hide 3)"1" (split)"1" (lemma delete_is_position)"1" (inst -1 "p!1" "t!1" )"1" (assert )"1" (hide-all-but (1 3))"1" (lemma empty_0[posnat])"1" (inst -1 p!1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma pos_subterm_ax)"2" (inst -1 "pi0!1" "#(last(p!1) + 1)" "s!1" )"2" (assert )"2" (expand positionsOF 1)"2" (lift-if)"2" (ground)"1" "1" "1" assert )"1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "args(subtermOF(t!1, pi0!1))" "args(subtermOF(s!1, pi0!1))" )"2" replace -6 -2)"2" replace -1 -2 rl)"2" "2" replace -1 -2 rl)"2" "2" case "positionsOF(subtermOF(s!1, pi0!1)) = only_empty_seq" )"1" "1" "pi0!1" "#(1 + last(p!1))" "s!1" )"1" assert )nil nil ))nil ))nil )"2" "2" expand positionsOF)"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand union)"3" expand member)"3" "3" expand IUnion)"3" expand finseq_appl)"3" "last(p!1) + 1" )"1" expand catenate)"1" "1" "1" "1" expand "1" "1" "1" expand *nil nil )"2" expand *nil nil )"3" expand *nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" case "delete(pi!1, length(pi!1) - 1) = pi0!1" )"1" replace -1 -2)"1" "args(subtermOF(t!1, pi0!1))" "args(subtermOF(s!1, pi0!1))" )"1" replace "1" replace "1" replace "1" replace "1" replace "1" case "1 + last(p!1) = last(pi!1)" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"2" "1" "1" expand "1" "1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "2" "1" nil nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "3" "1" nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil 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 (-4 1))"2" (expand * add_last o insert?)"2" case "1 + pi0!1`length = #(1 + last(p!1))`length + pi0!1`length" )"1" (replace -1 1 rl)"1" (decompose-equality 1)"1" (decompose-equality 1)"1" (expand finseq_appl)"1" (decompose-equality -2)"1" (grind) nil nil )) nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil ))nil ))nil )"2" (hide -1 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )nil subterm nil )"int" integers nil )nil seq_extras "structures/" )nil positions nil )nil subterm nil )"positions" positions nil )"term" subterm nil )nil positions nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"set[T]" indexed_sets nil )"(total_order?[real])" nil )"bool" reals nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"{p: position | positionsOF(s!1)(p) AND positionsOF(t!1)(p)}" nil )"finseq[posnat]" robinsonunificationEFnil )nil IUnion_extra nil )"finseq" finite_sequences nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"positions" positions nil )"int" integers nil )"bool" reals nil )"finseq" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"posint" nil )"finseq" seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"finseq[posnat]" robinsonunificationEF nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil robinsonunificationEF nil )"[below[length(fs)] -> T]" finite_sequencesnil )"set" sets nil )nil subterm nil )"posint" nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"finseq" finite_sequences nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil ))nil ))nil 3497078571"" (skosimp*)"" (lemma next_position_TCC15)"" (inst -1 s!1 t!1 p!1)"" (assert )"" (inst -1 pi0!1)"" (assert )"" (inst -1 pi!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil robinsonunificationEF nil )"posint" nil )"int" integers nil )nil finite_sequences nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil ))nil ))nil 3497078571"" (skosimp*)"" (lift-if)"" (lift-if)"" (prop)"1" (hide-all-but (-1 -6 3)) (("1" (grind) nil nil )) nil )"2" (lift-if)"2" (prop)"2" (rewrite lex2_lt)"1" (flatten)"1" (split)"1" (hide-all-but (-5 1))"1" (expand * add_last delete insert?)"1" (expand finseq_appl)"1" (decompose-equality -1)"1" (hide -2)"1" "1" "1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (reveal 3)"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (reveal 3)"3" "3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "delete(pi!1, length(pi!1) - 1) = delete(p!1, length(p!1) - 1)" )"1" (replace -1 1)"1" (replace -3 1 rl)"1" (rewrite both_sides_minus_lt2)"1" (case "last(pi!1) = last(p!1) + 1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -2 1 rl)"2" (replace -2 -5 rl)"2" (hide-all-but (-2 -5 1 5 6))"2" (expand delete 1)"2" expand finseq_appl)"2" "1" "1" "1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" expand * add_last insert?)"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "1" expand * add_last insert?)"1" expand finseq_appl)"1" "1" "1" "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (1 6))"3" (lemma empty_0[posnat])"3" (inst -1 p!1) (("3" (assert ) nil nil ))nil ))nil ))nil )"4" (hide-all-but (1 5))"4" (lemma empty_0[posnat])"4" (inst -1 pi!1) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite next_position_TCC5) nil nil )"3" (hide-all-but (1 5))"3" (lemma empty_0[posnat])"3" (inst -1 p!1) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (lemma next_position_TCC5)"4" (inst -1 s!1 s!1 pi!1) (("4" (assert ) nil nil ))nil ))nil )"5" (hide-all-but (1 4))"5" (lemma empty_0[posnat])"5" (inst -1 pi!1) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"posint" nil )"int" integers nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )"int" integers nil )nil robinsonunificationEF nil )nil real_props nil )"finseq[posnat]" robinsonunificationEF nil )"finseq[posnat]" robinsonunificationEFnil )nil seq_extras "structures/" )"odd_int" integers nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil seq_extras "structures/" )"boolean" notequal nil )"bool" reals nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )nil term_adt nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil robinsonunificationEF nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil lex2 nil )"(total_order?[real])" nil ))nil ))nil 3497078571"" (skosimp*)"" (typepred p!1)"" (lemma delete_is_position)"" (inst-cp -1 p!1 s!1)"" (inst -1 p!1 t!1)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil seq_extras "structures/" )"posint" nil )"int" integers nil )nil finite_sequences nil )nil positions nil ))nil ))nil 3506626310"" (skosimp*)"" (assert )"" (rewrite lex2_lt)"1" (flatten)"1" (hide-all-but (-2 1 4))"1" (expand * delete finseq_appl)"1" (decompose-equality -1)"1" (hide -2)"1" (lemma empty_0[posnat])"1" (inst -1 p!1) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -3 4 5)"2" (lemma next_position_TCC5)"2" (inst -1 s!1 t!1 p!1) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide-all-but (1 2))"3" (lemma empty_0[posnat])"3" (inst -1 p!1) (("3" (assert ) nil nil )) nil )) nil ))nil )"4" (hide -1 -3 4 5)"4" (lemma next_position_TCC5)"4" (inst -1 s!1 t!1 pi0!1)"1" (assert ) nil nil )"2" (hide 2)"2" (lemma delete_is_position)"2" (inst-cp -1 p!1 s!1)"2" (inst -1 p!1 t!1)"2" (lemma empty_0[posnat])"2" (inst -1 p!1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but (1 3))"5" (lemma empty_0[posnat])"5" (inst -1 pi0!1) (("5" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"posint" nil )"int" integers nil )"term[variable, symbol, arity]" nil )"finseq[posnat]" robinsonunificationEFnil )"term[variable, symbol, arity]" nil )nil positions nil )nil robinsonunificationEF nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil seq_extras "structures/" )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" seq_extras "structures/" )"bool" reals nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )nil term_adt nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil robinsonunificationEF nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil finite_sequences nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types 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 )nil lex2 nil )"(total_order?[real])" nil ))nil ))nil 3506439585"" (measure-induct+ "length(p)" ("s" "p" ))"" (expand * subset? member)"" (skosimp)"" (expand right_pos -2)"" (expand * union IUnion member)"" (prop)"1" (hide -1 -3)"1" (expand only_empty_seq)"1" (replaces -1)"1" (expand positionsOF)"1" (lift-if)"1" (expand only_empty_seq)"1" (prop)"1" (expand union)"1" "1" "1" expand member)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (expand singleton) (("2" (assert ) nil nil )) nil ))nil )"3" (inst -2 "x!1" "delete(x!2, length(x!2) - 1)" )"1" (expand delete -2 1)"1" (lemma empty_0[posnat])"1" (inst -1 x!2)"1" (assert )"1" (inst -2 x!3) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite delete_is_position)"2" (flatten) (("2" (rewrite empty_0) nil nil ))nil ))nil )"3" (lemma empty_0[posnat])"3" (inst -1 x!2) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (skosimp*)"4" (hide -3)"4" "pi" "add_last(delete(x!2, length(x!2) - 1), 1 + i!1 + last(x!2))" nil )"1" case "pi = delete(x!2, length(x!2) - 1) o #(1 + i!1 + last(x!2))" )"1" (replace -1 -4 rl)"1" (hide -2)"1" (lemma pos_o_term)"1" (inst -1 pi q1!1 x!1)"1" assert )"1" "1" "1" assert )"1" "delete(x!2, length(x!2) - 1)" )"1" "last(x!2)" )"1" "arity(f(subtermOF(x!1, delete(x!2, length(x!2) - 1))))" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "delete(x!2, length(x!2) - 1)" )"1" "last(x!2)" )nil nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "3" "3" "3" rewrite empty_0)nil nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 1 rl)"2" (hide - 2 3)"2" (grind)"2" (decompose-equality)"1" "1" "1" "1" assert )"1" assert )"1" "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" "3" "3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" "5" "5" "5" (assert ) nil nil ))nil ))nil ))nil )"6" "6" "6" "6" "6" "6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"7" "7" "7" "7" "7" (assert ) nil nil ))nil ))nil ))nil ))nil )"8" "8" "8" "8" "8" (assert ) nil nil ))nil ))nil ))nil ))nil )"9" "9" "9" "9" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (1 2))"3" (lemma empty_0[posnat])"3" (inst -1 x!2) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (lemma empty_0[posnat])"2" (inst -1 x!2) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"posint" nil )"positions" positions nil )"(singleton?)" sets nil )nil positions nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )nil finite_sequences nil )"{p: position | positionsOF(x!1)(p)}" nil )"term[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )"finseq" finite_sequences nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil subterm nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"finseq" finite_sequences nil )"int" integers nil )"posint" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil naturalnumbers nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"term" subterm nil )nil positions nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )"[numfield, numfield -> numfield]" number_fields nil )"finseq" seq_extras "structures/" )"set" sets nil )"set[T]" indexed_sets nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"positions" robinsonunificationEF nil )"bool" sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3503335634"" "IF p = empty_seq " (" s" " t" " p")) "1" (case "x!3 = empty_seq" )"1" (hide -2)"1" (expand next_position) (("1" (assert ) nil nil )) nil ))nil )"2" (expand next_position 2 1)"2" (assert )"2" (lift-if)"2" (prop)"1" (expand next_position 2) (("1" (assert ) nil nil ))nil )"2" (hide -3)"2" (expand next_position 2)"2" (assert )"2" case "positionsOF(x!2) ") "1" (assert ) nil nil )"2" (hide 3)"2" (lemma next_position_TCC15)"2" (inst -1 x!1 x!2 x!3)"2" (assert )"2" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (1 4))"3" (lemma empty_0[posnat])"3" (inst -1 x!3) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" " add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (assert )"1" case "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3)) = empty_seq" )"1" (hide-all-but -1) (("1" (grind) nil nil ))nil )"2" (assert )"2" (lemma next_position_TCC17)"2" (inst -1 x!1 x!2 x!3)"2" (assert )"2" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" assert )"1" expand next_position 2 2)"1" case "positionsOF(x!2) ") "1" (assert ) nil nil )"2" "2" "2" "2" assert )"2" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" assert )nil nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (1 3))"3" (lemma empty_0[posnat])"3" (inst -1 x!3) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 3))"2" (lemma empty_0[posnat])"2" (inst -1 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (inst -2 x!1 x!2 "delete(x!3, length(x!3) - 1)" )"1" (assert )"1" (split)"1" (expand next_position 2 2)"1" (assert )"1" case "positionsOF(x!2) ") "1" (hide -2 1 2)"1" (lemma next_position_TCC15)"1" "1" assert )"1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (hide-all-but (1 5))"3" (lemma empty_0[posnat])"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite lex2_lt)"1" (flatten)"1" (hide-all-but (1 6))"1" (expand delete)"1" (rewrite empty_0)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide -1 2 4 5)"2" (lemma next_position_TCC5)"2" (inst -1 x!1 x!2 x!3)"2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide -1 2 4 5)"3" (lemma next_position_TCC5)"3" "delete(x!3, length(x!3) - 1)" )"1" (assert ) nil nil )"2" (hide 2)"2" rewrite delete_is_position)"1" rewrite delete_is_position)"1" "1" (rewrite empty_0) nil nil ))nil ))nil )"2" "2" (rewrite empty_0) nil nil ))nil ))nil ))nil )"3" (hide 2 3)"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide -1 2 4 5)"4" (lemma empty_0[posnat])"4" "delete(x!3, length(x!3) - 1)" )"1" (assert ) nil nil )"2" (hide 2 3)"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but (1 6))"5" (lemma empty_0[posnat])"5" (inst -1 x!3) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 5))"2" (lemma empty_0[posnat])"2" (inst -1 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (expand next_position 1)"5" (assert )"5" case "positionsOF(x!2) ") "1" (hide -2 -4 1)"1" (lemma next_position_TCC15)"1" (inst -1 x!2 x!1 x!3)"1" (assert )"1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (hide-all-but (1 4))"3" (lemma empty_0[posnat])"3" (inst -1 x!3) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma next_position_TCC5)"2" (inst -1 x!1 x!2 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide 2) (("3" (rewrite empty_0) nil nil )) nil )"4" (hide 3)"4" (lemma next_position_TCC3)"4" (inst -1 x!1 x!2 x!3) (("4" (assert ) nil nil )) nil ))nil ))nil )"5" (hide 3)"5" (rewrite delete_is_position)"5" (hide 3)"5" (flatten) (("5" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil )"6" (hide 3)"6" (lemma empty_0[posnat])"6" (inst -1 x!3) (("6" (assert ) nil nil )) nil )) nil ))nil )"7" (hide 3)"7" (lemma next_position_TCC5)"7" (inst -1 y!1 y!2 y!3) (("7" (assert ) nil nil )) nil ))nil ))nil )"8" (hide 2) (("8" (rewrite empty_0) nil nil )) nil )"9" (hide 3)"9" (lemma next_position_TCC3)"9" (inst -1 y!1 y!2 y!3) (("9" (assert ) nil nil )) nil ))nil ))nil )"10" (hide 3)"10" (rewrite delete_is_position)"10" (hide 3)"10" (flatten) (("10" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"11" (hide 3)"11" (lemma empty_0[posnat])"11" (inst -1 y!3) (("11" (assert ) nil nil )) nil )) nil ))nil )"12" (hide 3)"12" (lemma next_position_TCC5)"12" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"12" (assert ) nil nil )) nil ))nil ))nil )"13" (hide 2) (("13" (rewrite empty_0) nil nil )) nil )"14" (hide 3)"14" (lemma next_position_TCC3)"14" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"14" (assert ) nil nil )) nil ))nil ))nil )"15" (hide 3)"15" (rewrite delete_is_position)"15" (hide 3)"15" (flatten) (("15" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"16" (hide 3)"16" (lemma empty_0[posnat])"16" (inst -1 "x!1`3" ) (("16" (assert ) nil nil )) nil )) nil ))nil )"17" (hide 3)"17" (lemma next_position_TCC5)"17" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"17" (assert ) nil nil )) nil ))nil ))nil )"18" (hide 2) (("18" (rewrite empty_0) nil nil )) nil )"19" (hide 3)"19" (lemma next_position_TCC3)"19" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"19" (assert ) nil nil )) nil ))nil ))nil )"20" (hide 3)"20" (rewrite delete_is_position)"20" (hide 3)"20" (flatten) (("20" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"21" (hide 3)"21" (lemma empty_0[posnat])"21" (inst -1 "y!1`3" ) (("21" (assert ) nil nil )) nil )) nil ))nil )"22" (hide 3)"22" (lemma next_position_TCC5)"22" (inst -1 "s!1" "t!1" "p!1" ) (("22" (assert ) nil nil ))nil ))nil ))nil )"23" (hide 2) (("23" (rewrite empty_0) nil nil )) nil )"24" (hide 3)"24" (lemma next_position_TCC3)"24" (inst -1 "s!1" "t!1" "p!1" ) (("24" (assert ) nil nil ))nil ))nil ))nil )"25" (hide 3)"25" (rewrite delete_is_position)"25" (hide 3)"25" (flatten) (("25" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"26" (hide 3)"26" (lemma empty_0[posnat])"26" (inst -1 "p!1" ) (("26" (assert ) nil nil )) nil )) nil ))nil ))nil )nil robinsonunificationEF nil )"finseq" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil robinsonunificationEF nil )nil seq_extras "structures/" )"{p: position | positionsOF(x!1)(p) AND positionsOF(x!2)(p)}" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"posint" nil )nil robinsonunificationEF nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"int" integers nil )nil lex2 nil )"(strict_total_order?[real])" real_props nil )nil robinsonunificationEF nil )nil positions nil )"position" robinsonunificationEF nil )nil ordinals nil )"bool" ordinals nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" seq_extras "structures/" )"term" subterm nil )nil positions nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"ordinal" lex2 nil )"finseq" finite_sequences nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil ordinals nil )"bool" ordinals nil )nil ordstruct_adt nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil measure_induction nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" orders nil )nil defined_types nil )"int" integers nil ))nil 3503157274"" "IF p = empty_seq " (" s" " t" " p")) "1" (case "x!3 = empty_seq" )"1" (hide -2 -4)"1" (expand next_position) (("1" (assert ) nil nil )) nil ))nil )"2" (expand next_position 2)"2" (assert )"2" (prop)"1" (hide -1)"1" (rewrite delete_is_position)"1" (flatten) (("1" (rewrite empty_0) nil nil )) nil ))nil ))nil )"2" " add_last(delete(x!3, length(x!3) - 1), ") "1" (assert )"1" (lift-if)"1" (prop)"1" (hide -2 -3 -4 -5 -6 1 2 3)"1" (grind) nil nil )) nil )"2" (lemma next_position_TCC17)"2" (inst -1 x!1 x!2 x!3)"2" (assert )"2" "delete(x!3, length(x!3) - 1)" )"1" (assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 5))"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 3))"2" (lemma empty_0[posnat])"2" (inst -1 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide 3)"3" (inst -2 x!1 x!2 "delete(x!3, length(x!3) - 1)" )"1" (assert )"1" (hide -1 2)"1" (rewrite lex2_lt)"1" (flatten)"1" (hide 1 4)"1" (expand delete)"1" (lemma empty_0[posnat])"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 4)"2" (lemma next_position_TCC5)"2" (inst -1 x!1 x!2 x!3)"2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide 4)"3" (lemma next_position_TCC5)"3" "delete(x!3, length(x!3) - 1)" )"1" (assert ) nil nil )"2" (hide 2)"2" rewrite delete_is_position)"1" rewrite delete_is_position)"1" "1" (rewrite empty_0) nil nil ))nil ))nil )"2" "2" (rewrite empty_0) nil nil ))nil ))nil ))nil )"3" (hide 2 3)"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 4)"4" (lemma empty_0[posnat])"4" "delete(x!3, length(x!3) - 1)" )"1" (assert ) nil nil )"2" (hide 2 3)"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide 2 4)"5" (lemma empty_0[posnat])"5" (inst -1 x!3) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 4))"2" (lemma empty_0[posnat])"2" (inst -1 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (expand positionsOF)"4" (lift-if)"4" (expand * union IUnion member only_empty_seq)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma next_position_TCC5)"2" (inst -1 x!1 x!2 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide 2) (("3" (rewrite empty_0) nil nil )) nil )"4" (hide 3)"4" (lemma next_position_TCC3)"4" (inst -1 x!1 x!2 x!3) (("4" (assert ) nil nil )) nil ))nil ))nil )"5" (hide 3)"5" (rewrite delete_is_position)"5" (hide 3)"5" (flatten) (("5" (rewrite empty_0) nil nil )) nil )) nil ))nil ))nil )"6" (hide 3)"6" (lemma empty_0[posnat])"6" (inst -1 x!3) (("6" (assert ) nil nil )) nil )) nil ))nil )"7" (hide 3)"7" (lemma next_position_TCC5)"7" (inst -1 y!1 y!2 y!3) (("7" (assert ) nil nil )) nil ))nil ))nil )"8" (hide 2) (("8" (rewrite empty_0) nil nil )) nil )"9" (hide 3)"9" (lemma next_position_TCC3)"9" (inst -1 y!1 y!2 y!3) (("9" (assert ) nil nil )) nil ))nil ))nil )"10" (hide 3)"10" (rewrite delete_is_position)"10" (hide 3)"10" (flatten) (("10" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"11" (hide 3)"11" (lemma empty_0[posnat])"11" (inst -1 y!3) (("11" (assert ) nil nil )) nil )) nil ))nil )"12" (hide 3)"12" (lemma next_position_TCC5)"12" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"12" (assert ) nil nil )) nil ))nil ))nil )"13" (hide 2) (("13" (rewrite empty_0) nil nil )) nil )"14" (hide 3)"14" (lemma next_position_TCC3)"14" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"14" (assert ) nil nil )) nil ))nil ))nil )"15" (hide 3)"15" (rewrite delete_is_position)"15" (hide 3)"15" (flatten) (("15" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"16" (hide 3)"16" (lemma empty_0[posnat])"16" (inst -1 "x!1`3" ) (("16" (assert ) nil nil )) nil )) nil ))nil )"17" (hide 3)"17" (lemma next_position_TCC5)"17" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"17" (assert ) nil nil )) nil ))nil ))nil )"18" (hide 2) (("18" (rewrite empty_0) nil nil )) nil )"19" (hide 3)"19" (lemma next_position_TCC3)"19" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"19" (assert ) nil nil )) nil ))nil ))nil )"20" (hide 3)"20" (rewrite delete_is_position)"20" (hide 3)"20" (flatten) (("20" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"21" (hide 3)"21" (lemma empty_0[posnat])"21" (inst -1 "y!1`3" ) (("21" (assert ) nil nil )) nil )) nil ))nil )"22" (hide 3)"22" (lemma next_position_TCC5)"22" (inst -1 "s!1" "t!1" "p!1" ) (("22" (assert ) nil nil ))nil ))nil ))nil )"23" (hide 2) (("23" (rewrite empty_0) nil nil )) nil )"24" (hide 3)"24" (lemma next_position_TCC3)"24" (inst -1 "s!1" "t!1" "p!1" ) (("24" (assert ) nil nil ))nil ))nil ))nil )"25" (hide 3)"25" (rewrite delete_is_position)"25" (hide 3)"25" (flatten) (("25" (rewrite empty_0) nil nil )) nil ))nil ))nil ))nil )"26" (hide 3)"26" (lemma empty_0[posnat])"26" (inst -1 "p!1" ) (("26" (assert ) nil nil )) nil )) nil ))nil ))nil )nil robinsonunificationEF nil )"positions" positions nil )"bool" sets nil )"set[T]" indexed_sets nil )"set" sets nil )nil lex2 nil )"(strict_total_order?[real])" real_props nil )nil robinsonunificationEF nil )"(total_order?[real])" nil )"posint" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"{p: position | positionsOF(x!1)(p) AND positionsOF(x!2)(p)}" nil )"[numfield, numfield -> numfield]" number_fields nil )"finseq" seq_extras "structures/" )nil robinsonunificationEF nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"int" integers nil )nil seq_extras "structures/" )nil positions nil )"position" robinsonunificationEF nil )nil ordinals nil )"bool" ordinals nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" seq_extras "structures/" )"term" subterm nil )nil positions nil )"[(app?) -> symbol]" term_adt nil )"[term -> boolean]" term_adt nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"ordinal" lex2 nil )"finseq" finite_sequences nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil ordinals nil )"bool" ordinals nil )nil ordstruct_adt nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil measure_induction nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" orders nil )nil defined_types nil )"int" integers nil ))nil 3506181251"" (skosimp)"" (hide 1)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )"boolean" notequal nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3506259641"" (skosimp)"" (typepred p!1)"" (hide -1 -2)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"finseq" finite_sequences nil )nil finite_sequences nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3506181434"" (lemma empty_0[posnat])"" "lex2(length(p), arity(f(subtermOF(s,delete(p,length(p) - 1)))) - last(p))" "s" "t" "p" ))"1" "p!1" "next_position(x!1, x!2, x!3)" :hide? nil )"1" (inst -3 x!3)"1" (assert )"1" (ground)"1" (expand next_position -1)"1" (lift-if)"1" (ground)"1" (hide -2 1 2)"1" (replace -1 1 rl)"1" (hide -1)"1" (expand delete)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide -2 -3 -4 1 3)"2" (replace -1 1 rl)"2" (hide -1)"2" expand * add_last delete insert?nil nil ))nil ))nil ))nil )"3" "x!1" "x!2" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (replace -2 -5)"1" (split -5)"1" case "length(add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))) = length(x!3)" )"1" (assert ) nil nil )"2" (hide - 2 3)"2" expand *nil nil ))nil ))nil )"2" (flatten)"2" case "length(add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))) = length(x!3)" )"1" (assert ) nil nil )"2" "2" expand *nil nil ))nil ))nil ))nil )"3" (hide -2 2 3)"3" (lemma next_position_TCC17)"3" "3" assert )"3" "delete(x!3, length(x!3) - 1)" )"3" assert )"3" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"3" assert )"3" "3" "3" "3" expand *"3" "3" "3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma next_position_TCC15)"2" (inst -1 x!1 x!2 x!3)"2" (assert )"2" "delete(x!3, length(x!3) - 1)" )"2" assert )"2" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"2" assert )"2" "2" expand *"2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "delete(x!3, length(x!3) - 1)" )"1" (replace -1 -3)"1" (split -3)"1" (expand delete -1)"1" (assert ) nil nil )) nil )"2" (flatten)"2" (expand delete -1)"2" (assert ) nil nil )) nil ))nil )"3" (assert )"3" (hide -1 4 5)"3" "3" "3" assert )"3" "delete(x!3, length(x!3) - 1)" )"3" assert )"3" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite delete_is_position)"2" (rewrite delete_is_position) nil nil ))nil ))nil )"5" (hide -1 -3 -4 1)"5" (lemma empty_0[posnat])"5" (inst -1 p!1) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand next_position -1)"2" (lift-if)"2" (ground)"1" (hide -2 1 2)"1" (replace -1 1 rl)"1" (hide -1)"1" (expand delete)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide -2 -3 -4 1 3)"2" (replace -1 1 rl)"2" (hide -1)"2" expand * add_last delete insert?"2" (grind) nil nil )) nil ))nil ))nil ))nil )"3" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (replace -2 -5)"1" (split -5)"1" (hide-all-but (-1 2 3))"1" expand * add_last delete insert?nil nil ))nil )"2" (flatten)"2" (hide -1 -3 -4 -5 -6 2)"2" case "last(add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))) = 1 + last(x!3)" )"1" "1" (assert ) nil nil ))nil )"2" "2" expand *"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma next_position_TCC17)"3" (inst -1 x!1 x!2 x!3)"3" assert )"3" "delete(x!3, length(x!3) - 1)" )"3" assert )"3" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"3" assert )"3" "3" "3" "3" expand *"3" "3" "3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma next_position_TCC15)"2" (inst -1 x!1 x!2 x!3)"2" (assert )"2" "delete(x!3, length(x!3) - 1)" )"2" assert )"2" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"2" assert )"2" "2" expand *"2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "x!1" "x!2" "delete(x!3, length(x!3) - 1)" )"1" (lemma next_position_TCC19)"1" (inst -1 x!1 x!2 x!3)"1" (assert )"1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" assert )"1" "1" replace -1 -3)"1" "1" case "length(delete(x!3, length(x!3) - 1)) < length(x!3)" )"1" (assert ) nil nil )"2" "2" expand delete)"2" assert )nil nil ))nil ))nil ))nil )"2" case "length(delete(x!3, length(x!3) - 1)) < length(x!3)" )"1" (assert ) nil nil )"2" "2" expand delete)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite delete_is_position)"2" (rewrite delete_is_position) nil nil ))nil ))nil )"5" (hide-all-but (-2 3 4))"5" (lemma empty_0[posnat])"5" (inst -1 p!1) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 1 2)"2" (inst -3 y!3) (("2" (assert ) nil nil )) nil )) nil )"3" (hide-all-but (-3 -4))"3" (inst -2 y!3) (("3" (assert ) nil nil )) nil )) nil )"4" (hide -1 2)"4" (lemma next_position_TCC5)"4" (inst -1 x!1 x!2 x!3) (("4" (assert ) nil nil )) nil ))nil ))nil )"5" (hide 1) (("5" (inst -2 x!3) (("5" (assert ) nil nil )) nil ))nil )"6" (hide 2)"6" (lemma next_position_TCC12)"6" (inst -1 x!1 x!2 x!3)"6" (assert )"6" (inst -1 "delete(x!3, length(x!3) - 1)" )"6" (inst -1 x!3) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"7" (hide 2)"7" (rewrite delete_is_position)"7" (inst -1 x!3) (("7" (assert ) nil nil )) nil )) nil ))nil )"8" (hide 2) (("8" (inst -1 x!3) (("8" (assert ) nil nil )) nil ))nil )"9" (hide 2)"9" (lemma next_position_TCC5)"9" (inst -1 y!1 y!2 y!3) (("9" (assert ) nil nil )) nil ))nil ))nil )"10" (hide 1)"10" (inst -2 y!3) (("10" (assert ) nil nil )) nil )) nil )"11" (hide 2)"11" (lemma next_position_TCC12)"11" (inst -1 y!1 y!2 y!3)"11" (assert )"11" (inst -1 "delete(y!3, length(y!3) - 1)" )"11" (inst -1 y!3) (("11" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"12" (hide 2)"12" (rewrite delete_is_position)"12" (inst -1 y!3) (("12" (assert ) nil nil )) nil )) nil ))nil )"13" (hide 2)"13" (inst -1 y!3) (("13" (assert ) nil nil )) nil )) nil )"14" (hide -2 2)"14" (inst -3 "x!1`3" ) (("14" (assert ) nil nil )) nil )) nil )"15" (hide-all-but (-3 -4))"15" (inst -2 "x!1`3" ) (("15" (assert ) nil nil )) nil )) nil )"16" (hide-all-but (-1 -3 -4))"16" (inst -3 "y!1`3" ) (("16" (assert ) nil nil )) nil )) nil )"17" (hide-all-but (-3 -4))"17" (inst -2 "y!1`3" ) (("17" (assert ) nil nil )) nil )) nil )"18" (hide 2)"18" (lemma next_position_TCC5)"18" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"18" (assert ) nil nil )) nil ))nil ))nil )"19" (hide 1)"19" (inst -2 "x!1`3" ) (("19" (assert ) nil nil )) nil )) nil )"20" (hide 2)"20" (lemma next_position_TCC12)"20" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"20" (assert )"20" (inst -1 "delete(x!1`3, length(x!1`3) - 1)" )"20" (inst -1 "x!1`3" ) (("20" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"21" (hide 2)"21" (rewrite delete_is_position)"21" (inst -1 "x!1`3" ) (("21" (assert ) nil nil )) nil ))nil ))nil )"22" (hide 2)"22" (inst -1 "x!1`3" ) (("22" (assert ) nil nil )) nil )) nil )"23" (hide 2)"23" (lemma next_position_TCC5)"23" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"23" (assert ) nil nil )) nil ))nil ))nil )"24" (hide 1)"24" (inst -2 "y!1`3" ) (("24" (assert ) nil nil )) nil )) nil )"25" (hide 2)"25" (lemma next_position_TCC12)"25" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"25" (assert )"25" (inst -1 "delete(y!1`3, length(y!1`3) - 1)" )"25" (inst -1 "y!1`3" ) (("25" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"26" (hide 2)"26" (rewrite delete_is_position)"26" (inst -1 "y!1`3" ) (("26" (assert ) nil nil )) nil ))nil ))nil )"27" (hide 2)"27" (inst -1 "y!1`3" ) (("27" (assert ) nil nil )) nil )) nil )"28" (hide +)"28" (inst -3 p!1) (("28" (assert ) nil nil )) nil )) nil )"29" (hide -1 +)"29" (inst -2 p!1) (("29" (assert ) nil nil )) nil )) nil )"30" (hide 2)"30" (lemma next_position_TCC5)"30" (inst -1 s!1 t!1 p!1) (("30" (assert ) nil nil )) nil ))nil ))nil )"31" (hide 1)"31" (inst -2 p!1) (("31" (assert ) nil nil )) nil )) nil )"32" (hide 2)"32" (lemma next_position_TCC12)"32" (inst -1 s!1 t!1 p!1)"32" (assert )"32" (inst -1 "delete(p!1, length(p!1) - 1)" )"32" (inst -1 p!1) (("32" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"33" (hide 2)"33" (rewrite delete_is_position)"33" (inst -1 p!1) (("33" (assert ) nil nil )) nil )) nil ))nil )"34" (inst -1 p!1) (("34" (assert ) nil nil )) nil ))nil ))nil )"int" integers nil )nil defined_types nil )"bool" orders nil )nil measure_induction nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunificationEFnil )nil term_adt nil )nil nat_types nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"boolean" notequal nil )nil finite_sequences nil )"finseq" finite_sequences nil )nil ordstruct_adt nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )nil positions nil )"term" subterm nil )"bool" reals nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"T" seq_extras "structures/" )"bool" ordinals nil )nil ordinals nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"position" robinsonunificationEF nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil robinsonunificationEF nil )nil positions nil )"(total_order?[real])" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"{p: position | AND positionsOF(x!2)(p) AND p /= empty_seq}" nil )"[numfield, numfield -> numfield]" number_fields nil )nil robinsonunificationEF nil )"[below[length(fs)] -> T]" finite_sequencesnil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil robinsonunificationEF nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"posint" nil )"(strict_total_order?[real])" real_props nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"{p: position | AND positionsOF(x!2)(p) AND p /= empty_seq}" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"{p: position | AND positionsOF(y!2)(p) AND p /= empty_seq}" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"[s: term, t: term, AND positionsOF(t)(p) AND p /= empty_seq}]" nil )"[s: term, t: term, AND positionsOF(t)(p) AND p /= empty_seq}]" nil )"{p: position | AND positionsOF(t!1)(p) AND p /= empty_seq}" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )nil seq_extras "structures/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil 3504615157"" (skosimp)"" (lemma "next_pos_length_and_last" )"" (inst -1 s!1 t!1 p!1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )nil robinsonunificationEFnil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[symbol -> nat]" robinsonunificationEFnil )nil positions nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"{p: position | positionsOF(s!1)(p) AND positionsOF(t!1)(p)}" nil )nil finite_sequences nil )"finseq" finite_sequences nil ))nil 3506959387"" (measure-induct+ "length(p)" ("s" "p" ))"" (skosimp)"" (expand member)"" (prop)"1" (expand right_pos -1)"1" (prop)"1" (hide 2 -3)"1" (expand only_empty_seq) (("1" (assert ) nil nil ))nil ))nil )"2" (expand union)"2" (prop)"1" (expand member)"1" (prop)"1" (hide -2 1 3)"1" (expand singleton)"1" (assert ) nil nil )) nil ))nil )"2" "delete(x!2, length(x!2) - 1)" )"1" (inst -2 q!1)"1" (expand delete -2 1)"1" (rewrite empty_0)"1" assert )"1" "1" "1" expand left_pos)"1" "1" "1" "p1!1 o #(last(x!2))" "1" "1" "1" assert )"1" "1" "1" nil nil ))nil )"2" rewrite o_assoc)"2" replace "2" "2" expand "2" rewrite "2" expand "2" "1" nil nil )"2" "1" nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite empty_0)nil nil ))nil ))nil ))nil )"2" "p1!1 o #(last(x!2))" "1" "1" "1" assert )"1" "1" rewrite o_assoc)"1" replace "1" "1" expand "1" rewrite "1" expand "1" "1" nil nil )"2" "1" nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" rewrite "3" "3" "3" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite empty_0)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand left_pos)"2" "delete(x!2, length(x!2) - 1)" "#(last(x!2))" "1" assert )"1" "1" "1" (grind) nil nil ))nil )"2" "2" expand delete)"2" rewrite empty_0)"2" "1" nil nil )"2" "1" nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite empty_0)nil nil ))nil ))nil )"3" "3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite delete_is_position)"2" (hide-all-but (1 3))"2" (flatten)"2" (rewrite empty_0) nil nil )) nil ))nil ))nil )"3" (hide-all-but (1 2))"3" (lemma empty_0[posnat])"3" (inst -1 x!2)"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (expand * member IUnion)"2" (skosimp*)"2" (expand left_pos)"2" "delete(x!2, length(x!2) - 1)" "#(last(x!2))" "#(1 + i!1 + last(x!2)) o q1!1" )"1" (flatten)"1" "1" "1" "1" "1" expand delete)"1" rewrite empty_0)"1" assert )"1" "1" (grind) nil nil )"2" "1" (grind) nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand delete)"2" rewrite empty_0)"2" assert )"2" "1" (grind) nil nil )"2" "1" (grind) nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil )"5" rewrite first_compo)"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "x!2 = empty_seq" )"1" (hide -3)"1" (expand * left_pos right_pos only_empty_seq)"1" (assert )"1" (skosimp)"1" (prop)"1" (replaces -3)"1" (lemma seq_empty[posnat])"1" (inst -1 r!1 p1!1)"1" (assert )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replaces -4)"2" (hide -1 -3)"2" (lemma seq_empty[posnat])"2" (inst -1 r!1 p1!1)"2" assert )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "q!1 = delete(x!2, length(x!2) - 1)" )"1" (hide -2 -3)"1" (expand right_pos)"1" (assert )"1" (expand * union member)"1" (flatten)"1" (hide 4)"1" (replace -1 3 rl)"1" (expand * right_pos only_empty_seq)"1" "1" expand * union member)"1" "1" "1" expand singleton)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -2 x!1 "delete(x!2, length(x!2) - 1)" )"1" (inst -2 q!1)"1" (expand delete -2 1)"1" (rewrite empty_0)"1" (assert )"1" (expand right_pos 3)"1" (expand * union member)"1" (flatten 3)"1" assert )"1" "1" expand * singleton left_pos)"1" "1" "1" "delete(p1!1, length(p1!1) - 1)" "1" assert )"1" "1" expand o)"1" "1" expand *"1" expand "1" "1" "1" "1" assert )"1" "1" "1" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand delete 1)"2" rewrite empty_0)"2" rewrite empty_0)"2" expand o)"2" expand "2" "2" assert )"2" "1" "1" nil nil ))nil )"2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil )"5" "5" "5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "delete(p1!1, length(p1!1) - 1)" "1" "1" "1" "1" "1" expand *"1" rewrite empty_0)"1" rewrite "1" assert )"1" expand o)"1" "1" assert )"1" "1" "1" nil nil )"2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil )"5" "5" "5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand IUnion)"2" "first(q1!1) - 1 - last(x!2)" )"1" assert )"1" "rest(q1!1)" )"1" "1" case "add_last(delete(x!2, length(x!2) - 1), ") "1" "1" "1" "add_last(delete(x!2, length(x!2) - 1), first(q1!1))" "rest(q1!1)" "1" replace "1" assert )nil nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "r!1 = delete(x!2, length(x!2) - 1)" )"1" replace "1" "1" "1" "1" "1" assert )"1" case "add_last(r!1, first(q1!1)) o rest(q1!1) = r!1 o ( #(first(q1!1)) o rest(q1!1))" )"1" "1" assert )nil nil ))nil )"2" "2" expand *"2" expand "2" "1" nil nil )"2" "1" nil nil )"2" "2" nil nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"2" rewrite "2" rewrite "2" "1" expand "1" "1" "1" expand "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "2" "2" "2" expand "2" "2" "2" "1" "1" assert )nil nil ))nil )"2" "2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "r!1 = delete(x!2, length(x!2) - 1)" )"1" replace "1" "1" expand "1" "1" "1" "1" "1" "1" "1" "1" assert )"1" expand "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" assert )"1" nil nil ))nil ))nil )"2" "2" "2" "2" "2" "2" "2" assert )"2" expand "2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" rewrite nil nil ))nil )"5" "5" rewrite nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" rewrite nil nil ))nil )"8" "8" "8" rewrite nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"2" rewrite "2" rewrite "2" expand "2" "2" "2" expand "2" "2" "2" "2" "1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" case "last(x!2) = first(p1!1)" )"1" replace "1" assert )nil nil ))nil )"2" "2" expand *"2" expand "2" "2" "2" "x!2`length - 1" )"1" expand "1" rewrite "1" assert )"1" expand "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi" "r!1 o #(first(q1!1))" )"2" case "delete(x!2, length(x!2) - 1) = r!1" )"1" "1" case "first(q1!1) = last(pi)" )"1" "1" "1" "1" "1" case "delete(pi, length(pi) - 1) = r!1" )"1" "1" assert )nil nil ))nil )"2" "2" expand *"2" "2" "1" nil nil )"2" "1" expand "1" "1" "1" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "2" "2" "2" "1" "1" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" "2" "2" "2" "2" assert )"2" replace "2" "2" rewrite "2" "r!1 o #(first(q1!1))" "rest(q1!1)" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"2" expand "2" "2" "2" "pi`length - 1" )"1" expand "#" "1" assert )"1" replace "1" assert )"1" expand "#" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil )"2" "2" expand "2" rewrite "2" rewrite "2" assert )"2" expand "2" expand "2" "2" "2" "1" expand "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "1" expand "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "3" "3" "3" nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" rewrite nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand *"3" rewrite empty_0)"3" assert )"3" expand "3" expand "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite delete_is_position)"2" (flatten) (("2" (rewrite empty_0) nil nil ))nil ))nil )"3" (lemma empty_0[posnat])"3" (inst -1 x!2) (("3" (assert ) nil nil )) nil ))nil ))nil )"3" (lemma empty_0[posnat])"3" (inst -1 x!2) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide -3)"3" (expand left_pos)"3" (skosimp)"3" (prop)"1" (replaces -1)"1" (replaces -2)"1" (expand o)"1" (decompose-equality -1)"1" (hide -2)"1" (lemma empty_0[posnat])"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replaces -4)"2" (replaces -1)"2" (expand o)"2" (flatten)"2" (decompose-equality -2)"2" (inst -1 "length(r!1)" )"1" assert )"1" expand first)"1" expand finseq_appl)"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"positions" positions nil )"(singleton?)" sets nil )nil positions nil )nil seq_extras "structures/" )nil finite_sequences nil )"int" integers nil )"finseq" finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"finseq" finite_sequences nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"finseq" seq_extras "structures/" )nil finite_sequences nil )"{p: position | positionsOF(x!1)(p)}" nil )"term[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )"set[T]" indexed_sets nil )"nonneg_int" nil )"T" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )nil positions nil )"term" subterm nil )nil naturalnumbers nil )"set" sets nil )"posint" nil )"(nonempty?)" sets nil )"non_empty_finite_set[position]" robinsonunificationEF nil )"position[variable, symbol, arity]" nil )"finseq" seq_extras "structures/" )"{q: position | positionsOF(x!1)(q)}" nil )"finseq" seq_extras "structures/" )nil subterm nil )nil seq_extras "structures/" )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"finseq" seq_extras "structures/" )"finseq[posnat]" robinsonunificationEF nil )"odd_int" integersnil )"below[pi`length - 1]" robinsonunificationEFnil )nil positions nil )nil robinsonunificationEF nil )"odd_int" integers nil )"position[variable, symbol, arity]" nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"position[variable, symbol, arity]" nil )"bool" booleans nil )"T" epsilons nil )"bool" booleans nil )nil seq_extras "structures/" )"nonneg_int" nil )"even_int" integersnil )"position[variable, symbol, arity]" nil )"position[variable, symbol, arity]" nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" positions nil )"boolean" notequal nil )"positions" robinsonunificationEF nil )"bool" sets nil ) (set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" robinsonunificationEFnil )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 )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3507041072"" (lemma empty_0[posnat])"" "lex2(length(p), arity(f(subtermOF(s,delete(p,length(p) - 1)))) - last(p))" "s" "t" "p" ))"1" (case "x!3 = empty_seq" )"1" (hide -2 -3)"1" (replaces -1)"1" expand * member right_pos next_position emptyset"1" (prop)"1" (expand positionsOF)"1" (lift-if)"1" (expand only_empty_seq)"1" (prop)"1" (expand union)"1" (flatten)"1" (hide 3)"1" expand member)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma member_right_pos)"2" (inst -1 x!1 x!3 "next_position(x!1, x!2, x!3)" )"1" (assert )"1" "q!1" "next_position(x!1, x!2, x!3)" nil )"1" (hide 3)"1" (expand next_position -1)"1" (lift-if)"1" (prop)"1" (hide -2 1)"1" (expand left_pos)"1" "delete(x!3, length(x!3) - 1)" "#(last(x!3))" empty_seq)"1" assert )"1" "1" "1" expand empty_seq)"1" expand "#" )"1" (propax) nil nil ))nil ))nil ))nil )"2" "2" expand * delete finseq_appl)"2" rewrite empty_0)"2" "1" expand o)"1" expand "#" )"1" (propax) nil nil ))nil ))nil )"2" "1" expand o)"1" (grind) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (rewrite empty_0) nil nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 -4 1)"2" (expand left_pos)"2" "delete(x!3, length(x!3) - 1)" "#(last(x!3))" "#(1 + last(x!3))" )"1" "1" "1" "1" replace -1 1 rl)"1" "1" expand *"1" "1" assert )"1" assert )"1" "1" nil nil )"2" "1" nil nil )"2" "2" assert )nil nil ))nil ))nil )"3" nil nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand delete)"2" "2" assert )"2" assert )"2" "1" (grind) nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" expand * first finseq_appl "#" )"5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (lemma next_position_TCC17)"1" (inst -1 x!1 x!2 x!3)"1" assert )"1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" assert )"1" case "NOT add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3)) = ") "1" assert )"1" "1" replace -1)"1" "pi" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" nil )"1" "1" "1" assert )"1" "1" "1" assert )"1" "1" expand "1" "1" "1" "add_last(delete(p1!1, length(p1!1) - 1), last(p1!1) - 1)" "1" assert )"1" "1" "1" nil nil ))nil )"2" "2" expand *"2" "2" "2" "2" assert )"2" assert )"2" "1" "1" "1" "1" "1" "1" assert )nil nil )"2" expand "2" assert )nil nil ))nil ))nil )"2" "1" assert )nil nil )"2" expand "2" assert )nil nil ))nil ))nil )"3" "1" assert )"1" "1" expand *"1" assert )nil nil ))nil ))nil ))nil )"2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" nil nil )"4" "4" assert )nil nil ))nil ))nil )"2" nil nil )"3" "3" assert )nil nil ))nil ))nil )"2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "last(p1!1) = 1 + last(x!3)" )"1" assert )nil nil )"2" "2" "2" expand *"2" "2" rewrite "2" assert )"2" "1" "x!3`length - 1" )"1" assert )"1" "1" "1" replace "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "2" "2" nil nil ))nil ))nil ))nil )"2" expand "2" "2" assert )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil )"2" "add_last(delete(p1!1, length(p1!1) - 1), last(p1!1) - 1)" "1" "1" "1" assert )"1" "1" replace "1" "1" "1" "1" assert )"1" expand *"1" "1" "1" "1" "1" "1" "1" "1" assert )nil nil )"2" expand "2" assert )nil nil ))nil ))nil )"2" "1" assert )nil nil )"2" expand "2" assert )nil nil ))nil ))nil )"3" "1" assert )nil nil )"2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" expand *"3" "3" assert )"3" assert )"3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "last(p1!1) - 1 = last(x!3)" )"1" assert )nil nil )"2" replace "2" "2" "2" "2" assert )"2" expand *"2" "2" "1" "x!3`length - 1" )"1" assert )nil nil )"2" expand "2" assert )nil nil ))nil ))nil )"2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (prop)"1" "1" "1" assert )"1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" (assert ) nil nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"3" (hide-all-but (-5 1 3))"3" (inst -1 x!3)"3" (assert ) nil nil )) nil ))nil ))nil )"4" "delete(x!3, length(x!3) - 1)" )"1" (lemma next_position_TCC19)"1" (inst -1 x!1 x!2 x!3)"1" assert )"1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "add_last(delete(x!3, length(x!3) - 1), 1 + last(x!3))" )"1" assert )"1" "1" replace -1)"1" "1" "delete(x!3, length(x!3) - 1)" "1" assert )"1" "1" "delete(x!3, length(x!3) - 1)" )"1" assert )"1" "1" "pi" "delete(x!3, length(x!3) - 1)" nil )"1" expand "1" "1" "1" "add_last(p1!1, last(x!3))" "1" assert )"1" "1" "1" nil nil ))nil )"2" "2" "2" "2" "2" assert )"2" expand *"2" "2" "2" "1" "1" "1" "1" nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "add_last(p1!1, last(x!3))" "1" assert )"1" "1" "1" "1" "1" "1" "1" "1" assert )"1" expand *"1" "1" "1" "1" "1" case "x!4 = x!3`length - 1" )"1" assert )nil nil )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" rewrite "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "delete(x!3, length(x!3) - 1)" )"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" rewrite "3" "3" assert )nil nil ))nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite delete_is_position)"1" rewrite delete_is_position)"1" "1" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" (inst -3 x!3) (("3" (assert ) nil nil ))nil ))nil )"5" (hide -1 -3 -4 1)"5" (expand left_pos)"5" (inst 1 empty_seq x!3 empty_seq)"5" assert )"5" (rewrite empty_o_seq) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite next_position_is_position) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma next_position_TCC5)"2" (inst -1 x!1 x!2 x!3) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide 1) (("3" (inst -2 x!3) (("3" (assert ) nil nil )) nil ))nil )"4" (hide 2)"4" (lemma next_position_TCC3)"4" (inst -1 x!1 x!2 x!3) (("4" (assert ) nil nil )) nil ))nil ))nil )"5" (hide 2)"5" (rewrite delete_is_position)"5" (inst -1 x!3) (("5" (assert ) nil nil )) nil )) nil ))nil )"6" (hide 2) (("6" (inst -1 x!3) (("6" (assert ) nil nil )) nil ))nil )"7" (hide 2)"7" (lemma next_position_TCC5)"7" (inst -1 y!1 y!2 y!3) (("7" (assert ) nil nil )) nil ))nil ))nil )"8" (hide 1) (("8" (inst -2 y!3) (("8" (assert ) nil nil )) nil ))nil )"9" (hide 2)"9" (lemma next_position_TCC3)"9" (inst -1 y!1 y!2 y!3) (("9" (assert ) nil nil )) nil ))nil ))nil )"10" (hide 2)"10" (rewrite delete_is_position)"10" (inst -1 y!3) (("10" (assert ) nil nil )) nil )) nil ))nil )"11" (hide 2)"11" (inst -1 y!3) (("11" (assert ) nil nil )) nil )) nil )"12" (hide 2)"12" (lemma next_position_TCC5)"12" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"12" (assert ) nil nil )) nil ))nil ))nil )"13" (hide 1)"13" (inst -2 "x!1`3" ) (("13" (assert ) nil nil )) nil )) nil )"14" (hide 2)"14" (lemma next_position_TCC3)"14" (inst -1 "x!1`1" "x!1`2" "x!1`3" )"14" (assert ) nil nil )) nil ))nil ))nil )"15" (hide 2)"15" (rewrite delete_is_position)"15" (inst -1 "x!1`3" ) (("15" (assert ) nil nil )) nil ))nil ))nil )"16" (hide 2)"16" (inst -1 "x!1`3" ) (("16" (assert ) nil nil )) nil )) nil )"17" (hide 2)"17" (lemma next_position_TCC5)"17" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"17" (assert ) nil nil )) nil ))nil ))nil )"18" (hide 1)"18" (inst -2 "y!1`3" ) (("18" (assert ) nil nil )) nil )) nil )"19" (hide 2)"19" (lemma next_position_TCC3)"19" (inst -1 "y!1`1" "y!1`2" "y!1`3" )"19" (assert ) nil nil )) nil ))nil ))nil )"20" (hide 2)"20" (rewrite delete_is_position)"20" (inst -1 "y!1`3" ) (("20" (assert ) nil nil )) nil ))nil ))nil )"21" (hide 2)"21" (inst -1 "y!1`3" ) (("21" (assert ) nil nil )) nil )) nil )"22" (hide 2)"22" (lemma next_position_TCC5)"22" (inst -1 s!1 t!1 p!1) (("22" (assert ) nil nil )) nil ))nil ))nil )"23" (hide 1)"23" (inst -2 p!1) (("23" (assert ) nil nil )) nil )) nil )"24" (hide 2)"24" (lemma next_position_TCC3)"24" (inst -1 s!1 t!1 p!1) (("24" (assert ) nil nil )) nil ))nil ))nil )"25" (hide 2)"25" (rewrite delete_is_position)"25" (inst -1 p!1) (("25" (assert ) nil nil )) nil )) nil ))nil )"26" (hide 2)"26" (inst -1 p!1) (("26" (assert ) nil nil )) nil )) nil ))nil ))nil )"int" integers nil )nil defined_types nil )"bool" orders nil )nil measure_induction nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil naturalnumbers nil )"[symbol -> nat]" robinsonunificationEFnil )nil term_adt nil )nil nat_types nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"boolean" notequal nil )nil finite_sequences nil )"finseq" finite_sequences nil )nil ordstruct_adt nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )nil positions nil )"term" subterm nil )"bool" reals nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"T" seq_extras "structures/" )"bool" ordinals nil )nil ordinals nil )"positions" robinsonunificationEF nil )"position" robinsonunificationEF nil )"bool" sets nil ) (set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil robinsonunificationEF nil )nil seq_extras "structures/" )nil positions nil )"position[variable, symbol, arity]" nil )"position[variable, symbol, arity]" nil )"below[x!3`length]" robinsonunificationEFnil )nil seq_extras "structures/" )"below[x!3`length]" robinsonunificationEFnil )nil robinsonunificationEF nil )"finseq[posnat]" robinsonunificationEF nil )"position[variable, symbol, arity]" nil )nil robinsonunificationEF nil )"position[variable, symbol, arity]" nil )"even_int" integersnil )"below[x!3`length]" robinsonunificationEFnil )"odd_int" integers nil )"position[variable, symbol, arity]" nil )"below[x!3`length]" robinsonunificationEFnil )nil robinsonunificationEFnil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )"[numfield, numfield -> numfield]" number_fields nil )"T" seq_extras "structures/" )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"int" integers nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil integers nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"finite_sequence[T]" set2seq "structures/" )nil finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"bool" positions nil )"{p: position | AND positionsOF(x!2)(p) AND p /= empty_seq}" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"set" sets nil )"positions" positions nil )"set" sets nil )nil robinsonunificationEF nil )nil robinsonunificationEF nil )nil seq_extras "structures/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil 3507387106"" (skosimp)"" case "subset?(right_pos(s!1, p!1), right_pos(s!1, q!1)) AND ") "1" (hide -2)"1" (flatten)"1" (expand subset?)"1" (inst -1 p!1)"1" (inst -2 q!1)"1" (case "p!1 = empty_seq" )"1" (hide -2)"1" (expand right_pos -2 2)"1" (assert )"1" (case "member(q!1, right_pos(s!1, q!1))" )"1" (assert )"1" (hide -1)"1" expand * member only_empty_seq)"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand * right_pos member)"2" expand * union member)"2" "2" "2" expand singleton)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "q!1 = empty_seq" )"1" (hide -3)"1" (expand right_pos -2 2)"1" (assert )"1" case "member(p!1, right_pos(s!1, p!1))" )"1" (assert )"1" "1" expand * member only_empty_seq)nil nil ))nil ))nil )"2" (hide-all-but 1)"2" expand * right_pos union member)"2" "2" "2" expand singleton)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "member(p!1, right_pos(s!1, p!1)) AND member(q!1, right_pos(s!1, q!1))" )"1" (flatten)"1" (assert )"1" (hide -1 -2)"1" (lemma member_right_pos)"1" "1" "1" assert )"1" "1" expand left_pos)"1" "1" "1" replace -1 -4)"1" replace -4 -2)"1" replace -3 -2)"1" expand o -2)"1" "1" "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -5 -1)"2" replace -4 -2)"2" replace -2 -1)"2" case "p1!2 o p1!1 = q1!2" )"1" replace "1" rewrite "1" assert )nil nil )"2" "2" "2" rewrite nil nil ))nil ))nil ))nil ))nil )"2" "2" expand o)"2" "2" "2" "1" "1" "1" "1" "x!1 + r!2`length" )"1" assert )nil nil ))nil )"2" "x!1 + r!2`length" )"2" assert )nil nil ))nil ))nil ))nil )"2"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 1.10 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
