Nuprl Lemma : isaxiom-append-nil

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


Definitions occuring in Statement :  append: as bs nil: [] has-value: (a)↓ assert: b bfalse: ff btrue: tt uimplies: supposing a uall: [x:A]. B[x] isaxiom: if Ax then otherwise b base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a append: as bs list_ind: list_ind member: t ∈ T has-value: (a)↓ all: x:A. B[x] implies:  Q or: P ∨ Q cons: [a b] assert: b ifthenelse: if then else 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

\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