SortedListTakeLemmas

Value Members

1. final def !=(arg0: AnyRef): Boolean

   Definition Classes

   AnyRef

2. final def !=(arg0: Any): Boolean

   Definition Classes

   Any

3. final def ##(): Int

   Definition Classes

   AnyRef → Any

4. final def ==(arg0: AnyRef): Boolean

   Definition Classes

   AnyRef

5. final def ==(arg0: Any): Boolean

   Definition Classes

   Any

6. final def asInstanceOf[T0]: T0

   Definition Classes

   Any

7. def clone(): AnyRef

   Attributes

   protected[java.lang]

   Definition Classes

   AnyRef

   Annotations

   @throws( ... )

8. final def eq(arg0: AnyRef): Boolean

   Definition Classes

   AnyRef

9. def equals(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

10. def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

11. def foldl_insert_2(list0: List[BigInt], list: List[BigInt]): Boolean

12. def foldl_insert_3(list0: List[BigInt], list: List[BigInt], n: BigInt): Boolean

    WARNING: Leon takes 10+ seconds to verify this lemma on my desktop.

13. def foldl_insert_lemma(list0: List[BigInt], list: List[BigInt], n: BigInt): Boolean

14. final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

15. def hashCode(): Int

    Definition Classes

    AnyRef → Any

16. def insert_comm_lemma(list: List[BigInt], e1: BigInt, e2: BigInt, n: BigInt): Boolean

17. def insert_merge(list: List[BigInt], e: BigInt, n: BigInt): Boolean

18. def insert_merge_perm(list: List[BigInt], e: BigInt): Boolean

    Annotations

    @induct()

19. final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

20. def list_decomp(list0: List[BigInt], list: List[BigInt]): Boolean

    Annotations

    @induct()

21. def merge_assoc_lemma(l1: List[BigInt], l2: List[BigInt], l3: List[BigInt], n: BigInt): Boolean

22. def merge_comm_lemma(l1: List[BigInt], l2: List[BigInt], n: BigInt): Boolean

23. def min_delete(l: List[BigInt]): Boolean

    Annotations

    @induct()

24. final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

25. final def notify(): Unit

    Definition Classes

    AnyRef

26. final def notifyAll(): Unit

    Definition Classes

    AnyRef

27. def permutation_first_last_swap(list: List[BigInt], e: BigInt): Boolean

    Annotations

    @induct()

28. def sort_cons_sort(list: List[BigInt], e: BigInt): Boolean

29. def sort_tail(l: List[BigInt]): Boolean

30. def sort_take_concat(l1: List[BigInt], l2: List[BigInt], n: BigInt, m: BigInt): Boolean

31. def sort_take_concat_decomp_l(l1: List[BigInt], l2: List[BigInt], n: BigInt, m: BigInt): Boolean

32. def sort_take_concat_decomp_r(l1: List[BigInt], l2: List[BigInt], n: BigInt, m: BigInt): Boolean

33. def sort_take_concat_more(l1: List[BigInt], l2: List[BigInt], n: BigInt, m: BigInt, r: BigInt, i: BigInt, j: BigInt): Boolean

34. def sort_take_concat_norm(l1: List[BigInt], l2: List[BigInt], n: BigInt, m: BigInt, r: BigInt): Boolean

35. def sort_take_concat_sort_take(l1: List[BigInt], l2: List[BigInt], n: BigInt, m: BigInt, r: BigInt): Boolean

36. def sort_take_cons_sort_take(list: List[BigInt], e: BigInt, n: BigInt): Boolean

37. def sort_take_decomp(l: List[BigInt], n: BigInt): Boolean

38. def sort_take_idempotent(l: List[BigInt], n: BigInt): Boolean

39. def sort_take_min(l: List[BigInt], n: BigInt): Boolean

40. def sort_take_perm_eq(l1: List[BigInt], l2: List[BigInt], n: BigInt): Boolean

41. def sort_take_sorted(l: List[BigInt], n: BigInt): Boolean

42. final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

43. def take_all(l: List[BigInt], n: BigInt): Boolean

44. def take_delete(l: List[BigInt], n: BigInt, x: BigInt): Boolean

45. def take_idempotent(l: List[BigInt], n: BigInt): Boolean

46. def take_n_m(l: List[BigInt], n: BigInt, m: BigInt): Boolean

47. def toString(): String

    Definition Classes

    AnyRef → Any

48. final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

49. final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

50. final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )