### Nuprl Lemma : isaxiom-append-nil

`∀[l:Base]. (↑isaxiom(l)) supposing ((↑isaxiom(l @ [])) and (l @ [])↓)`

Proof

Definitions occuring in Statement :  append: `as @ bs` nil: `[]` has-value: `(a)↓` assert: `↑b` bfalse: `ff` btrue: `tt` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` isaxiom: `if z = Ax then a otherwise b` base: `Base`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` append: `as @ bs` list_ind: list_ind member: `t ∈ T` has-value: `(a)↓` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` cons: `[a / b]` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` false: `False` top: `Top` nil: `[]` it: `⋅` btrue: `tt` true: `True` not: `¬A` prop: `ℙ`
Lemmas referenced :  has-value-implies-dec-ispair-2 top_wf has-value-implies-dec-isaxiom-2 bottom_diverge assert_wf has-value_wf_base is-exception_wf btrue_wf bfalse_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  sqequalHypSubstitution sqequalRule introduction cut callbyvalueCallbyvalue hypothesis callbyvalueReduce extract_by_obid dependent_functionElimination thin hypothesisEquality independent_functionElimination unionElimination voidElimination lambdaFormation isect_memberEquality voidEquality axiomEquality natural_numberEquality Error :universeIsType,  isectElimination isaxiomCases divergentSqle baseClosed baseApply closedConclusion axiomSqEquality Error :inhabitedIsType

Latex:
\mforall{}[l:Base].  (\muparrow{}isaxiom(l))  supposing  ((\muparrow{}isaxiom(l  @  []))  and  (l  @  [])\mdownarrow{})

Date html generated: 2019_06_20-PM-00_39_30
Last ObjectModification: 2018_09_26-PM-02_10_34

Theory : list_0

Home Index