[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 array-copy
- array-copy/at-subarray
is used by
lexicographic-suffix-next,
- array-copy/subarray-subarray-elim
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- array-copy/at-subarray
is used by
ls-at-subarray,
- array-copy/size-subarray
is used by
suffix-same,
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- array-copy/subarray-elim
is used by
lexicographic-total,
lexicographic-suffix-next,
lexicographic-emparray,
array-exists-first-neq,
- array-copy/subarray-zero
is used by
suffix-end,
lexicographic-suffix-next,
lexicographic-emparray,
array-exists-first-neq,
Used from specification nat-basic1
- nat-basic1/gearray/f
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/lf
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/lf-01
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/lf-02
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/ls-02
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/ls-03
is used by
lexicographic-suffix-next,
- nat-basic1/gearray/neq-01
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/one-01
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/ref-1
is used by
suffix-same,
suffix-end,
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/trans-1
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic1/gearray/zero
is used by
lexicographic-suffix-next,
- nat-basic1/gearray/zero-01
is used by
lexicographic-suffix-next,
Used from specification oelem
- oelem/irreflexivity
is used by
lexicographic-trans,
lexicographic-suffix-next,
lexicographic-irrefl,
- oelem/lel
is used by
lexicographic-trans,
lexicographic-suffix-next,
- oelem/nen
is used by
lexicographic-trans,
lexicographic-suffix-next,
- oelem/nll
is used by
lexicographic-trans,
- oelem/sls
is used by
lexicographic-total,
lexicographic-suffix-next,
- oelem/transitivity
is used by
lexicographic-trans,
lexicographic-suffix-next,
Used from specification array
Used from specification nat
- nat/add-01
is used by
lexicographic-suffix-next,
- nat/anti
is used by
lexicographic-trans,
lexicographic-total,
array-exists-first-neq,
- nat/ax-02
is used by
lexicographic-trans,
lexicographic-total,
lexicographic-suffix-next,
lexicographic-irrefl,
- nat/cancel-01
is used by
lexicographic-suffix-next,
- nat/elim-pred-c
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat/elim-sub
is used by
suffix-same,
lexicographic-suffix-next,
- nat/eq
is used by
lexicographic-suffix-next,
- nat/eq-02
is used by
lexicographic-suffix-next,
- nat/eq-add2n-1-eq-le
is used by
lexicographic-suffix-next,
- nat/eqle-one
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat/fle
is used by
lexicographic-trans,
lexicographic-suffix-next,
- nat/fle-01
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/l-num-06
is used by
lexicographic-suffix-next,
- nat/le
is used by
lexicographic-suffix-next,
- nat/le-add
is used by
lexicographic-suffix-next,
- nat/le-ls-simp
is used by
suffix-same,
lexicographic-trans,
lexicographic-suffix-next,
lexicographic-irrefl,
array-exists-first-neq,
- nat/le-sum
is used by
lexicographic-suffix-next,
- nat/lels
is used by
lexicographic-trans,
lexicographic-total,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/lels-01
is used by
suffix-same,
suffix-end,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/lels-02
is used by
lexicographic-trans,
lexicographic-total,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/lels-03
is used by
lexicographic-trans,
lexicographic-suffix-next,
- nat/lep
is used by
suffix-same,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/lep-02
is used by
suffix-same,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/ler
is used by
lexicographic-trans,
lexicographic-total,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/let
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/lez
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat/lez-01
is used by
lexicographic-emparray,
array-exists-first-neq,
- nat/ls
is used by
lexicographic-suffix-next,
- nat/ls-01
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat/ls-02
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat/ls-03
is used by
lexicographic-suffix-next,
- nat/ls-le-simp
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat/neq-add1
is used by
lexicographic-suffix-next,
- nat/succ-01
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat/zero
is used by
suffix-end,
Used from specification nat-basic2
- nat-basic2/addex
is used by
lexicographic-suffix-next,
- nat-basic2/a
is used by
suffix-same,
ls-at-subarray,
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic2/ax-08
is used by
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic2/c
is used by
suffix-same,
ls-at-subarray,
lexicographic-trans,
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic2/eq
is used by
array-exists-first-neq,
- nat-basic2/eq-01
is used by
suffix-same,
lexicographic-suffix-next,
- nat-basic2/eqs
is used by
lexicographic-suffix-next,
- nat-basic2/l
is used by
lexicographic-suffix-next,
- nat-basic2/l-01
is used by
lexicographic-suffix-next,
- nat-basic2/l-02
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic2/l-07
is used by
lexicographic-suffix-next,
- nat-basic2/neq-01
is used by
lexicographic-suffix-next,
- nat-basic2/one
is used by
lexicographic-suffix-next,
- nat-basic2/oz
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic2/s
is used by
lexicographic-suffix-next,
array-exists-first-neq,
- nat-basic2/succ
is used by
lexicographic-trans,
lexicographic-suffix-next,