### Nuprl Lemma : has-valueall-inl

`∀[a:Base]. uiff(has-valueall(inl a);has-valueall(a))`

Proof

Definitions occuring in Statement :  has-valueall: `has-valueall(a)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` inl: `inl x` base: `Base`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` has-valueall: `has-valueall(a)` top: `Top` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` has-value: `(a)↓` prop: `ℙ`
Lemmas referenced :  base_wf has-valueall_wf_base is-exception_wf has-value_wf_base evalall-inl
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis independent_pairFormation callbyvalueCallbyvalue callbyvalueReduce axiomSqleEquality baseApply closedConclusion baseClosed hypothesisEquality divergentSqle sqleReflexivity productElimination independent_pairEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[a:Base].  uiff(has-valueall(inl  a);has-valueall(a))

Date html generated: 2016_05_13-PM-03_25_30
Last ObjectModification: 2016_01_14-PM-06_44_48

Theory : call!by!value_1

Home Index