### Nuprl Lemma : assert_dec2bool

`∀[d:Decision]. uiff(↑dec2bool(d);↑d)`

Proof

Definitions occuring in Statement :  dec2bool: `dec2bool(d)` decision: `Decision` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` assert: `↑b` dec2bool: `dec2bool(d)` ifthenelse: `if b then t else f fi ` bfalse: `ff` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` decision: `Decision` true: `True` false: `False` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  decision_wf true_wf false_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation introduction cut sqequalHypSubstitution unionElimination thin sqequalRule natural_numberEquality voidElimination hypothesisEquality extract_by_obid hypothesis lambdaFormation axiomEquality equalityTransitivity equalitySymmetry isectElimination dependent_functionElimination independent_functionElimination instantiate because_Cache

Latex:
\mforall{}[d:Decision].  uiff(\muparrow{}dec2bool(d);\muparrow{}d)

Date html generated: 2017_10_01-AM-08_28_34
Last ObjectModification: 2017_07_26-PM-04_23_34

Theory : basic

Home Index