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