libref.proof

PairListLemmas

object PairListLemmas

Annotations
@library()
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. PairListLemmas
  2. AnyRef
  3. Any
  1. Hide All
  2. Show all
Learn more about member selection
Visibility
  1. Public
  2. All

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. def concat_permutation[K, V](ll: PList[K, V], l1: PList[K, V], l2: PList[K, V]): Boolean

  9. def concat_permutation_lemma[K, V](ll: PList[K, V], l1: PList[K, V], l2: PList[K, V]): Boolean

  10. def cons_delete_perm[K, V](list: PList[K, V], e: Pair[K, V]): Boolean

  11. def cons_merge_assoc[K, V](e: Pair[K, V], list1: PList[K, V], list2: PList[K, V]): Boolean

  12. def delete_comm[K, V](list: PList[K, V], a: Pair[K, V], b: Pair[K, V]): Boolean

    Annotations
    @induct()

  13. def delete_concat[K, V](l1: PList[K, V], l2: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  14. def delete_contains[K, V](list: PList[K, V], a: Pair[K, V], b: Pair[K, V]): Boolean

    Annotations
    @induct()

  15. def delete_content[K, V](list: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  16. def disjoint_by_pred[K, V](pos: PList[K, V], neg: PList[K, V], p: (Pair[K, V]) ⇒ Boolean): Boolean

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

    Definition Classes
    AnyRef

  18. def equals(arg0: Any): Boolean

    Definition Classes
    AnyRef → Any

  19. def filter_complete[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean, e: Pair[K, V]): Boolean

    Annotations
    @induct()

  20. def filter_disjoint[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean): Boolean

  21. def filter_sound[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean, e: Pair[K, V]): Boolean

    Annotations
    @induct()

  22. def filter_union_content[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean): Boolean

  23. def filter_union_perm[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean): Boolean

  24. def filter_union_perm1[K, V](h: Pair[K, V], t: PList[K, V], pos: PList[K, V], neg: PList[K, V]): Boolean

  25. def filter_union_perm2[K, V](h: Pair[K, V], t: PList[K, V], pos: PList[K, V], neg: PList[K, V]): Boolean

  26. def filter_union_size[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean): Boolean

  27. def finalize(): Unit

    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )

  28. def forall_p_not_in[K, V](list: PList[K, V], p: (Pair[K, V]) ⇒ Boolean, e: Pair[K, V]): Boolean

    Annotations
    @induct()

  29. def getAll_contain_lemma[K, V](map: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  30. def getAll_delete_lemma[K, V](map: PList[K, V], e: Pair[K, V], key: K): Boolean

    Annotations
    @induct()

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

    Definition Classes
    AnyRef → Any

  32. def hasKey_contains[K, V](map: PList[K, V], key: K): Boolean

  33. def hashCode(): Int

    Definition Classes
    AnyRef → Any

  34. final def isInstanceOf[T0]: Boolean

    Definition Classes
    Any

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

    Definition Classes
    AnyRef

  36. final def notify(): Unit

    Definition Classes
    AnyRef

  37. final def notifyAll(): Unit

    Definition Classes
    AnyRef

  38. def permutation_append[K, V](l1: PList[K, V], l2: PList[K, V], ll: PList[K, V]): Boolean

    Annotations
    @induct()

  39. def permutation_by_tran[K, V](l1: PList[K, V], l2: PList[K, V], l3: PList[K, V]): Boolean

  40. def permutation_car_swap[K, V](list: PList[K, V], a: Pair[K, V], b: Pair[K, V]): Boolean

    Annotations
    @induct()

  41. def permutation_comm[K, V](l1: PList[K, V], l2: PList[K, V]): Boolean

  42. def permutation_comm_lemma[K, V](l1: PList[K, V], l2: PList[K, V]): Boolean

    Annotations
    @induct()

  43. def permutation_concat_assoc[K, V](l1: PList[K, V], l2: PList[K, V], l3: PList[K, V]): Boolean

  44. def permutation_concat_comm[K, V](l1: PList[K, V], l2: PList[K, V]): Boolean

  45. def permutation_cons[K, V](l1: PList[K, V], l2: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  46. def permutation_cons_tail[K, V](l1: PList[K, V], l2: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  47. def permutation_contains_lemma[K, V](l1: PList[K, V], l2: PList[K, V], e: Pair[K, V]): Boolean

  48. def permutation_content[K, V](l1: PList[K, V], l2: PList[K, V]): Boolean

  49. def permutation_content_lemma[K, V](l1: PList[K, V], l2: PList[K, V]): Boolean

    Annotations
    @induct()

  50. def permutation_delete[K, V](l1: PList[K, V], l2: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  51. def permutation_delete_cons[K, V](list: PList[K, V], e: Pair[K, V]): Boolean

  52. def permutation_delete_cons[K, V](l1: PList[K, V], h2: Pair[K, V], t2: PList[K, V]): Boolean

  53. def permutation_delete_cons[K, V](l1: PList[K, V], l2: PList[K, V]): Boolean

  54. def permutation_delete_head[K, V](t1: PList[K, V], l2: PList[K, V], h1: Pair[K, V]): Boolean

    Annotations
    @induct()

  55. def permutation_eq[K, V](s: PList[K, V], t: PList[K, V]): Boolean

  56. def permutation_filter_contains[K, V](list1: PList[K, V], list2: PList[K, V], p: (Pair[K, V]) ⇒ Boolean, x: Pair[K, V]): Boolean

  57. def permutation_getAll_lemma[K, V](map1: PList[K, V], map2: PList[K, V], key: K): Boolean

    WARNING: Leon may take 2~30 seconds to verify this lemma.

  58. def permutation_hasKey_lemma[K, V](map1: PList[K, V], map2: PList[K, V], key: K): Boolean

  59. def permutation_prefix[K, V](l1: PList[K, V], l2: PList[K, V], e: Pair[K, V]): Boolean

    Annotations
    @induct()

  60. def permutation_refl[K, V](list: PList[K, V]): Boolean

    Annotations
    @induct()

  61. def permutation_tran[K, V](l1: PList[K, V], l2: PList[K, V], l3: PList[K, V]): Boolean

  62. def permutation_tran_lemma[K, V](l1: PList[K, V], l2: PList[K, V], l3: PList[K, V]): Boolean

    Annotations
    @induct()

  63. def permutation_tran_lemma2[K, V](l1: PList[K, V], l2: PList[K, V], l3: PList[K, V], l4: PList[K, V]): Boolean

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

    Definition Classes
    AnyRef

  65. def toString(): String

    Definition Classes
    AnyRef → Any

  66. final def wait(): Unit

    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

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

    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

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

    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped