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 


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: 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: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  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: ⇐⇒ Q so_lambda: λ2y.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 ⊆B bool: 𝔹 unit: Unit btrue: tt uiff: uiff(P;Q) ifthenelse: if then else 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:  Q cand: 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

\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 

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

Theory : general

Home Index