[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification list-del

list-del/indexseq-stackseq/get-rec is used by orderedl-at, coversi-append, covers-rem,
list-del/indexseq-stackseq/put-at is used by pushx-covers,
list-del/get-app is used by pushx-cut-seq,
list-del/get-append-less is used by tolist-cut-seq, pushx-inv, pushx-cut-seq, pushix-to-push, precedes-append,
list-del/indexseq-stackseq/get-append-less is used by pushx-covers,
list-del/get-last-03 is used by tolist-single, pushx-inv, pushx-cut-seq, pushix-to-push,
list-del/indexseq-stackseq/get-last-03 is used by pushx-covers,
list-del/indexseq-stackseq/get-succ is used by theoremx-atmost-h, pushx-nonrec,
list-del/indexseq-stackseq/get-zero-01 is used by theoremx-atmost-h, pushx-nonrec, orderedl-at, coversi-append, covers-rem,
list-del/indexseq-stackseq/one-03 is used by orderedl-at,
list-del/indexseq-stackseq/put-at-eq is used by pushx-covers,
list-del/indexseq-stackseq/put-length is used by pushx-covers,
list-del/indexseq-stackseq/put-succ is used by pushx-nonrec,
list-del/indexseq-stackseq/put-zero is used by pushx-nonrec,

Used from specification nat-basic1

nat-basic1/f is used by tolist-cut-seq, theoremx-atmost-h, theoremx, solixh-ordered, solixh-inv, solixh-covers, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushx-covers, pushix-to-push, precedesex-solixh, precedesex-pushix, precedes-trans, precedes-irrefl, precedes-append, orderedl-at, ordered-precedes-h, ordered-precedes, coversi-append, covers-rem, ascsubseq-rem, ascsubseq-in-size, allls-incbound, allls-in,
nat-basic1/lf is used by theoremx-atmost-h, theoremx, pushx-ordered, pushx-inv-gen, precedesex-pushix, precedes-trans, precedes-irrefl, precedes-append, ordered-precedes-h, ascsubseq-rem, ascsubseq-in-size,
nat-basic1/lf-01 is used by theoremx, solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh, precedesex-pushix,
nat-basic1/lf-02 is used by theoremx, pushx-covers, precedesex-pushix, ascsubseq-in-size,
nat-basic1/ls-02 is used by theoremx, pushx-inv-gen, pushx-inv, pushx-covers, precedes-irrefl, precedes-append, ordered-precedes-h, ordered-precedes, ascsubseq-rem, ascsubseq-in-size,
nat-basic1/zero is used by covers-empty,
nat-basic1/zero-01 is used by theoremx-atmost-h, solix-covers, pushx-nonrec, orderedl-at, coversi-empty, covers-empty, ascsubseq-empty,

Used from specification oelem

oelem/indexseq/irreflexivity is used by theoremx-atleast-ind, pushx-inv-gen, pushx-inv, pushx-covers, precedes-notsame, ascsubseq-in-size,
oelem/indexseq/ls-le is used by pushx-inv-gen,
oelem/nll is used by ordered-precedes-h, ascsubseq-rem,
oelem/nnn is used by ordered-precedes-h,
oelem/indexseq/transitivity is used by theoremx-atmost-h, theoremx, pushx-ordered, pushx-inv-gen, precedesex-pushix, precedes-trans, precedes-irrefl, precedes-append, ordered-precedes-h, ascsubseq-rem, ascsubseq-in-size,
oelem/transitivity is used by precedes-trans, ascsubseq-rem,

Used from specification nat-basic2

nat-basic2/a is used by tolist-size, theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast, solixh-to-solitaireh, solixh-ordered, solixh-inv, solixh-covers, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-covers, precedesex-solixh, precedes-trans, precedes-append, orderedl-at, inv-incbound, coversi-append, covers-rem, allls-incbound,
nat-basic2/c is used by tolist-size, theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast, solixh-to-solitaireh, solixh-ordered, solixh-inv, solixh-covers, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-covers, precedesex-solixh, precedes-trans, precedes-append, orderedl-at, inv-incbound, coversi-append, covers-rem, allls-incbound,
nat-basic2/eq-01 is used by tolist-size, theoremx-atleast-ind, theoremx-atleast,
nat-basic2/eq-inc-neq is used by solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh,
nat-basic2/eqs is used by solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh,
nat-basic2/l is used by theoremx-atmost-h,
nat-basic2/l-02 is used by solixh-to-solitaireh, solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh, allls-incbound,
nat-basic2/nls-fst is used by theoremx-atmost-h,
nat-basic2/oz is used by orderedl-at, coversi-append, covers-rem,
nat-basic2/s is used by theoremx-atmost-h, theoremx-atleast-ind, solixh-to-solitaireh, solixh-ordered, solixh-inv, solixh-covers, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-covers, precedesex-solixh, precedes-append, orderedl-at, coversi-append, covers-rem,
nat-basic2/succ is used by theoremx-atmost-h, theoremx, solixh-ordered, solixh-inv, solixh-covers, pushx-ordered, pushx-inv-gen, precedesex-solixh, precedesex-pushix, precedes-trans, precedes-irrefl, precedes-append, ordered-precedes-h, ascsubseq-rem,

Used from specification list

list/indexseq/One is used by tolist-single, ascsubseq-2, allls-single,
list/indexseq-stackseq/One is used by tolistl-single, precedesex-2, ordered-single, inv-single,
list/indexseq/c is used by tolist-single, ascsubseq-2, allls-single,
list/indexseq-stackseq/c is used by tolistl-single, precedesex-2, ordered-single, inv-single,
list/indexseq/firstoc-rew is used by theoremx-atmost-h, precedes-ascsubseq-2, ordered-precedes,
list/indexseq-stackseq/lastdiv-rew is used by theoremx-atleast-ind,
list/indexseq/Last is used by theoremx-atleast-ind, theoremx-atleast,
list/Last is used by solixh-to-solitaireh, pushix-to-push,
list/indexseq-stackseq/Last is used by theoremx-atleast-ind, precedesex-rev-rec1,
list/indexseq/Nil is used by theoremx-atmost-h, theoremx-atleast-ind, precedes-ascsubseq-2-h, ordered-precedes-h, ascsubseq-rem, ascsubseq-nodups, ascsubseq-append,
list/Nil is used by solix-to-solitaire,
list/indexseq-stackseq/Nil is used by theoremx-atleast-ind, pushx-nonrec, precedesex-rev-rec1, inv-butlast,
list/indexseq/a is used by tolist-cut-seq, theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushx-covers, pushix-to-push, precedesex-pushix, precedes-ascsubseq-2-h, precedes-ascsubseq-2, ordered-precedes-h, ordered-precedes, coversi-empty, covers-rem, ascsubseq-rest-notprec-first, ascsubseq-rem, ascsubseq-prepend, ascsubseq-nodups, ascsubseq-in-size, ascsubseq-first-notin-rest, ascsubseq-empty, ascsubseq-append, ascsubseq-2, allls-incbound, allls-in,
list/stackseq/a is used by tolistl-single, tolistl-cut-seq, tolist-size, pushix-to-push,
list/indexseq-stackseq/a is used by tolistl-cut-seq, tolist-size, theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushx-covers, pushix-to-push, precedesex-rev-rec1, precedesex-pushix, precedesex-prepend, precedesex-append, precedesex-2, orderedl-at, inv-last-nonempty, inv-incbound, inv-butlast, coversi-append, covers-rem,
list/a is used by tolistl-cut-seq, tolist-single, tolist-cut-seq, solixh-to-solitaireh, solix-to-solitaire, pushx-inv, pushx-cut-seq, pushix-to-push, precedesex-append, precedes-append,
list/indexseq/app is used by theoremx-atmost-h, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushix-to-push, precedesex-pushix, ascsubseq-rest-notprec-first, ascsubseq-rem, ascsubseq-prepend, ascsubseq-in-size, ascsubseq-first-notin-rest, ascsubseq-empty, ascsubseq-2,
list/stackseq/app is used by tolistl-single, pushix-to-push,
list/indexseq-stackseq/app is used by pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushix-to-push, precedesex-pushix, precedesex-prepend, precedesex-append, precedesex-2, orderedl-at, inv-last-nonempty,
list/app is used by tolist-single, solixh-to-solitaireh, pushix-to-push,
list/app-01 is used by tolist-cut-seq,
list/stackseq/app-01 is used by tolistl-cut-seq, pushix-to-push,
list/indexseq-stackseq/app-01 is used by pushx-nonrec, pushx-cut-seq,
list/indexseq/app-02-ant is used by theoremx-atmost-h,
list/indexseq/c is used by tolist-cut-seq, theoremx-atleast, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushx-covers, pushix-to-push, precedesex-pushix, precedes-ascsubseq-2-h, ordered-precedes-h, coversi-empty, ascsubseq-rest-notprec-first, ascsubseq-rem, ascsubseq-prepend, ascsubseq-nodups, ascsubseq-in-size, ascsubseq-first-notin-rest, ascsubseq-empty, ascsubseq-append, ascsubseq-2, allls-incbound, allls-in,
list/c is used by tolist-single, tolist-cut-seq, solixh-to-solitaireh, pushix-to-push,
list/indexseq-stackseq/c is used by tolistl-cut-seq, tolist-size, theoremx-atmost-h, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushix-to-push, precedesex-rev-rec1, precedesex-pushix, precedesex-prepend, precedesex-append, orderedl-at, inv-last-nonempty, inv-incbound, inv-butlast,
list/stackseq/c is used by tolistl-single, tolistl-cut-seq, tolist-size, pushix-to-push,
list/indexseq-stackseq/c-03 is used by precedesex-pushix,
list/c-04 is used by tolist-single,
list/indexseq-stackseq/c-04 is used by pushx-nonrec, pushx-cut-seq,
list/stackseq/c-04 is used by tolistl-single, pushix-to-push,
list/indexseq-stackseq/c-06 is used by precedesex-pushix,
list/indexseq-stackseq/c-07 is used by orderedl-at, coversi-append, covers-rem,
list/indexseq/c-08 is used by pushx-cut-seq,
list/c-08 is used by pushix-to-push,
list/indexseq/e is used by pushx-inv-gen, pushx-inv,
list/indexseq/e-01 is used by pushx-ordered, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushix-to-push, precedesex-pushix, coversi-empty, ascsubseq-empty,
list/indexseq-stackseq/e-01 is used by orderedl-at, inv-last-nonempty, coversi-append, covers-rem,
list/indexseq/e-03 is used by theoremx-atmost-h,
list/indexseq/in-01 is used by theoremx-atmost-h, precedes-ascsubseq-2,
list/indexseq/in-06 is used by pushx-covers,
list/indexseq/in-08 is used by theoremx-atleast,
list/indexseq/in-12 is used by ascsubseq-nodups,
list/indexseq-stackseq/in-14 is used by precedesex-pushix,
list/indexseq/in-14 is used by theoremx-atleast, precedesex-pushix,
list/indexseq-stackseq/in-15 is used by pushx-covers,
list/indexseq/in-17 is used by theoremx-atmost-h, theoremx-atleast, pushx-covers, precedesex-pushix, ordered-precedes, coversi-empty, covers-rem, ascsubseq-rest-notprec-first, ascsubseq-nodups, ascsubseq-in-size, ascsubseq-first-notin-rest, allls-in,
list/indexseq-stackseq/in-17 is used by pushx-covers, precedesex-pushix,
list/indexseq-stackseq/in-append is used by pushx-covers, precedesex-pushix,
list/indexseq/in-append is used by theoremx-atmost-h, theoremx-atleast, pushx-covers, precedesex-pushix, precedes-ascsubseq-2, ordered-precedes, coversi-empty, covers-rem, ascsubseq-rest-notprec-first, ascsubseq-nodups, ascsubseq-in-size, ascsubseq-first-notin-rest, allls-in,
list/indexseq/in-empty is used by coversi-empty, ascsubseq-rest-notprec-first, ascsubseq-nodups, ascsubseq-in-size, ascsubseq-first-notin-rest, allls-in,
list/stackseq/len is used by tolist-size,
list/indexseq/len is used by theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast,
list/indexseq-stackseq/len is used by tolist-size, theoremx-atmost-h, theoremx-atleast-ind, pushx-nonrec, pushx-covers, orderedl-at, coversi-append, covers-rem,
list/len is used by solixh-to-solitaireh, precedes-append,
list/indexseq-stackseq/len-02 is used by tolist-size, theoremx-atmost-h, theoremx-atleast-ind, pushx-nonrec, pushx-covers, orderedl-at, coversi-append, covers-rem,
list/stackseq/len-02 is used by tolist-size,
list/len-02 is used by solixh-to-solitaireh, precedes-append,
list/indexseq/len-02 is used by theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast,

Used from specification list-data

list-data/indexseq/elim-list-c is used by theoremx-atleast, pushx-ordered, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushix-to-push, precedesex-pushix,
list-data/l is used by tolist-cut-seq, solixh-ordered, solixh-inv, solixh-covers, pushx-ordered, pushx-nonrec, pushx-inv-gen, pushx-inv, pushx-cut-seq, pushx-covers, pushix-to-push, precedesex-solixh, precedesex-pushix, precedes-trans, precedes-irrefl, precedes-append, ascsubseq-rem, ascsubseq-in-size,
list-data/indexseq/l is used by theoremx-atmost-h, theoremx-atleast-ind, theoremx-atleast, theoremx,
list-data/indexseq-stackseq/l is used by theoremx-atmost-h, theoremx-atleast, theoremx, pushx-nonrec, pushx-covers, orderedl-at, coversi-append, covers-rem,
list-data/stackseq/size-01 is used by tolist-size,
list-data/size-01 is used by solix-to-solitaire, ascsubseq-empty,
list-data/indexseq/size-01 is used by theoremx-atmost-h,
list-data/indexseq-stackseq/size-01 is used by tolist-size, theoremx-atleast-ind, theoremx-atleast, orderedl-at, coversi-empty, covers-empty,

Used from specification list-last

list-last/indexseq-stackseq/butlast-last is used by theoremx-atleast,
list-last/indexseq-stackseq/l is used by inv-last-nonempty,
list-last/indexseq-stackseq/l-02 is used by inv-last-nonempty,
list-last/indexseq-stackseq/lb is used by theoremx-atleast,

Used from specification nat

nat/anti is used by solixh-ordered, solixh-inv, solixh-covers, pushx-covers, precedesex-solixh,
nat/ax-02 is used by pushx-ordered, ordered-precedes-h,
nat/elim-pred-c is used by theoremx-atleast, orderedl-at, coversi-append, covers-rem,
nat/elim-sub is used by solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh,
nat/fle is used by ordered-precedes-h, ascsubseq-rem, ascsubseq-in-size, allls-in,
nat/fle-01 is used by pushx-covers, ordered-precedes-h, ascsubseq-in-size, allls-incbound,
nat/ge is used by theoremx,
nat/le-ls-simp is used by ordered-precedes-h, ascsubseq-rem, allls-in,
nat/lels is used by theoremx-atleast-ind, theoremx, solixh-ordered, solixh-inv, solixh-covers, pushx-ordered, pushx-covers, precedesex-solixh, orderedl-at, ordered-precedes-h, coversi-append, covers-rem, covers-ascsubseq, ascsubseq-rem, ascsubseq-append, ascsubseq-2, allls-incbound,
nat/lels-01 is used by theoremx,
nat/lels-02 is used by theoremx,
nat/lels-03 is used by solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh,
nat/ler is used by pushx-covers,
nat/lez is used by theoremx, solix-ordered, solix-inv, solix-covers, precedesex-solix, orderedl-at, coversi-append, covers-rem,
nat/lez-01 is used by orderedl-at,
nat/ls-le-simp is used by theoremx, solixh-ordered, solixh-inv, solixh-covers, pushx-ordered, pushx-covers, precedesex-solixh, ascsubseq-2,
nat/succ-01 is used by solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh, orderedl-at, coversi-append, covers-rem,
nat/zero-02 is used by solixh-ordered, solixh-inv, solixh-covers, precedesex-solixh,