Nuprl - Proof: dec pred iff some boolfun

(9steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A property is effectively decidable just when it is characterized by a boolean-valued function.

At: dec pred iff some boolfun

T:Type, E:(T

Prop). (

x:T. Dec(E(x)))

(

f:(T

x:T. f(x)

E(x))

By:

GenUnivCD

Generated subgoals:

1 1. T : Type
2. E : TProp
3. x:T. Dec(E(x))
  f:(T). x:T. f(x)  E(x)
7 steps

2 1. T : Type
2. E : TProp
3. f:(T). x:T. f(x)  E(x)
4. x : T
  Dec(E(x))
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(9steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc

1	1. T : Type 2. E : TProp 3. x:T. Dec(E(x)) f:(T). x:T. f(x) E(x)	7 steps
2	1. T : Type 2. E : TProp 3. f:(T). x:T. f(x) E(x) 4. x : T Dec(E(x))	1 step