/*
Addition of natural numbers.
*/

use nat;
use prev;
use z;
use s;
use 1;
use 2;
use cong;

sym add;

fn nat_add_ty : true -> (add' : nat' => nat' => nat') {
    axiom add_ty : true -> (add' : nat' => nat' => nat');
    x : true;
    let r = add_ty(x) : (add' : nat' => nat' => nat');
    return r;
}

fn nat_add_cong : true -> cong'(add') {
    axiom nat_add_cong : true -> cong'(add');
    x : true;
    let r = nat_add_cong(x) : cong'(add');
    return x;
}

fn nat_add_zero : (a : nat') -> add'(a, z') == a {
    axiom nat_add_zero : (a : nat') -> add'(a, z') == a;
    x : (a : nat');
    let r = nat_add_zero(x) : add'(a, z') == a;
    return r;
}

fn nat_add_succ : (a : nat') & (b : nat') -> add'(a, s'(b)) == s'(add'(a, b)) {
    axiom nat_add_succ : (a : nat') & (b : nat') -> add'(a, s'(b)) == s'(add'(a, b));
    x : (a : nat') & (b : nat');
    let r = nat_add_succ(x) : add'(a, s'(b)) == s'(add'(a, b));
    return r;
}

fn nat_add_eq_left : a == b -> add'(a, c) == add'(b, c) {
    use cong_eq_left;
    use nat_add_cong;
    use nat_add_ty;
    use triv;

    x : a == b;

    let add_ty = triv(nat_add_ty) : (add' : nat' => nat' => nat');
    let x2 = triv(nat_add_cong) : cong'(add');
    let r = cong_eq_left(x2, add_ty, x) : add'(a, c) == add'(b, c);
    return r;
}

fn nat_add_eq_right : a == b -> add'(c, a) == add'(c, b) {
    use cong_eq_right;
    use nat_add_cong;
    use nat_add_ty;
    use triv;

    x : a == b;

    let add_ty = triv(nat_add_ty) : (add' : nat' => nat' => nat');
    let x2 = triv(nat_add_cong) : cong'(add');
    let r = cong_eq_right(x2, add_ty, x) : add'(c, a) == add'(c, b);
    return r;
}

fn nat_add_eq_both : (a == c) & (b == d) -> add'(a, b) == add'(c, d) {
    use cong_eq_both;
    use nat_add_cong;
    use nat_add_ty;
    use triv;

    x : a == c;
    y : b == d;

    let add_ty = triv(nat_add_ty) : (add' : nat' => nat' => nat');
    let x2 = triv(nat_add_cong) : cong'(add');
    let r = cong_eq_both(x2, add_ty, x, y) : add'(a, b) == add'(c, d);
    return r;
}

