### Nuprl Lemma : causal_order_filter_iseg

`∀[T,T':Type].`
`  ∀L:T List. ∀P,Q:ℕ||L|| ⟶ 𝔹. ∀f,g:T ⟶ T'.`
`    ((∀L':T List. (L' ≤ L `` map(f;filter2(P;L')) ≤ map(g;filter2(Q;L'))))`
`    `` causal_order(L;λi,j. ((g L[i]) = (f L[j]) ∈ T');λi.(↑Q[i]);λi.(↑P[i])))`

Proof

Definitions occuring in Statement :  causal_order: `causal_order(L;R;P;Q)` filter2: `filter2(P;L)` iseg: `l1 ≤ l2` select: `L[n]` length: `||as||` map: `map(f;as)` list: `T List` int_seg: `{i..j-}` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` lambda: `λx.A[x]` 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` prop: `ℙ` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` so_apply: `x[s]` causal_order: `causal_order(L;R;P;Q)` nat: `ℕ` guard: `{T}` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` int_iseg: `{i...j}` cand: `A c∧ B` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  all_wf list_wf iseg_wf map_wf filter2_wf iseg_length decidable__lt length_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf lelt_wf int_seg_wf bool_wf assert_wf firstn_wf firstn-iseg int_seg_properties decidable__le itermConstant_wf itermAdd_wf int_term_value_constant_lemma int_term_value_add_lemma le_wf iseg_member subtype_rel_dep_function int_seg_subtype false_wf squash_wf true_wf length_firstn_eq iff_weakening_equal subtype_rel_self select_wf member_filter2 less_than_wf select_firstn equal_wf length_firstn member_map l_member_wf intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis sqequalRule lambdaEquality functionEquality because_Cache functionExtensionality applyEquality independent_isectElimination setElimination rename dependent_set_memberEquality productElimination independent_pairFormation dependent_functionElimination unionElimination imageElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll universeEquality addEquality independent_functionElimination equalityTransitivity equalitySymmetry productEquality imageMemberEquality baseClosed hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T,T':Type].
\mforall{}L:T  List.  \mforall{}P,Q:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f,g:T  {}\mrightarrow{}  T'.
((\mforall{}L':T  List.  (L'  \mleq{}  L  {}\mRightarrow{}  map(f;filter2(P;L'))  \mleq{}  map(g;filter2(Q;L'))))
{}\mRightarrow{}  causal\_order(L;\mlambda{}i,j.  ((g  L[i])  =  (f  L[j]));\mlambda{}i.(\muparrow{}Q[i]);\mlambda{}i.(\muparrow{}P[i])))

Date html generated: 2017_10_01-AM-08_37_56
Last ObjectModification: 2017_07_26-PM-04_26_42

Theory : list!

Home Index