Nuprl Lemma : null-strict

[a:Base]. (a)↓ supposing (null(a))↓


Proof




Definitions occuring in Statement :  null: null(as) has-value: (a)↓ uimplies: supposing a uall: [x:A]. B[x] base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a null: null(as) 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 callbyvalueIspair hypothesis sqequalRule axiomSqleEquality lemma_by_obid isectElimination thin baseApply closedConclusion baseClosed hypothesisEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[a:Base].  (a)\mdownarrow{}  supposing  (null(a))\mdownarrow{}



Date html generated: 2016_05_15-PM-02_07_18
Last ObjectModification: 2016_01_15-PM-10_24_01

Theory : untyped!computation


Home Index