fn nat_one_plus_one_equals_two : true -> add'(1', 1') == 2' {
    use eq_symmetry;
    use eq_transitivity;
    use eq_transitivity_sym;
    use nat_add_eq_both;
    use nat_add_succ;
    use nat_add_zero;
    use nat_one_eq;
    use nat_one_ty;
    use nat_succ_eq;
    use nat_two_ty;
    use nat_two_eq;
    use nat_zero_ty;
    use ty_in_left_arg;

    x : true;

    let x2 = nat_one_eq(x) : 1' == s'(z');
    let x3 = nat_one_ty(x) : (1' : nat');
    let succ_ty = ty_in_left_arg(x3, x2) : (s'(z') : nat');
    let zero_ty = nat_zero_ty(x) : (z' : nat');
    let x7 = nat_add_succ(succ_ty, zero_ty) : add'(s'(z'), s'(z')) == s'(add'(s'(z'), z'));

    let y1 = nat_add_zero(succ_ty) : add'(s'(z'), z') == s'(z');
    let y2 = nat_succ_eq(y1) : s'(add'(s'(z'), z')) == s'(s'(z'));
    let y3 = eq_transitivity(x7, y2) : add'(s'(z'), s'(z')) == s'(s'(z'));

    let x9 = nat_two_eq(x) : 2' == s'(s'(z'));
    let x16 = eq_transitivity_sym(y3, x9) : add'(s'(z'), s'(z')) == 2';
    let x17 = nat_add_eq_both(x2, x2) : add'(1', 1') == add'(s'(z'), s'(z'));

    let r = eq_transitivity(x17, x16) : add'(1', 1') == 2';
    return r;
}

fn nat_add_check_all_ty : (a : nat') & (b : nat') -> (add'(a, b) : nat') {
    x : (a : nat');
    y : (b : nat');
    use ty_app2;
    use nat_add_ty;
    use triv;
    let x2 = triv(nat_add_ty) : (add' : nat' => nat' => nat');
    let r = ty_app2(x2, x, y) : (add'(a, b) : nat');
    return r;
}

fn nat_add_from_zero_left : (a : nat') & (add'(a, z') == z') -> a == z' {
    use eq_transitivity_rev_sym;
    use nat_add_zero;

    x : (a : nat');
    y : add'(a, z') == z';

    let x2 = nat_add_zero(x) : add'(a, z') == a;
    let r = eq_transitivity_rev_sym(x2, y) : a == z';
    return r;
}

fn nat_add_from_zero_right : (a : nat') & (add'(z', a) == z') -> a == z' {
    use nat_def;
    use refl;

    x : (a : nat');
    y : add'(z', a) == z';

    let x2 = nat_def(x) : (a == z') | (prev'(a) : nat') & (a == s'(prev'(a)));
    let x3 = refl() : (a == z') => (a == z');

    lam f : (prev'(a) : nat') & (a == s'(prev'(a))) => (a == z') {
        use eq_transitivity;
        use eq_transitivity_rev_sym;
        use nat_add_eq_right;
        use nat_add_succ;
        use nat_para_eq_zero_pos;
        use nat_zero_ty;
        use triv;

        z : (prev'(a) : nat');
        z2 : a == s'(prev'(a));

        let z3 = nat_add_eq_right(z2) : add'(z', a) == add'(z', s'(prev'(a)));
        let zero_ty = triv(nat_zero_ty) : (z' : nat');
        let z4 = nat_add_succ(zero_ty, z) :
            add'(z', s'(prev'(a))) == s'(add'(z', prev'(a)));
        let z5 = eq_transitivity(z3, z4) :
            add'(z', a) == s'(add'(z', prev'(a)));
        let z5 = eq_transitivity_rev_sym(y, z5) : z' == s'(add'(z', prev'(a)));
        let z6 = nat_para_eq_zero_pos(z5) : false;
        let r = match z6 : a == z';
        return r;
    }

    let r = match x2 (x3, f) : a == z';
    return r;
}

fn nat_add_zero_left_cong : true -> cong'(sym(a, add'(z', a') == a')) {
    use cong_app;
    use cong_bin_eq_fst;
    use nat_add_cong;
    use nat_add_ty;

    x : true;

    let y = nat_add_cong(x) : cong'(add');
    let y2 = nat_add_ty(x) : (add' : nat' => nat' => nat');
    let x2 = cong_app(y, y2) : cong'(add'(z'));
    let r = cong_bin_eq_fst(x2) : cong'(sym(a, add'(z', a') == a'));
    return r;
}

fn nat_add_zero_left : (a : nat') -> add'(z', a) == a {
    use nat_ind;
    use nat_add_zero_left_cong;

    x : (a : nat');

    fn f : true -> add'(z', z') == z' {
        use nat_add_zero;
        use nat_zero_ty;

        x : true;

        let zero_ty = nat_zero_ty(x) : (z' : nat');
        let r = nat_add_zero(zero_ty) : add'(z', z') == z';
        return r;
    }
    let f2 = f() : sym(a, add'(z', a') == a')(z')^true;
    fn g : (a : nat') -> (add'(z', a) == a) => (add'(z', s'(a)) == s'(a)) {
        x : (a : nat');

        lam r : (add'(z', a) == a) => (add'(z', s'(a)) == s'(a)) {
            use eq_transitivity;
            use nat_zero_ty;
            use nat_add_succ;
            use nat_succ_eq;
            use triv;

            y : add'(z', a) == a;

            let zero_ty = triv(nat_zero_ty) : (z' : nat');
            let x2 = nat_add_succ(zero_ty, x) : add'(z', s'(a)) == s'(add'(z', a));
            let x3 = nat_succ_eq(y) : s'(add'(z', a)) == s'(a);
            let r = eq_transitivity(x2, x3) : add'(z', s'(a)) == s'(a);
            return r;
        }
        return r;
    }
    let g2 = g() : all(((add'(z', a) == a) => (add'(z', s'(a)) == s'(a)))^(a : nat'));
    let g3 = g2() : sym(p, all((p'(a) => p'(s'(a)))^(a : nat')))(
        sym(a, add'(z', a') == a'));
    let x2 = nat_ind(nat_add_zero_left_cong, f2, g3) :
        sym(a, add'(z', a') == a')(a)^(a : nat');
    let r = x2(x) : add'(z', a) == a;
    return r;
}

fn nat_sym_add_case1_cong :
    true -> cong'(sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b'))))
{
    axiom nat_sym_add_case1_cong : true ->
        cong'(sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b'))));
    x : true;
    let r = nat_sym_add_case1_cong(x) :
        cong'(sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b'))));
    return r;
}

