DeleteLemmas
proof
DeleteOps
proof
DistinctLemmas
proof
DistinctList
proof
DistinctListOps
proof
DistinctOps
proof
DistinctSortedListLemmas
spec
DistinctSortedListOps
spec
DistinctSortedListSpec
spec
Dummy
lang
defined_between_at
IMap
defined_between_shrink
IMap
defined_between_tran
IMap
delete
PairList
PList
DeleteOps
AVLTreeOps
IntSet
RedBlackTree
TreeSet
deleteAll
PList
deleteFirst
PList
deleteLast
PList
deleteMax
AVLTreeOps
IntSet
TreeSet
deleteMin
AHeap
AVLTreeOps
ArrayHeap
HeapADT
IntSet
LeftistHeapOps
ListHeap
TreeSet
deleteMin_bisim
ArrayHeapListHeapBisim
deleteMin_invariant
LeftistHeapSpec
deleteMin_op
AHeap
deleteMin_perm
AHeap
deleteMin_root
AHeap
deleteMin_toList_perm
AHeap
delete_comm
DeleteLemmas
PairListLemmas
delete_concat
DeleteLemmas
PairListLemmas
delete_concat_left
DeleteLemmas
delete_concat_perm1
PermutationLemmas
delete_concat_perm2
PermutationLemmas
delete_concat_right
DeleteLemmas
delete_contains
DeleteLemmas
PairListLemmas
delete_contains_distinct
DistinctLemmas
delete_contains_uniquate
ListSetLemmas
delete_content
DeleteLemmas
PairListLemmas
delete_distinct_assoc
DistinctLemmas
delete_neq_contains
DistinctLemmas
ListSetLemmas
delete_neq_not_contains
DistinctLemmas
ListSetLemmas
delete_not_contains
DeleteLemmas
delete_permutation
PermutationLemmas
delete_uniquate_assoc
ListSetLemmas
denominator
Rational
depth
Leaf
Node
TreeNode
dequeue
ArrayQueue
ListQueue
descendant_is_larger
AHeap
deterministic_lemma
DistinctSortedListLemmas
diff
List
disjoint_by_pred
PairListLemmas
distinct
List
PairList
DistinctOps
ListSetLemmas
distinct_concat_assoc_perm
DistinctLemmas
distinct_concat_comm_perm
DistinctLemmas
distinct_concat_perm_l
DistinctLemmas
distinct_concat_perm_r
DistinctLemmas
distinct_cons
DistinctLemmas
distinct_cons_not_contains
DistinctLemmas
distinct_contains
DistinctLemmas
distinct_content_permutation
DistinctSortedListLemmas
distinct_count
ListLemmas
distinct_delete
DistinctLemmas
distinct_delete_content
DistinctLemmas
distinct_delete_content0
DistinctLemmas
distinct_delete_content_lemma
DistinctLemmas
distinct_exclusive
DistinctLemmas
distinct_idempotent
DistinctLemmas
distinct_is_distinct
DistinctLemmas
distinct_not_contains
DistinctLemmas
distinct_perm
DistinctLemmas
distinct_sorted
DistinctSortedListOps
distinct_sorted_content
DistinctSortedListLemmas
distinct_sublist
DistinctLemmas
distinct_sublist_delete_l
DistinctLemmas
distinct_sublist_delete_r
DistinctLemmas
domain
FunctionalArray
domain_in_range
BoundedArray
doubleLeftRotation
AVLTreeOps
doubleRightRotation
AVLTreeOps
double_add_lemma
PrimitiveDataTypeSpec
drop
List
List
PList
ListArray
MapArray
dropRight
List
dropWhile
List
List
PList
drop_forall
ListLemmas
drop_rotate_well_ordered
AHeap
drop_toList
MapArrayLemmas
dual
AHeap