debug_log.txt

check: λa λb use a.P = λa ∀(b: Nat) (_2); use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~a a.P) a.succ) a.zero): ∀(b: Nat) (_4)} b)
    :: ∀(a: Nat) ∀(b: Nat) Bool
check: λa λb use a.P = λa ∀(b: Nat) (_2); use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~a a.P) a.succ) a.zero): ∀(b: Nat) (_4)} b)
    :: ∀(a: Nat) ∀(b: Nat) Bool
check: λb use a.P = λa ∀(b: Nat) (_2); use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~{a: Nat} a.P) a.succ) a.zero): ∀(b: Nat) (_4)} b)
    :: ∀(b: Nat) Bool
check: λb use a.P = λa ∀(b: Nat) (_2); use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~{a: Nat} a.P) a.succ) a.zero): ∀(b: Nat) (_4)} b)
    :: ∀(b: Nat) Bool
check: use a.P = λa ∀(b: Nat) (_2); use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~{a: Nat} a.P) a.succ) a.zero): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: use a.P = λa ∀(b: Nat) (_2); use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~{a: Nat} a.P) a.succ) a.zero): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~{a: Nat} λa ∀(b: Nat) (_2)) a.succ) a.zero): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: use a.succ = λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero); use a.zero = λb Bool/true; ({(((~{a: Nat} λa ∀(b: Nat) (_2)) a.succ) a.zero): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: use a.zero = λb Bool/true; ({(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) a.zero): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: use a.zero = λb Bool/true; ({(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) a.zero): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: ({(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
check: ({(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true): ∀(b: Nat) (_4)} {b: Nat})
    :: Bool
infer: ({(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true): ∀(b: Nat) (_4)} {b: Nat})
infer: {(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true): ∀(b: Nat) (_4)}
infer: {(((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true): ∀(b: Nat) (_4)}
check: (((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true)
    :: ∀(b: Nat) (_4)
check: (((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true)
    :: ∀(b: Nat) (_4)
infer: (((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)) λb Bool/true)
infer: ((~{a: Nat} λa ∀(b: Nat) (_2)) λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero))
infer: (~{a: Nat} λa ∀(b: Nat) (_2))
infer: ~{a: Nat}
infer: ~{a: Nat}
infer: {a: Nat}
infer: {a: Nat}
equal:
- ∀(b: Nat) (_4)
- (λa ∀(b: Nat) (_2) ~{a: Nat})
ident:
- ∀(b: Nat) (_4)
- ∀(b: Nat) (_2)
"unify: 4 x=(_4) t=(_2)"
oxi unsolved:True solvable:True no_loops:True
solve: 4 (_2)
YEP
check: λa ∀(b: Nat) (_2)
    :: ∀(x: Nat) *
check: λa ∀(b: Nat) (_2)
    :: ∀(x: Nat) *
check: ∀(b: Nat) (_2)
    :: *
check: ∀(b: Nat) (_2)
    :: *
infer: ∀(b: Nat) (_2)
equal:
- *
- *
ident:
- *
- *
YEP
check: Nat
    :: *
infer: Nat
infer: {Nat: *}
equal:
- *
- *
ident:
- *
- *
YEP
check: (_2)
    :: *
check: (_2)
    :: *
check: λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)
    :: ∀(pred: Nat) (λa ∀(b: Nat) (_2) (Nat/succ pred))
check: λa.pred λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)
    :: ∀(pred: Nat) (λa ∀(b: Nat) (_2) (Nat/succ pred))
check: λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)
    :: (λa ∀(b: Nat) (_2) (Nat/succ {a.pred: Nat}))
check: λb use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~b b.P) b.succ) b.zero)
    :: (λa ∀(b: Nat) (_2) (Nat/succ {a.pred: Nat}))
check: use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~{b: Nat} b.P) b.succ) b.zero)
    :: (_2)
check: use b.P = (_3); use b.succ = λx Bool/true; use b.zero = Bool/false; (((~{b: Nat} b.P) b.succ) b.zero)
    :: (_2)
check: use b.succ = λx Bool/true; use b.zero = Bool/false; (((~{b: Nat} (_3)) b.succ) b.zero)
    :: (_2)
check: use b.succ = λx Bool/true; use b.zero = Bool/false; (((~{b: Nat} (_3)) b.succ) b.zero)
    :: (_2)
check: use b.zero = Bool/false; (((~{b: Nat} (_3)) λx Bool/true) b.zero)
    :: (_2)
check: use b.zero = Bool/false; (((~{b: Nat} (_3)) λx Bool/true) b.zero)
    :: (_2)
check: (((~{b: Nat} (_3)) λx Bool/true) Bool/false)
    :: (_2)
check: (((~{b: Nat} (_3)) λx Bool/true) Bool/false)
    :: (_2)
infer: (((~{b: Nat} (_3)) λx Bool/true) Bool/false)
infer: ((~{b: Nat} (_3)) λx Bool/true)
infer: (~{b: Nat} (_3))
infer: ~{b: Nat}
infer: ~{b: Nat}
infer: {b: Nat}
infer: {b: Nat}
equal:
- (_2)
- ((_3) ~{b: Nat})
ident:
- (_2)
- (_3 ~{b: Nat})
"unify: 2 x=(_2) t=(_3 ~{b: Nat})"
oxi unsolved:True solvable:True no_loops:True
solve: 2 (_3 ~{b: Nat})

/\ PROBLEM

YEP
check: (_3)
    :: ∀(x: Nat) *
check: (_3)
    :: ∀(x: Nat) *
check: λx Bool/true
    :: ∀(pred: Nat) ((_3) (Nat/succ pred))
check: λx Bool/true
    :: ∀(pred: Nat) ((_3) (Nat/succ pred))
check: Bool/true
    :: ((_3) (Nat/succ {x: Nat}))
check: Bool/true
    :: ((_3) (Nat/succ {x: Nat}))
infer: Bool/true
infer: {~λP λt λf t: Bool}
equal:
- ((_3) (Nat/succ {x: Nat}))
- Bool
ident:
- (_3 (Nat/succ {x: Nat}))
- Bool
"unify: 3 x=(_3 (Nat/succ {x: Nat})) t=Bool"
MEH: (Nat/succ {x: Nat})
oxi unsolved:True solvable:False no_loops:True
NOP
"unify: 3 x=(_3 (Nat/succ {x: Nat})) t=Bool"
MEH: (Nat/succ {x: Nat})
oxi unsolved:True solvable:False no_loops:True