lemma ex_1a(x: int, y: int) 
    ensures 5*x - 3 * (y + x) == 2*x - 3*y
{
    calc {
        5 * x -3 * (y + x);
    ==  // Distributivity of Multiplication
        5 * x -3 * y - 3 * x;
    == // Commutativity
        5 * x - 3 * x - 3 * y;
    == // Addition
        2 * x - 3*y;
    }
}
lemma ex_1b(x: int, y: int) 
    ensures 2 * (x + 4*y + 7) - 10 == 2*x + 8*y + 4
{
    calc {
        2 * (x + 4*y + 7) - 10;
    == // Distributivity of Multiplication
        2 * x + 2 * 4 * y + 2 * 7 - 10;
    == // Multiplication of integers
        2 * x + 8 * y + 14 - 10;
    == // Addition of integers
        2*x + 8*y + 4;
    }
}

lemma ex_1c(x: int, y: int) 
    ensures 7*x + 5 < (x + 3) * (x + 4)
    {
    calc {
        7*x + 5;
    < 
        7*x + 12;
    <= {assert x * x >= 0;}
        7*x + 12 + x * x;
    ==
        x * x + 3 * x + 4 * x + 12;
    ==
        (x + 3) * (x + 4);
    }
}

// E5.6

function Ack(m: nat, n: nat): nat
    decreases m, n
{
    if m == 0 then
        n + 1
    else if n == 0 then
        Ack(m - 1, 1)
    else
        Ack(m - 1, Ack(m, n - 1))
}

lemma {:induction false} IncreasingAck(n: nat)
    ensures Ack(1, n) == n + 2
{
    if n == 0 {
        calc {
            Ack(1, n);
        ==
            Ack(0, 1);
        ==
            2;
        }
    } else {
        calc {
            Ack(1, n);
        == // last else branch of Ack
            Ack(0, Ack(1, n - 1));
        == { IncreasingAck(n - 1);}
            Ack(0, n - 1 + 2);
        ==
            Ack(0, n + 1);
        ==
            n + 1 + 1;
        ==
            n + 2;
        }
    }
}