Nuprl - Pf decidable iff exists bool function 2 1 1 1 1 1 1 1

(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: decidable iff exists bool function 2 1 1 1 1 1 1 1

1. T: Type
2. Z: Type
3. P: TZProp
4. g: x:Ty:ZP(x,y)+(P(x,y) False)
5. x: T
6. y: Z
7. y1: y:ZP(x,y)+(P(x,y) False)
8. y1 = g(x)
9. y2: P(x,y)+(P(x,y) False)
10. y2 = g(x,y)

P(x,y) InjCase(y2 ; true; false)

By: Analyze -2 THEN Reduce 0

Generated subgoal:

1 9. y3: P(x,y) False
10. inr(y3) = g(x,y)
11. P(x,y)
False

About:

(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc