datatype Tree<T> =  Leaf(data: T)
                    | Node(left: Tree<T>, right: Tree<T>)

function Mirror<T>(t: Tree<T>): Tree<T> {
    match t
    case Leaf(_) => t
    case Node(left, right) 
        => Node(Mirror(right), Mirror(left))
}

lemma {:induction false} MirrorMirror<T>(t: Tree<T>)
    ensures Mirror(Mirror(t)) == t
{
    match t
    case Leaf(_) =>
        // trivial
    case Node(left, right) =>
        calc {
            Mirror(Mirror(Node(left, right)));
        == 
            Mirror(Node(Mirror(right), Mirror(left)));
        ==  
            Node(Mirror(Mirror(left)),Mirror(Mirror(right)));
        == {MirrorMirror(left); MirrorMirror(right);}
            Node(left, right);
        }
}

function Size<T>(t: Tree<T>): nat {
    match t
    case Leaf(_) => 1
    case Node(left, right) => Size(left) + Size(right)
}

lemma {:induction false} MirrorSize<T>(t: Tree<T>)
    ensures Size(Mirror(t)) == Size(t)
{
    match t
    case Leaf(_) =>
    case Node(left, right) =>
        calc {
            Size(Mirror(Node(left, right)));
        ==  // def. Mirror
            Size(Node(Mirror(right), Mirror(left)));
        ==  // def. Size
            Size(Mirror(right)) + Size(Mirror(left));
        == {MirrorSize(right); MirrorSize(left);}
            Size(right) + Size(left);
        == // arithmatic
            Size(left) + Size(right);
        == // def. size
            Size(Node(left, right));
        }
}

method test() {
    assert multiset([1, 2]) == multiset([2, 1]);
}

// method Seperate(a: array<int>, key: int) returns (pivot: nat)
//     requires a.Length >= 1
//     modifies a
//     ensures multiset(a[..]) == multiset(old(a[..]))
//     ensures 0 <= pivot <= a.Length
//     ensures forall i | 0 <= i < pivot :: a[i] <= key
//     ensures forall i | pivot <= i < a.Length :: key < a[i]
// {
//     var lo: nat, hi: nat := 0, a.Length - 1;
//     while lo < hi
//         decreases hi - lo
//         invariant 0 <= lo <= hi < a.Length
//         invariant forall i | 0 <= i < lo :: a[i] <= key
//         invariant forall i | hi < i < a.Length :: key < a[i]
//         invariant multiset(a[..]) == multiset(old(a[..]))
//     {
//         if a[lo] <= key {
//             lo := lo + 1;
//         } else if key < a[hi] {
//             hi := hi - 1;
//         } else {
//             assert a[lo] in multiset(a[..]);
//             assert a[hi] in multiset(a[..]);
//             a[lo], a[hi] := a[hi], a[lo];
//             assert a[lo] in multiset(a[..]);
//             assert a[hi] in multiset(a[..]);
//             lo := lo + 1;
//         }
//     }
//     pivot := lo;
// }