Nuprl Lemma : combine-combine-list-right

`∀[T:Type]`
`  ∀f:T ⟶ T ⟶ T. ∀L:T List.`
`    ((∀x,y,z:T.  (f[x;f[y;z]] = f[y;z] ∈ T `⇐⇒` (f[x;y] = y ∈ T) ∨ (f[x;z] = z ∈ T)))`
`    `` 0 < ||L||`
`    `` (∀a:T. (f[a;combine-list(x,y.f[x;y];L)] = combine-list(x,y.f[x;y];L) ∈ T `⇐⇒` (∃b∈L. f[a;b] = b ∈ T))))`

Proof

Definitions occuring in Statement :  combine-list: `combine-list(x,y.f[x; y];L)` l_exists: `(∃x∈L. P[x])` length: `||as||` list: `T List` less_than: `a < b` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` or: `P ∨ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` 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` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` false: `False` and: `P ∧ Q` cons: `[a / b]` top: `Top` combine-list: `combine-list(x,y.f[x; y];L)` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` guard: `{T}`
Lemmas referenced :  list-cases length_of_nil_lemma product_subtype_list length_of_cons_lemma reduce_hd_cons_lemma reduce_tl_cons_lemma list_induction all_wf iff_wf equal_wf list_accum_wf l_exists_wf cons_wf l_member_wf list_wf list_accum_nil_lemma l_exists_single nil_wf list_accum_cons_lemma or_wf l_exists_cons less_than_wf length_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesisEquality introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis dependent_functionElimination unionElimination sqequalRule imageElimination productElimination voidElimination promote_hyp hypothesis_subsumption isect_memberEquality voidEquality lambdaEquality cumulativity because_Cache applyEquality functionExtensionality setElimination rename setEquality independent_functionElimination independent_pairFormation independent_pairEquality axiomEquality addLevel allFunctionality impliesFunctionality orFunctionality levelHypothesis inlFormation inrFormation natural_numberEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type]
\mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T.  \mforall{}L:T  List.
((\mforall{}x,y,z:T.    (f[x;f[y;z]]  =  f[y;z]  \mLeftarrow{}{}\mRightarrow{}  (f[x;y]  =  y)  \mvee{}  (f[x;z]  =  z)))
{}\mRightarrow{}  0  <  ||L||
{}\mRightarrow{}  (\mforall{}a:T
(f[a;combine-list(x,y.f[x;y];L)]  =  combine-list(x,y.f[x;y];L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  f[a;b]  =  b))))

Date html generated: 2017_04_17-AM-07_39_22
Last ObjectModification: 2017_02_27-PM-04_13_20

Theory : list_1

Home Index