Nuprl Lemma : has-value-band-type

[a,b:Base].  a ∈ Top Top supposing (a ∧b b)↓


Proof




Definitions occuring in Statement :  band: p ∧b q has-value: (a)↓ uimplies: supposing a uall: [x:A]. B[x] top: Top member: t ∈ T union: left right base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a band: p ∧b q ifthenelse: if then else fi  has-value: (a)↓ prop:
Lemmas referenced :  base_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution callbyvalueDecide hypothesis equalityTransitivity equalitySymmetry sqequalRule axiomEquality lemma_by_obid isectElimination thin baseApply closedConclusion baseClosed hypothesisEquality isect_memberEquality because_Cache

Latex:
\mforall{}[a,b:Base].    a  \mmember{}  Top  +  Top  supposing  (a  \mwedge{}\msubb{}  b)\mdownarrow{}



Date html generated: 2016_05_13-PM-03_59_50
Last ObjectModification: 2016_01_14-PM-07_21_05

Theory : bool_1


Home Index