Rational

lang

Real

lang

RedBlackTree

spec

RedTree

RedBlackTree

RelReasoning

proof

Right

lang

r

Node WithProof WithRel

rebalance

AVLTreeOps

reciprocal

Rational

reflexivity

AHeap

remove

DistinctList DistinctListOps

removeFirst

List

replace

List List PList

replaceAt

List List

resize

BoundedArray

reverse

List List PList

reverseAppend

ListSpecs ListLemmas

reverseIndex

ListSpecs ListLemmas

reverseReverse

ListSpecs ListLemmas

reverse_prefix

ListLemmas

right

Oracle AHeap Node Node BlackTree Leaf RedTree Tree

rightHeight

LeftistHeap

rightRotation

AVLTreeOps

rightUnitAppend

ListSpecs ListLemmas

rk

Node

rotate

List List PList MapArray

rotate_perm

PermutationLemmas

rotate_toList

MapArrayLemmas

runState

State