import set.Predicate as P;
import set.Truth as T;
import func.Function as F;
import set.R;
import set.N;
import set.parts;
import set.Finite;
import lim.infty;

ax rec = (
    p in P;
    init in N;
    p(init);
    n in [init;infty[ => (
        p n => (p (n+1))
    )
) => (
    n in [init; infty[ => (p n)
);
ax triangle_inequality = a,b in R => abs (a+b) <= (abs a + (abs b));

let f in F(R, R);
let alpha in [0; 1[;
let u in F(R, N);

// axioms
ax ax1 = f is func.Continuous;
ax ax2 = (x,y) in R^2 => (
    abs (f x - (f y)) <= (alpha * (abs (x-y)))
);
ax ax3 = u(0) = 0;
ax ax4 = n in N => (
    u (n+1) = (f (u n));
    abs (u (n+1) - (u n)) <= (alpha^n * (abs (u 1)))
);

let n,p in N;
ax a6 = n <= p;

let x = u(p)-u(n);

x = sum (k in [|n,p-1|]) (u(k+1)-u(k)) : {
    rec
        (
            l in N => (
                u(l+1)-u(n) = sum(k in [|n, l|], u(k+1)-u(k))
            )
        )
        n
        _
        (
            l in [init;infty[ => (
                let rec_p = u(l+1)-u(n) = sum(k in [|n, l|], u(k+1)-u(k));
                rec_p => u(l+2)-u(n) = sum(k in [|n, l+1|], u(k+1)-u(k)) : {
                    let x = u(l+2)-u(n);
                    x = u(l+2)-u(l+1) + u(l+1)-u(n);
                    x = u(l+2)-u(l+1) + sum(k in [|n, l|], u(k+1)-u(k)) : {rec_p};
                    x = sum(k in [|n, l+1|], u(k+1)-u(k))
                }
            )
        )
}

// TODO : Finish this example

abs x <= (sum (k in [|n, p-1|]) (abs (u (k+1) - (u k)))) : {
    rec
        (
            l in N => abs (sum (k in [|n,p-1|]) (u(k+1)-u(k)))
        )
}