Nuprl Lemma : causal_order_sigma

[T,A:Type].
  ∀L:T List
    ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ]. ∀[P,Q:A ⟶ ℕ||L|| ⟶ ℙ].
      (Trans(ℕ||L||)(R _1 _2)
       (∀x:A. causal_order(L;R;λi.P[x;i];λi.Q[x;i]))
       causal_order(L;R;λi.∃x:A. P[x;i];λi.∃x:A. Q[x;i]))


Proof




Definitions occuring in Statement :  causal_order: causal_order(L;R;P;Q) length: ||as|| list: List trans: Trans(T;x,y.E[x; y]) int_seg: {i..j-} uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a lambda: λx.A[x] function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  causal_order: causal_order(L;R;P;Q) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q exists: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s1;s2] so_apply: x[s] and: P ∧ Q int_seg: {i..j-} subtype_rel: A ⊆B so_lambda: λ2y.t[x; y] cand: c∧ B
Lemmas referenced :  exists_wf int_seg_wf length_wf all_wf le_wf subtype_rel_self trans_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality lambdaEquality applyEquality hypothesis natural_numberEquality functionEquality productEquality setElimination rename instantiate universeEquality because_Cache inhabitedIsType functionIsType universeIsType dependent_functionElimination independent_functionElimination dependent_pairFormation independent_pairFormation

Latex:
\mforall{}[T,A:Type].
    \mforall{}L:T  List
        \mforall{}[R:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P,Q:A  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}].
            (Trans(\mBbbN{}||L||)(R  $_{1}$  $_{2}$)
            {}\mRightarrow{}  (\mforall{}x:A.  causal\_order(L;R;\mlambda{}i.P[x;i];\mlambda{}i.Q[x;i]))
            {}\mRightarrow{}  causal\_order(L;R;\mlambda{}i.\mexists{}x:A.  P[x;i];\mlambda{}i.\mexists{}x:A.  Q[x;i]))



Date html generated: 2019_10_15-AM-10_57_41
Last ObjectModification: 2018_09_27-AM-09_52_36

Theory : list!


Home Index