use cong;

sym Lob;
sym N;
sym N2;
sym K;
sym T;
sym nec;
sym NecToPos;
sym pos;
sym PosToNec;

fn nec_def : true -> nec'(a) == □a {
    axiom nec_def : true -> nec'(a) == □a;
    x : true;
    let r = nec_def(x) : nec'(a) == □a;
    return r;
}

fn pos_def : true -> pos'(a) == ◇a {
    axiom pos_def : true -> pos'(a) == ◇a;
    x : true;
    let r = pos_def(x) : pos'(a) == ◇a;
    return r;
}

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

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

/// `□(□p => p)`.
fn lob_triv : (p^true => p)^true {
    lam f : p^true => p {
        x : p^true;
        let y = () : true;
        let z = x(y) : p;
        return z;
    }
    return f;
}

/// `(□(□false => false) => □false)  ->  false`.
fn para_lob : (false^true => false)^true => false^true  ->  false {
    x : (false^true => false)^true => false^true;
    use lob_triv;
    let y = lob_triv() : (false^true => false)^true;
    let x2 = x(y) : false^true;
    let x3 = () : true;
    let x4 = x2(x3) : false;
    return x4;
}

/// Demonstrates that Löb's axiom is absurd in HOOO EP.
fn lob_absurd : all((p^true => p)^true => p^true)  ->  false {
    arg : all((p^true => p)^true => p^true);
    let x = arg() : (false^true => false)^true => false^true;
    use para_lob;
    let r = para_lob(x) : false;
    return r;
}

/*
Löb axiom: `□(□p => p) => □p`
Formal expression: `Lob'`
*/

/// Reduction of Löb relation.
fn modal_lob_to : Lob'  ->  all(□(□a => a) => □a) {
    axiom modal_lob_to : Lob' -> all(□(□a => a) => □a);
    x : Lob';
    let r = modal_lob_to(x) : all(□(□a => a) => □a);
    unsafe return r;
}

/// Construction of Löb relation.
fn modal_lob_from : all(□(□a => a) => □a)  ->  Lob' {
    axiom modal_lob_from : all(□(□a => a) => □a)  ->  Lob';
    x : all(□(□a => a) => □a);
    let r = modal_lob_from(x) : Lob';
    return r;
}

/*
N axiom: `□a => a^true`
Formal expression `N'`
*/

/// Reduction of N relation.
fn modal_n_to : N'  ->  all(a^true => □a) {
    axiom modal_n_to : N' -> all(a^true => □a);
    x : N';
    let r = modal_n_to(x) : all(a^true => □a);
    unsafe return r;
}

/// Construciton of N relation.
fn modal_n_from : all(a^true => □a)  ->  N' {
    axiom modal_n_from : all(a^true => □a) -> N';
    x : all(a^true => □a);
    let r = modal_n_from(x) : N';
    return r;
}

/*
N2 axiom `□a == a^true
Formal expression `N2'`
*/

/// Reduction of N2 relation.
fn modal_n2_to : N2'  ->  all(□a == a^true) {
    axiom modal_n2_to : N2' -> all(□a == a^true);
    x : N2';
    let r = modal_n2_to(x) : all(□a == a^true);
    unsafe return r;
}

/// Construction of N2 relation.
fn modal_n2_from : all(□a == a^true)  ->  N2' {
    axiom modal_n2_from : all(□a == a^true) -> N2';
    x : all(□a == a^true);
    let r = modal_n2_from(x) : N2';
    return r;
}

/*
K axiom: `□(a => b) => (□a => □b)`
Formal expression: `K'`
*/

/// Reduction of K relation.
fn modal_k_to : K'  ->  all(□(a => b) => (□a => □b)) {
    axiom modal_k_to : K' -> all(□(a => b) => (□a => □b));
    x : K';
    let r = modal_k_to(x) : all(□(a => b) => (□a => □b));
    unsafe return r;
}

/// Construction of K relation.
fn modal_k_from : all(□(a => b) => (□a => □b))  ->  K' {
    axiom modal_k_from : all(□(a => b) => (□a => □b)) -> K';
    x : all(□(a => b) => (□a => □b));
    let r = modal_k_from(x) : K';
    return r;
}

/*
T axiom: `□a => a`
Formal expression: `T'`
*/

/// Reduction of T relation.
fn modal_t_to : T'  ->  all(□a => a) {
    axiom modal_t_to : T' -> all(□a => a);
    x : T';
    let r = modal_t_to(x) : all(□a => a);
    unsafe return r;
}

/// Construction of T relation.
fn modal_t_from : all(□a => a)  ->  T {
    axiom modal_t_from : all(□a => a) -> T;
    x : all(□a => a);
    let r = modal_t_from(x) : T;
    return r;
}

