### Nuprl Lemma : l-ordered-remove-combine

`∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀cmp:T ⟶ ℤ. ∀L:T List.`
`  (l-ordered(T;x,y.R[x;y];L) `` l-ordered(T;x,y.R[x;y];remove-combine(cmp;L)))`

Proof

Definitions occuring in Statement :  l-ordered: `l-ordered(T;x,y.R[x; y];L)` remove-combine: `remove-combine(cmp;l)` list: `T List` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_apply: `x[s]` true: `True` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` top: `Top` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` cand: `A c∧ B` not: `¬A` subtype_rel: `A ⊆r B`
Lemmas referenced :  list_induction l-ordered_wf remove-combine_wf list_wf true_wf l-ordered-nil-true remove-combine-nil nil_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int lt_int_wf assert_of_lt_int l-ordered-cons less_than_wf remove-combine-implies-member l_member_wf all_wf remove-combine-cons cons_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality cumulativity applyEquality functionExtensionality hypothesis dependent_functionElimination independent_functionElimination natural_numberEquality addLevel impliesFunctionality because_Cache productElimination isect_memberEquality voidElimination voidEquality rename unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination dependent_pairFormation promote_hyp instantiate independent_pairFormation productEquality universeEquality intEquality

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}cmp:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:T  List.
(l-ordered(T;x,y.R[x;y];L)  {}\mRightarrow{}  l-ordered(T;x,y.R[x;y];remove-combine(cmp;L)))

Date html generated: 2018_05_21-PM-07_37_50
Last ObjectModification: 2017_07_26-PM-05_12_08

Theory : general

Home Index