s.dfy

function power(x: int, y: int) : int
    requires y >= 0
    decreases y
{
    if y == 0 then 1
    else if y % 2 == 0 then power(x * x, y / 2)
    else x * power(x * x, (y - 1) / 2)
}

lemma PowerOddLemma(x: int, y: int)
    requires y > 0 && y % 2 == 1
    ensures power(x, y) == x * power(x, y - 1)
{}

lemma PowerEvenLemma(x: int, y: int)
    decreases y
    requires y > 0 && y % 2 == 0
    ensures power(x, y) == x * power(x, y - 1)
{
    calc {
        x * power(x, y - 1);
        x * x * power(x * x , (y - 2) / 2);
        x * x * power(x * x, y / 2  - 1);
    }
    if (y / 2) % 2 == 0 {
        PowerEvenLemma(x * x, y / 2);
    }
    else {
        PowerOddLemma(x * x, y / 2);
    }
}

lemma PowerLemma(x: int, y: int)
  requires y > 0
  ensures power(x, y) == x * power(x, y - 1)
{
    if y % 2 == 0 { PowerEvenLemma(x, y); }
    else { PowerOddLemma(x, y); }
}

lemma PowerSumLemma(x: int, y: int, z: int)
  requires y >= 0 && z >= 0
  ensures power(x, y) * power(x, z) == power(x, y + z)
{
    if y == 0 {}
    else {
        PowerSumLemma(x, y - 1, z);
        calc {
            power(x, y) * power(x, z);
            { PowerLemma(x, y); }
            x * power(x, y - 1) * power(x, z);
            x * power(x, y + z - 1);
            { PowerLemma(x, y + z); }
            power(x, y + z);
        }
    }
}

lemma PowerSumOriginalLemma(x: int, y: int)
    requires y >= 0
    ensures forall a :: 0 <= a <= y ==> power(x, y) == power(x, a) * power(x, y - a)
{
    forall a | 0 <= a <= y ensures power(x, y) == power(x, a) * power(x, y - a)
    {
         PowerSumLemma(x, a, y - a);
    }
}