/// Axiom N2 implies axiom N.
fn modal_n2_to_n : N2'  ->  N' {
    x : N2';
    use modal_n2_to;
    let x3 = modal_n2_to(x) : all(□a == a^true);
    use snd;
    let x4 = snd(x3) : all(a^true => □a);
    use modal_n_from;
    let r = modal_n_from(x4) : N';
    return r;
}

/// Axiom N2 implies axiom K.
fn modal_n2_to_k : N2'  ->  K' {
    x : N2';
    use modal_n2_to;
    let eq_nec_a_tauto_a = modal_n2_to(x) : all(□a == a^true);
    let eq_nec_b_tauto_b = modal_n2_to(x) : all(□b == b^true);
    let eq_nec_ab_tauto_ab = modal_n2_to(x) : all(□(a => b) == (a => b)^true);
    use fst;
    let nec_a_to_tauto_a = fst(eq_nec_a_tauto_a) : all(□a => a^true);
    let nec_ab_to_tauto_ab = fst(eq_nec_ab_tauto_ab) : all(□(a => b) => (a => b)^true);
    use snd;
    let tauto_b_to_nec_b = snd(eq_nec_b_tauto_b) : all(b^true => □b);
    use hooo_imply;
    let f = hooo_imply() : all((a => b)^true => (a^true => b^true));
    use imply_transitivity;
    let f2 = imply_transitivity(nec_ab_to_tauto_ab, f) : all(□(a => b) => (a^true => b^true));
    lam g : all(a^true => b^true) => all(□a => □b) {
        x : all(a^true => b^true);
        use imply_transitivity;
        let x2 = imply_transitivity(nec_a_to_tauto_a, x) : all(□a => b^true);
        let r = imply_transitivity(x2, tauto_b_to_nec_b) : all(□a => □b);
        unsafe return r;
    }
    let f3 = imply_transitivity(f2, g) : all(□(a => b) => (□a => □b));
    use modal_k_from;
    let r = modal_k_from(f3) : K';
    return r;
}

/// Axiom N2 implies axiom T.
fn modal_n2_to_t_2 : N2'  ->  T' {
    x : N2';
    use modal_n2_to;
    use triv;
    let f = triv() : all(a^true => a);
    let eq_nec_a_tauto_a = modal_n2_to(x) : all(□a == a^true);
    use fst;
    let x3 = fst(eq_nec_a_tauto_a) : all(□a => a^true);
    use imply_transitivity;
    let x4 = imply_transitivity(x3, f) : all(□a => a);
    use modal_t_from;
    let r = modal_t_from(x4) : T';
    return r;
}

/*
NecToPos axiom: `□a == !◇!a`
Formal expression: `NecToPos'`
*/

/// Reduction of NecToPos relation.
fn modal_nec_to_pos_to : NecToPos'  ->  all(□a == !◇!a) {
    axiom modal_nec_to_pos_to : NecToPos' -> all(□a == !◇!a);
    x : NecToPos';
    let r = modal_nec_to_pos_to(x) : all(□a == !◇!a);
    unsafe return r;
}

/// Construction of NecToPos relation.
fn modal_nec_to_pos_from : all(□a == !◇!a)  ->  NecToPos' {
    axiom modal_nec_to_pos_from : all(□a == !◇!a) -> NecToPos';
    x : all(□a == !◇!a);
    let r = modal_nec_to_pos_from(x) : NecToPos';
    return r;
}

/*
PosToNec axiom: `◇a == !□!a`
Formal expression: `PosToNec'`
*/

/// Reduction of PosToNec relation.
fn modal_pos_to_nec_to : PosToNec'  ->  all(◇a == !□!a) {
    axiom modal_pos_to_nec_to : PosToNec' -> all(◇a == !□!a);
    x : PosToNec';
    let r = modal_pos_to_nec_to(x) : all(◇a == !□!a);
    unsafe return r;
}

/// Construction of PosToNec relation.
fn modal_pos_to_nec_from : all(◇a == !□!a)  ->  PosToNec' {
    axiom modal_pos_to_nec_from : all(◇a == !□!a) -> PosToNec';
    x : all(◇a == !□!a);
    let r = modal_pos_to_nec_from(x) : PosToNec';
    return r;
}