fn nat_add_succ_right : (a : nat') & (b : nat') -> add'(s'(a), b) == s'(add'(a, b)) {

    x : (a : nat');
    y : (b : nat');

    fn f : true -> (a : nat') => add'(s'(a), z') == s'(add'(a, z')) {
        x : true;

        lam g : (a : nat') => add'(s'(a), z') == s'(add'(a, z')) {
            y : (a : nat');

            use nat_succ_ty;
            let x2 = nat_succ_ty(y) : (s'(a) : nat');
            use nat_add_zero;
            let y2 = nat_add_zero(x2) : add'(s'(a), z') == s'(a);
            let y3 = nat_add_zero(y) : add'(a, z') == a;
            use nat_succ_eq;
            let y4 = nat_succ_eq(y3) : s'(add'(a, z')) == s'(a);
            use eq_transitivity_sym;
            let r = eq_transitivity_sym(y2, y4) : add'(s'(a), z') == s'(add'(a, z'));
            return r;
        }
        return g;
    }
    let x2 = f() : sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b')))(z')^true;
    fn g : (b : nat') ->
        ((a : nat') => add'(s'(a), b) == s'(add'(a, b))) =>
        ((a : nat') => add'(s'(a), s'(b)) == s'(add'(a, s'(b))))
    {
        b_ty : (b : nat');

        lam f :
            ((a : nat') => add'(s'(a), b) == s'(add'(a, b))) =>
            ((a : nat') => add'(s'(a), s'(b)) == s'(add'(a, s'(b))))
        {
            x  : (a : nat') => add'(s'(a), b) == s'(add'(a, b));

            lam f2 : (a : nat') => add'(s'(a), s'(b)) == s'(add'(a, s'(b))) {

                a_ty : (a : nat');

                let y2 = x(a_ty) : add'(s'(a), b) == s'(add'(a, b));
                use nat_add_succ;
                let y3 = nat_add_succ(a_ty, b_ty) : add'(a, s'(b)) == s'(add'(a, b));
                use eq_transitivity_sym;
                let y4 = eq_transitivity_sym(y2, y3) : add'(s'(a), b) == add'(a, s'(b));
                use nat_succ_eq;
                let y5 = nat_succ_eq(y4) : s'(add'(s'(a), b)) == s'(add'(a, s'(b)));
                use nat_succ_ty;
                let succ_add_ty = nat_succ_ty(a_ty) : (s'(a) : nat');
                let y6 = nat_add_succ(succ_add_ty, b_ty) :
                    add'(s'(a), s'(b)) == s'(add'(s'(a), b));
                use eq_transitivity;
                let r = eq_transitivity(y6, y5) :
                    add'(s'(a), s'(b)) == s'(add'(a, s'(b)));
                return r;
            }
            return f2;
        }
        return f;
    }
    let g2 = g() : all((b : nat') -> ((a : nat') => add'(s'(a), b) == s'(add'(a, b))) =>
        ((a : nat') => add'(s'(a), s'(b)) == s'(add'(a, s'(b)))));
    let x3 = g2() : sym(p, all((p'(a) => p'(s'(a)))^(a : nat')))(
        sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b'))));

    use nat_sym_add_case1_cong;
    use nat_ind;
    let x4 = nat_ind(nat_sym_add_case1_cong, x2, x3) :
        (b : nat') -> sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b')))(b);
    let x5 = x4(y) : sym(b, (a : nat') => add'(s'(a), b') == s'(add'(a, b')))(b);
    let x6 = x5() : (a : nat') => add'(s'(a), b) == s'(add'(a, b));
    let r = x6(x) : add'(s'(a), b) == s'(add'(a, b));
    return r;
}

fn nat_add_succ_symmetry : (a : nat') & (b : nat') -> add'(s'(a), b) == add'(a, s'(b)) {

    x : (a : nat');
    y : (b : nat');

    use nat_def;
    let or_a = nat_def(x) : (a == z') | (prev'(a) : nat') & (a == s'(prev'(a)));
    let or_b = nat_def(y) : (b == z') | (prev'(b) : nat') & (b == s'(prev'(b)));

    use nat_add_succ_right;
    let x2 = nat_add_succ_right(x, y) : add'(s'(a), b) == s'(add'(a, b));
    use nat_add_succ;
    let x3 = nat_add_succ(x, y) : add'(a, s'(b)) == s'(add'(a, b));

    use eq_transitivity_sym;
    let r = eq_transitivity_sym(x2, x3) : add'(s'(a), b) == add'(a, s'(b));
    return r;
}

fn nat_add_zero_symmetry : (a : nat') -> add'(a, z') == add'(z', a) {
    use eq_transitivity_sym;
    use nat_add_zero;
    use nat_add_zero_left;

    x : (a : nat');

    let x2 = nat_add_zero(x) : add'(a, z') == a;
    let x3 = nat_add_zero_left(x) : add'(z', a) == a;
    let r = eq_transitivity_sym(x2, x3) : add'(a, z') == add'(z', a);
    return r;
}

fn nat_add_sym_symmetry_cong :
    true -> cong'(sym(a, (b : nat') => (add'(a', b) == add'(b, a'))))
{
    axiom nat_add_sym_symmetry_cong :
        true -> cong'(sym(a, (b : nat') => (add'(a', b) == add'(b, a'))));
    x : true;
    let r = nat_add_sym_symmetry_cong(x) :
        cong'(sym(a, (b : nat') => (add'(a', b) == add'(b, a'))));
    return r;
}

fn nat_add_symmetry : (a : nat') & (b : nat') -> add'(a, b) == add'(b, a) {
    use nat_def;

    x : (a : nat');
    y : (b : nat');

    fn f : true -> (b : nat') => add'(z', b) == add'(b, z') {
        x : true;
        lam r : (b : nat') => add'(z', b) == add'(b, z') {
            z : (b : nat');
            use nat_add_zero_symmetry;
            let z2 = nat_add_zero_symmetry(z) : add'(b, z') == add'(z', b);
            use eq_symmetry;
            let r = eq_symmetry(z2) : add'(z', b) == add'(b, z');
            return r;
        }
        return r;
    }
    let f5 = f() : sym(a, (b : nat') =>
        (add'(a', b) == add'(b, a')))(z')^true;
    fn g : (a : nat') ->
        ((b : nat') => (add'(a, b) == add'(b, a))) =>
        ((b : nat') => (add'(s'(a), b) == add'(b, s'(a))))
    {

        x : (a : nat');

        lam h :
            ((b : nat') => (add'(a, b) == add'(b, a))) =>
            ((b : nat') => (add'(s'(a), b) == add'(b, s'(a))))
        {

            y : (b : nat') => (add'(a, b) == add'(b, a));

            lam h2 : (b : nat') => (add'(s'(a), b) == add'(b, s'(a))) {

                z : (b : nat');

                let y2 = y(z) : add'(a, b) == add'(b, a);
                use nat_succ_eq;
                let y3 = nat_succ_eq(y2) : s'(add'(a, b)) == s'(add'(b, a));
                use nat_add_succ;
                let y4 = nat_add_succ(x, z) : add'(a, s'(b)) == s'(add'(a, b));
                let y5 = nat_add_succ(z, x) : add'(b, s'(a)) == s'(add'(b, a));
                use eq_transitivity;
                let y6 = eq_transitivity(y4, y3) :
                    add'(a, s'(b)) == s'(add'(b, a));
                use eq_transitivity_sym;
                let y7 = eq_transitivity_sym(y6, y5) :
                    add'(a, s'(b)) == add'(b, s'(a));
                use nat_add_succ_symmetry;
                let y8 = nat_add_succ_symmetry(x, z) : add'(s'(a), b) == add'(a, s'(b));
                let r = eq_transitivity(y8, y7) : add'(s'(a), b) == add'(b, s'(a));
                return r;
            }
            return h2;
        }
        return h;
    }
    let f6 = g() :
        sym(p, all((p'(a) => p'(s'(a)))^(a : nat')))(
            sym(a, (b : nat') => (add'(a', b) == add'(b, a')))
        );
    use nat_add_sym_symmetry_cong;
    let c = nat_add_sym_symmetry_cong() :
        cong'(sym(a, (b : nat') => (add'(a', b) == add'(b, a'))))^true;
    use nat_ind;
    let z5 = nat_ind(c, f5, f6) :
        sym(a, (b : nat') => (add'(a', b) == add'(b, a')))(a)^(a : nat');
    let z6 = z5(x) : (b : nat') => (add'(a, b) == add'(b, a));
    let r = z6(y) : add'(a, b) == add'(b, a);
    return r;
}