[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 challenge1
Status:
Proved!
Axioms: 22, User Theorems: 44 (Proved: 44, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 796, Interactions: 283
EndIncreasingPart-base(0,0)
array-le-same-prefix3(2,0)
array-split-into-subarrays(9,2)
lexicographic-base1(0,0)
next-perm(36,6)
ordered-append(7,3)
ordered-smallerPerms(3,1)
rev-subarray-split-last-swap(50,15)
subarray-write-above(5,1)
EndIncreasingPart-rec(0,0)
array-le-same-prepart(13,5)
ascending-order-is-min-permuted(19,9)
lexicographic-base2(0,0)
next-perm-greaterPerms(14,5)
ordered-arraylist-append-last(6,3)
ordered-step-down(8,4)
rev-subarray-split-step(56,22)
toSet(0,0)
all-perms(0,0)
array-le-same-prepart2(7,3)
descending-order-is-max-permuted(20,10)
lexicographic-base3(0,0)
next-perm-smallerPerms(14,5)
ordered-arraylist-base0(0,0)
perm-all-perms-eq(8,3)
smaller-perms(0,0)
array-le-kill-prefix(35,18)
array-le-split(2,0)
get-rev(14,4)
lexicographic-rec1(0,0)
next-permutation(0,0)
ordered-arraylist-base1(0,0)
permut(0,0)
sort-def(0,0)
array-le-one-diffrent-position(35,12)
array-le-swap(11,5)
greater-perms(0,0)
max-smaller-perms-all-perms(5,2)
next-proper-permutation(167,52)
ordered-arraylist-rec(0,0)
permut-correct(51,22)
subarray-inc(7,3)
array-le-refl(2,1)
array-le-trans(15,4)
hasGreaterElem-base(0,0)
maximum-permutation(0,0)
nil-toSet(3,1)
ordered-arraylist-two(2,1)
remains-ordered-by-swap(55,19)
subarray-inc-offset(11,4)
array-le-same-prefix(9,2)
array-neg-le-eq(8,2)
hasGreaterElem-rec1(0,0)
minimum-permutation(0,0)
not-ordered(8,4)
ordered-notsmaller(5,4)
rev-mkarray-empty(3,1)
subarray-inc-offset0(14,5)
array-le-same-prefix2(6,2)
array-neg-le-eq-2(9,2)
hasGreaterElem-rec2(0,0)
next(0,0)
ordered-all-rev(24,10)
ordered-size-smaller-one(2,0)
rev-subarray-last(11,4)
subarray-prefix-fistn(5,2)