bug.jonprl.output

-*- mode: compilation; default-directory: "~/build/JonPRL/" -*-
Compilation started at Thu Oct  6 17:42:16

/Users/jrw12/build/JonPRL/bin/jonprl --check bug.jonprl
In assert, goal is:
⊢ =(nat; nat; U{i})
z = h@101
term = void
term' = void
In assert, goal is:

1. h@101 : approx(<>; bot)
⊢ =(nat; nat; U{i})
z = q@102
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@112 : nat
⊢ =(=(zero; succ(n@112); nat); =(zero; succ(n@112); nat); U{i})
z = h@105
term = void
term' = void
In assert, goal is:

1. n@112 : nat
2. h@105 : approx(<>; bot)
⊢ =(=(zero; succ(n@112); nat); =(zero; succ(n@112); nat); U{i})
z = q@106
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@112 : nat
⊢ =(nat; nat; U{i})
z = h@105
term = void
term' = void
In assert, goal is:

1. n@112 : nat
2. h@105 : approx(<>; bot)
⊢ =(nat; nat; U{i})
z = q@106
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@112 : nat
⊢ =(zero; zero; nat)
z = h@105
term = void
term' = void
In assert, goal is:

1. n@112 : nat
2. h@105 : approx(<>; bot)
⊢ =(zero; zero; nat)
z = q@106
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@112 : nat
⊢ =(succ(n@112); succ(n@112); nat)
z = h@105
term = void
term' = void
In assert, goal is:

1. n@112 : nat
2. h@105 : approx(<>; bot)
⊢ =(succ(n@112); succ(n@112); nat)
z = q@106
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@112 : nat
⊢ =(n@112; n@112; nat)
z = h@105
term = void
term' = void
In assert, goal is:

1. n@112 : nat
2. h@105 : approx(<>; bot)
⊢ =(n@112; n@112; nat)
z = q@106
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
⊢ approx(<>; bot)
z = h@296
term = void
term' = void
In assert, goal is:

1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
3. h@296 : approx(<>; bot)
⊢ approx(<>; bot)
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
⊢ =(=(succ(n@299); zero; nat); =(succ(n@299); zero; nat); U{i})
z = h@296
term = void
term' = void
In assert, goal is:

1. n@299 : nat
2. h@296 : approx(<>; bot)
⊢ =(=(succ(n@299); zero; nat); =(succ(n@299); zero; nat); U{i})
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
⊢ =(nat; nat; U{i})
z = h@296
term = void
term' = void
In assert, goal is:

1. n@299 : nat
2. h@296 : approx(<>; bot)
⊢ =(nat; nat; U{i})
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
⊢ =(succ(n@299); succ(n@299); nat)
z = h@296
term = void
term' = void
In assert, goal is:

1. n@299 : nat
2. h@296 : approx(<>; bot)
⊢ =(succ(n@299); succ(n@299); nat)
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
⊢ =(n@299; n@299; nat)
z = h@296
term = void
term' = void
In assert, goal is:

1. n@299 : nat
2. h@296 : approx(<>; bot)
⊢ =(n@299; n@299; nat)
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
⊢ =(zero; zero; nat)
z = h@296
term = void
term' = void
In assert, goal is:

1. n@299 : nat
2. h@296 : approx(<>; bot)
⊢ =(zero; zero; nat)
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:
⊢ =(nat; nat; U{i})
z = h@296
term = void
term' = void
In assert, goal is:

1. h@296 : approx(<>; bot)
⊢ =(nat; nat; U{i})
z = q@297
term = has-value(bot)
term' = has-value(bot)
In assert, goal is:

1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
⊢ approx(<>; bot)
z = H@507
term = is-zero(succ(n@72))
term' = is-zero(succ(n@299))
In subst, goal is:

1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
⊢ natrec(succ(n@299); unit; _._.void)
eq = =(succ(n@77); zero; nat)
eq' = =(succ(n@299); zero; nat)
xC = h@520.natrec(h@520; _@90; _._._@97)
xC' = h@530.natrec(h@530; _@90; _._._@97)


[bug.jonprl:12.3-20.1]: tactic 'COMPLETE' failed with goal: 
[main] ⊢ (n@576:nat) =(succ(n@576); zero; nat) -> void

Remaining subgoals:

[aux] 
1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
⊢ =(succ(n@77); zero; nat)

[main] 
1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
⊢ natrec(zero; unit; _._.void)

[aux] 
1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
3. h@570 : nat
⊢ member(natrec(h@570; unit; _._.void); U{i})

[main] 
1. n@299 : nat
2. x@302 : =(succ(n@299); zero; nat)
3. H@507 : is-zero(succ(n@299))
⊢ approx(<>; bot)

RefinementFailed
Compilation exited abnormally with code 1 at Thu Oct  6 17:42:16