Nuprl Lemma : cons_iseg_not_null

`∀[T:Type]. ∀u:T. ∀L,v:T List.  (L ≤ [u / v] `` (¬↑null(L)) `` (∃K:T List. ((L = [u / K] ∈ (T List)) ∧ K ≤ v)))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` null: `null(as)` cons: `[a / b]` list: `T List` assert: `↑b` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` or: `P ∨ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` not: `¬A` true: `True` false: `False` cons: `[a / b]` top: `Top` bfalse: `ff` iff: `P `⇐⇒` Q` and: `P ∧ Q` exists: `∃x:A. B[x]` cand: `A c∧ B` prop: `ℙ`
Lemmas referenced :  list-cases null_nil_lemma product_subtype_list null_cons_lemma cons_iseg and_wf equal_wf cons_wf list_wf iseg_wf not_wf assert_wf null_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesisEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis dependent_functionElimination unionElimination sqequalRule independent_functionElimination natural_numberEquality voidElimination promote_hyp hypothesis_subsumption productElimination isect_memberEquality voidEquality because_Cache dependent_pairFormation dependent_set_memberEquality independent_pairFormation applyEquality lambdaEquality setElimination rename setEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}u:T.  \mforall{}L,v:T  List.    (L  \mleq{}  [u  /  v]  {}\mRightarrow{}  (\mneg{}\muparrow{}null(L))  {}\mRightarrow{}  (\mexists{}K:T  List.  ((L  =  [u  /  K])  \mwedge{}  K  \mleq{}  v)))

Date html generated: 2016_05_14-PM-01_30_55
Last ObjectModification: 2015_12_26-PM-05_23_50

Theory : list_1

Home Index