### Nuprl Lemma : l-ordered-decomp2

`∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].`
`  (∀[L:T List]`
`     (L = (filter(λy.R[y;x];L) @ [x / filter(λy.R[x;y];L)]) ∈ (T List)) supposing `
`        (l-ordered(T;x,y.↑R[x;y];L) and `
`        (x ∈ L))) supposing `
`     (Trans(T;x,y.↑R[x;y]) and `
`     Irrefl(T;x,y.↑R[x;y]) and `
`     StAntiSym(T;x,y.↑R[x;y]))`

Proof

Definitions occuring in Statement :  l-ordered: `l-ordered(T;x,y.R[x; y];L)` l_member: `(x ∈ l)` filter: `filter(P;l)` append: `as @ bs` cons: `[a / b]` list: `T List` irrefl: `Irrefl(T;x,y.E[x; y])` st_anti_sym: `StAntiSym(T;x,y.R[x; y])` trans: `Trans(T;x,y.E[x; y])` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` or: `P ∨ Q` append: `as @ bs` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` iff: `P `⇐⇒` Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` true: `True` cons: `[a / b]` le: `A ≤ B` less_than': `less_than'(a;b)` colength: `colength(L)` nil: `[]` it: `⋅` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` less_than: `a < b` squash: `↓T` decidable: `Dec(P)` subtype_rel: `A ⊆r B` bool: `𝔹` unit: `Unit` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` irrefl: `Irrefl(T;x,y.E[x; y])` st_anti_sym: `StAntiSym(T;x,y.R[x; y])` bfalse: `ff` bnot: `¬bb` assert: `↑b` rev_implies: `P `` Q` cand: `A c∧ B` rev_uimplies: `rev_uimplies(P;Q)` trans: `Trans(T;x,y.E[x; y])`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than list-cases filter_nil_lemma list_ind_nil_lemma istype-void nil_member l-ordered-nil-true assert_wf l-ordered_wf nil_wf l_member_wf product_subtype_list colength-cons-not-zero colength_wf_list istype-le subtract-1-ge-0 subtype_base_sq intformeq_wf int_formula_prop_eq_lemma set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int subtract_wf intformnot_wf itermSubtract_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_subtract_lemma int_term_value_add_lemma decidable__le le_wf filter_cons_lemma eqtt_to_assert list_ind_cons_lemma eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot assert_elim not_assert_elim btrue_neq_bfalse cons_member l-ordered-cons cons_wf istype-nat list_wf trans_wf irrefl_wf st_anti_sym_wf istype-universe iff_imp_equal_bool btrue_wf istype-true equal_wf iff_weakening_equal squash_wf true_wf filter_is_nil l_all_iff not_wf istype-assert filter_trivial assert_functionality_wrt_uiff subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin lambdaFormation_alt extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination Error :memTop,  sqequalRule independent_pairFormation universeIsType voidElimination isect_memberEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType functionIsTypeImplies unionElimination productElimination because_Cache applyEquality promote_hyp hypothesis_subsumption equalityIstype dependent_set_memberEquality_alt instantiate equalityTransitivity equalitySymmetry applyLambdaEquality imageElimination baseApply closedConclusion baseClosed intEquality sqequalBase equalityElimination cumulativity functionIsType universeEquality imageMemberEquality hyp_replacement productIsType setIsType functionEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].
(\mforall{}[L:T  List]
(L  =  (filter(\mlambda{}y.R[y;x];L)  @  [x  /  filter(\mlambda{}y.R[x;y];L)]))  supposing
(l-ordered(T;x,y.\muparrow{}R[x;y];L)  and
(x  \mmember{}  L)))  supposing
(Trans(T;x,y.\muparrow{}R[x;y])  and
Irrefl(T;x,y.\muparrow{}R[x;y])  and
StAntiSym(T;x,y.\muparrow{}R[x;y]))

Date html generated: 2020_05_20-AM-08_09_24
Last ObjectModification: 2020_01_25-PM-11_57_54

Theory : general

Home Index