Provable-Programming-exercises/chap_3/e3_1.dfy

function F(x: int): int 
    decreases x
{
    if x < 10 then x else F(x - 1)
}

function G(x: int): int 
    decreases x
{
    if 0 <= x then G(x - 2) else x
}

function H(x: int): int 
    decreases x + 60
{
    if x < -60 then x else H(x - 1)
}

function I(x: nat, y: nat): int 
    decreases x + y
{
    if x == 0 || y == 0 then
        12
    else if x % 2 == y % 2 then
        I(x - 1, y)
    else   
        I(x, y - 1)
}

function J(x: nat, y: nat): int 
    decreases x, y
{
    if x == 0 then
        y
    else if y == 0 then
        J(x - 1, 3)
    else
        J(x, y - 1)
}

function K(x: nat, y: nat, z: nat): int 
    decreases x, y, z
{
    if x < 10 || y < 5 then
        x + y
    else if z == 0 then 
        K(x - 1, y, 5)
    else
        K(x, y - 1, z - 1)
}

function L(x: int): int 
    decreases 100 - x
{
    if x < 100 then L(x+1) + 10 else x
}

function G'(n: nat): nat 
    decreases n
{
    if n == 0 then 0 else n - G'(G'(n - 1))
}