[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
,
Theorem base summary for Specification list-perm
Status:
Proved!
Axioms: 5, User Theorems: 126 (Proved: 126, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 797, Interactions: 253
a(2,0)
del-04(20,6)
in-04(2,0)
oc-diff-01(13,2)
ocs-del-length(13,2)
papp(2,0)
perm-dups-03(3,1)
perm-rmv-in-list(7,6)
sub-del-any(14,7)
subsize(16,7)
ad(7,3)
del-05(6,2)
in-05(5,1)
oc-dups(7,1)
ocs-del1(7,1)
papp-01(2,0)
perm-e(1,0)
perm-same-prefix(2,1)
subapp(5,1)
sym(3,2)
adjoin(6,3)
del-in(2,0)
in-put(12,3)
oc-e(0,0)
ocs-del1-if(2,0)
papp-02(5,2)
perm-last-rec(7,5)
perm-shift-in2(4,2)
subapp-01(5,2)
sym-01(2,1)
app(6,1)
del1(7,1)
l(5,2)
oc-filt(13,2)
ocs-dups-ex(11,4)
papp-03(8,3)
perm-mklist(10,5)
perm-shift-out2(4,2)
subapp-02(6,2)
sym-02(2,1)
app-01(6,1)
del1-01(11,1)
msubset(0,0)
oc-filt-01(2,0)
ocs-mklist(7,3)
perm(0,0)
perm-mklist-del(9,4)
perm-switch(9,5)
subapp-03(6,2)
trans(11,4)
app-02(6,1)
delapp(13,5)
neq(2,0)
oc-n(0,0)
ocs-not-more(9,0)
perm-all(14,5)
perm-one(1,1)
rec(2,0)
subdel(6,3)
app-03(4,1)
diff(19,2)
nodups(11,4)
oc-y(0,0)
ocs-put(17,3)
perm-com1(3,1)
perm-put(12,4)
rec-01(1,1)
subdel-01(9,4)
app-04(2,1)
empty(1,0)
notin(5,1)
oc-zero(1,0)
ocs-put-01(17,3)
perm-com2(3,1)
perm-put-del1(17,7)
ref(2,1)
subdel-02(3,2)
app-05(1,0)
empty-01(2,0)
oc(3,0)
ocappend(7,1)
ocs-put-02(20,5)
perm-del(7,2)
perm-r(2,0)
rest(4,2)
subdel-03(3,2)
c(7,0)
filter(19,2)
oc-adjoin(3,1)
ocnodups(7,1)
ocs-same-length-all(11,7)
perm-del-01(14,8)
perm-rec(5,3)
shift(1,0)
subempty(1,1)
cons(1,0)
in(3,0)
oc-del(3,1)
ocnodups-01(2,0)
ocs-same-length-mklist(11,5)
perm-del-in(3,1)
perm-rev(2,0)
shift-01(1,0)
subperm(3,1)
del(10,5)
in-01(3,0)
oc-del-01(5,2)
ocone(2,0)
ocs-sw(17,8)
perm-dups(6,2)
perm-rev-01(6,5)
shift-02(10,0)
subperm-01(3,1)
del-01(2,1)
in-02(2,0)
oc-del-02(3,1)
ocs-del(1,0)
one(1,1)
perm-dups-01(3,1)
perm-rmdup-rev(6,5)
shift-03(14,8)
subrec(18,4)
del-02(11,5)
in-03(2,0)
oc-diff(2,0)
ocs-del-del1(6,1)
one-01(3,1)
perm-dups-02(3,1)
perm-rmv-in(1,0)
size-perm(11,2)
subrec-01(5,1)