[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 forall-indexWhere
Status:
Proved!
Axioms: 7, User Theorems: 23 (Proved: 23, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 189, Interactions: 22
exists-append(12,0)
exists-one(2,1)
forall-1l(6,1)
forall-in-def(15,2)
indexWhere-app-split(10,0)
indexWhere-length-ls(6,1)
exists-base(0,0)
exists-rec(0,0)
forall-append(12,0)
forall-l(8,1)
indexWhere-base(0,0)
indexWhere-length-notle(8,0)
exists-forall(8,0)
filter-exists(4,0)
forall-base(0,0)
forall-one(2,1)
indexWhere-get(6,0)
indexWhere-one(4,2)
exists-get-def(19,4)
filter-forall(4,0)
forall-exists(8,0)
forall-rec(0,0)
indexWhere-le-length(2,0)
indexWhere-rec1(0,0)
exists-in-def(15,1)
filter-forall2(5,2)
forall-get-def(19,4)
forall-rmpos(6,2)
indexWhere-length-eq(8,0)
indexWhere-rec2(0,0)