/// `□a & (a == b)  ->  □a`.
fn modal_nec_in_arg : □a & (a == b)  ->  □b {
    use cong_to;
    use eq_transitivity;
    use eq_transitivity_rev_sym;
    use fst;
    use nec_cong;
    use nec_def;
    use triv;

    x : □a;
    y : a == b;

    let x2 = triv(nec_cong) : cong'(nec');
    let x3 = cong_to(x2) : sym(f, all(a == b -> f'(a) == f'(b)))(nec');
    let x4 = x3() : a == b -> nec'(a) == nec'(b);
    let x5 = x4(y) : nec'(a) == nec'(b);
    let x6 = triv(nec_def) : nec'(a) == □a;
    let x7 = triv(nec_def) : nec'(b) == □b;
    let x8 = eq_transitivity_rev_sym(x6, x5) : □a == nec'(b);
    let x9 = eq_transitivity(x8, x7) : □a == □b;
    let x10 = fst(x9) : □a => □b;
    let r = x10(x) : □b;
    return r;
}

/// `◇a & (a == b)  ->  ◇b`.
fn modal_pos_in_arg : ◇a & (a == b)  ->  ◇b {
    use cong_to;
    use eq_transitivity;
    use eq_transitivity_rev_sym;
    use fst;
    use pos_cong;
    use pos_def;
    use triv;

    x : ◇a;
    y : a == b;

    let x2 = triv(pos_cong) : cong'(pos');
    let x3 = cong_to(x2) : sym(f, all(a == b -> f'(a) == f'(b)))(pos');
    let x4 = x3() : a == b -> pos'(a) == pos'(b);
    let x5 = x4(y) : pos'(a) == pos'(b);
    let x6 = triv(pos_def) : pos'(a) == ◇a;
    let x7 = triv(pos_def) : pos'(b) == ◇b;
    let x8 = eq_transitivity_rev_sym(x6, x5) : ◇a == pos'(b);
    let x9 = eq_transitivity(x8, x7) : ◇a == ◇b;
    let x10 = fst(x9) : ◇a => ◇b;
    let r = x10(x) : ◇b;
    return r;
}

fn modal_nec_eq : (a == b)  ->  □a == □b {
    x : a == b;
    lam f : □a => □b {
        y : □a;
        use modal_nec_in_arg;
        let r = modal_nec_in_arg(y, x) : □b;
        return r;
    }
    lam g : □b => □a {
        y : □b;
        use eq_symmetry;
        let x2 = eq_symmetry(x) : b == a;
        use modal_nec_in_arg;
        let r = modal_nec_in_arg(y, x2) : □a;
        return r;
    }
    use refl;
    let r = refl(f, g) : □a == □b;
    return r;
}

fn modal_pos_eq : (a == b)  ->  ◇a == ◇b {
    x : a == b;
    lam f : ◇a => ◇b {
        y : ◇a;
        use modal_pos_in_arg;
        let r = modal_pos_in_arg(y, x) : ◇b;
        return r;
    }
    lam g : ◇b => ◇a {
        y : ◇b;
        use eq_symmetry;
        let x2 = eq_symmetry(x) : b == a;
        use modal_pos_in_arg;
        let r = modal_pos_in_arg(y, x2) : ◇a;
        return r;
    }
    use refl;
    let r = refl(f, g) : ◇a == ◇b;
    return r;
}

fn modal_tauto_excm_to_imply_nec_to_pos_pos_to_nec :
    all(excm(a)^true)  ->  NecToPos' => PosToNec'
{
    x : all(excm(a)^true);
    lam f : NecToPos' => PosToNec' {
        use eq_modus_tollens;
        use eq_symmetry;
        use eq_transitivity;
        use modal_nec_to_pos_to;
        use modal_pos_eq;
        use modal_pos_to_nec_from;
        use not_excm_to_eq_nn;
        use triv;
        
        let x2 = x() : all(excm(◇!!a)^true);
        let x3 = triv(x2) : all(excm(◇!!a));
        let x4 = not_excm_to_eq_nn(x3) : all(◇!!a == !!◇!!a);
        let x5 = eq_symmetry(x4) : all(!!◇!!a == ◇!!a);
        
        let x7 = triv(x) : all(excm(a));
        let x8 = not_excm_to_eq_nn(x7) : all(a == !!a);
        
        y : NecToPos';
        let y2 = modal_nec_to_pos_to(y) : all(□!a == !◇!!a);
        let y3 = eq_modus_tollens(y2) : all(!□!a == !!◇!!a);
        let y4 = eq_transitivity(y3, x5) : all(!□!a == ◇!!a);
        let y6 = eq_symmetry(y4) : all(◇!!a == !□!a);
        let y7 = modal_pos_eq(x8) : all(◇a == ◇!!a);
        let y8 = eq_transitivity(y7, y6) : all(◇a == !□!a);
        let r = modal_pos_to_nec_from(y8) : PosToNec';
        return r;
    }
    return f;
}

