Set
lang
SetAggregationProof
spec
SetLemmas
proof
SetMapLemmas
spec
SetMapSpec
spec
SetOps
collection
Some
lang
SortedListLemmas
proof
SortedListOps
proof
SortedListSpec
proof
SortedListTakeLemmas
proof
SortedListTakeOps
proof
SortedListTakeSpec
proof
SpecsDecorations
lang
State
state
StrOps
lang
scanLeft
List
List
PList
scanRight
List
List
PList
scanVsFoldLeft
ListSpecs
ListLemmas
scanVsFoldRight
ListSpecs
ListLemmas
script
isabelle
sequence
State
set
SetOps
setExists
collection
setForall
collection
setToList
collection
set_exists
SetLemmas
set_filter
SetLemmas
set_forall
SetLemmas
set_min
SetLemmas
set_sort
SetLemmas
set_union_lemma
PrimitiveDataTypeSpec
set_vector_add_lemma
PrimitiveDataTypeSpec
shift
ListArray
shift_append_eq
ListArrayLemmas
shift_drop_eq
ListArrayLemmas
size
List
Set
List
PList
SetOps
ArrayHeap
ArrayList
ArrayQueue
ArrayStack
BoundedArray
HeapADT
IntSet
Iterator
HeapNode
LinkedList
ListADT
ListArray
ListHeap
ListIterator
ListQueue
ListStack
MapArray
MapArrayList
RedBlackTree
TreeSet
size_bisim
ArrayHeapListHeapBisim
LinkedListArrayListBisimulation
LinkedListMapArrayListBisimulation
size_invariant
LeftistHeapSpec
slice
List
List
PList
ListArray
slice_all
ListLemmas
sll
BoundedArray
snoc
MapArray
snocAfterAppend
ListSpecs
ListLemmas
snocFoldRight
ListSpecs
ListLemmas
snocIndex
ListSpecs
ListLemmas
snocIsAppend
ListSpecs
ListLemmas
snocLast
ListSpecs
ListLemmas
snocReverse
ListSpecs
ListLemmas
snoc_forall
MapArrayLemmas
snoc_toList
MapArrayLemmas
sort
SortedListOps
sort_assoc_lemma
SortedListLemmas
sort_associative_prop
SortedListSpec
sort_commutative_prop
SortedListSpec
sort_cons_delete
SortedListLemmas
sort_cons_sort
SortedListTakeLemmas
sort_delete_lemma
SortedListLemmas
sort_head_min
SortedListSpec
sort_idempotent_prop
SortedListSpec
sort_not_contains_lemma
SortedListLemmas
sort_permutation
SortedListLemmas
sort_permutation_prop
SortedListSpec
sort_sorted
SortedListLemmas
sort_tail
SortedListTakeLemmas
sort_take
SortedListTakeOps
sort_take_concat
SortedListTakeLemmas
sort_take_concat_decomp_l
SortedListTakeLemmas
sort_take_concat_decomp_r
SortedListTakeLemmas
sort_take_concat_more
SortedListTakeLemmas
sort_take_concat_norm
SortedListTakeLemmas
sort_take_concat_sort_take
SortedListTakeLemmas
sort_take_cons_sort_take
SortedListTakeLemmas
sort_take_decomp
SortedListTakeLemmas
sort_take_idempotent
SortedListTakeLemmas
sort_take_min
SortedListTakeLemmas
sort_take_perm_eq
SortedListTakeLemmas
sort_take_sorted
SortedListTakeLemmas
sorted
ListOps
sorted_take
SortedListTakeOps
span
List
spec
libref
split
List
List
splitAt
List
List
splitAtIndex
List
srl
BoundedArray
state
monads
State
subsetOf
Set
substring
StrOps
suffix_tran
ListLemmas
sugar
proof
swap
Either
Left
Right
IMap
MapArray
swap_defined_between
IMap
swap_toList_append
IMap
swap_toList_comm
IMap
swap_toList_contains
IMap
swap_toList_contains_strict
IMap
swap_toList_eq
IMap
swap_toList_perm
IMap
MapArrayLemmas
synthesis
lang