fn modal_tauto_excm_to_imply_pos_to_nec_nec_to_pos :
    all(excm(a)^true)  ->  PosToNec' => NecToPos'
{
    x : all(excm(a)^true);
    lam f : PosToNec' => NecToPos' {
        use eq_modus_tollens;
        use eq_symmetry;
        use eq_transitivity;
        use modal_nec_eq;
        use modal_nec_to_pos_from;
        use modal_pos_to_nec_to;
        use not_excm_to_eq_nn;
        use triv;

        let x3 = triv(x) : all(excm(□!!a));
        let x4 = not_excm_to_eq_nn(x3) : all(□!!a == !!□!!a);
        let x5 = eq_symmetry(x4) : all(!!□!!a == □!!a);

        let x7 = triv(x) : all(excm(a));
        let x8 = not_excm_to_eq_nn(x7) : all(a == !!a);

        y : PosToNec';
        let y3 = modal_pos_to_nec_to(y) : all(◇!a == !□!!a);
        let y4 = eq_modus_tollens(y3) : all(!◇!a == !!□!!a);
        let y5 = eq_transitivity(y4, x5) : all(!◇!a == □!!a);
        let y6 = eq_symmetry(y5) : all(□!!a == !◇!a);
        let y7 = modal_nec_eq(x8) : all(□a == □!!a);
        let y8 = eq_transitivity(y7, y6) : all(□a == !◇!a);
        let r = modal_nec_to_pos_from(y8) : NecToPos';
        return r;
    }
    return f;
}

/// There is no consistent modal logic of the Löb axiom in HOOO EP (N2).
fn modal_n2_to_nlob : N2'  ->  !Lob' {
    x : N2';
    lam f : !Lob' {
        use eq_transitivity;
        use imply_eq_left;
        use imply_in_left_arg;
        use imply_in_right_arg;
        use modal_lob_to;
        use modal_n2_to;
        use modal_nec_eq;
        use para_lob;

        y : Lob';
        let y3 = modal_lob_to(y) : □(□false => false) => □false;
        
        let x3 = modal_n2_to(x) : □false == false^true;

        let x4 = imply_eq_left(x3) : (□false => false) == (false^true => false);
        let x5 = modal_nec_eq(x4) : □(□false => false) == □(false^true => false);

        let x7 = modal_n2_to(x) : □(false^true => false) == (false^true => false)^true;

        let x8 = eq_transitivity(x5, x7) : □(□false => false) == (false^true => false)^true;
        let x9 = imply_in_left_arg(y3, x8) : (false^true => false)^true => □false;
        let x10 = imply_in_right_arg(x9, x3) : (false^true => false)^true => false^true;
        let r = para_lob(x10) : false;
        return r;
    }
    return f;
}

fn modal_tauto_n2_to_para_nec_false : N2'^true  ->  false^(□false) {
    x : N2'^true;
   
    fn h : all(N2'(a))  ->  N2'(false) {
        k : all(N2'(a));
        let r = k() : N2'(false);
        return r;
    }
 
    use pow_transitivity;
    use modal_n2_to;
    let f2 = modal_n2_to() : N2' -> □false == false^true;
    let x3 = pow_transitivity(x, f2) : (□false == false^true)^true;
    use fst;
    let f3 = fst() : (□false == false^true) -> (□false => false^true);
    let x4 = pow_transitivity(x3, f3) : (□false => false^true)^true;
    
    fn f : □false => false^true  ->  □false => false {
        x : □false => false^true;
        lam g : □false => false {
            y : □false;
            let y2 = x(y) : false^true;
            use triv;
            let r = triv(y2) : false;
            return r;
        }
        return g;
    }

    let x5 = pow_transitivity(x4, f) : (!□false)^true;
    use tauto_not_to_para;
    let r = tauto_not_to_para(x5) : false^(□false);
    return r;
}

fn modal_tauto_t_to_para_nec_false : T'^true  ->  false^(□false) {
    x : T'^true;

    use pow_transitivity;
    use modal_t_to;
    let f = modal_t_to() : T' -> !□false;
    let x3 = pow_transitivity(x, f) : (!□false)^true;

    use tauto_not_to_para;
    let r = tauto_not_to_para(x3) : false^(□false);
    return r;
}

fn modal_n_to_nlob : N' & false^(□false)  ->  !Lob' {
    x : N';
    y0 : false^(□false);

    use para_to_tauto_not;
    let y = para_to_tauto_not(y0) : (□false => false)^true;

    use modal_n_to;
    let x3 = modal_n_to(x) : (□false => false)^true => □(□false => false);
    let y2 = x3(y) : □(□false => false);

    use triv;
    let w = triv(y) : □false => false;

    lam f : !Lob' {
        z : Lob';
        use modal_lob_to;
        let z3 = modal_lob_to(z) : □(□false => false) => □false;
        let z4 = z3(y2) : □false;
        let r = w(z4) : false;
        return r;
    }

    return f;
}