Nuprl Lemma : causal_order_transitivity

[T:Type]
  ∀L:T List
    ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ]. ∀[P1,P2,P3:ℕ||L|| ⟶ ℙ].
      (Trans(ℕ||L||)(R _1 _2)  causal_order(L;R;P1;P2)  causal_order(L;R;P2;P3)  causal_order(L;R;P1;P3))


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: all: x:A. B[x] implies:  Q apply: a 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 member: t ∈ T exists: x:A. B[x] and: P ∧ Q cand: c∧ B guard: {T} int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] trans: Trans(T;x,y.E[x; y])
Lemmas referenced :  int_seg_properties length_wf decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf le_wf int_seg_wf all_wf exists_wf subtype_rel_self trans_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation cut hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination productElimination dependent_pairFormation introduction extract_by_obid isectElimination natural_numberEquality setElimination rename because_Cache unionElimination independent_isectElimination approximateComputation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation productEquality applyEquality functionEquality instantiate universeEquality cumulativity

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[R:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P1,P2,P3:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}].
            (Trans(\mBbbN{}||L||)(R  $_{1}$  $_{2}$)
            {}\mRightarrow{}  causal\_order(L;R;P1;P2)
            {}\mRightarrow{}  causal\_order(L;R;P2;P3)
            {}\mRightarrow{}  causal\_order(L;R;P1;P3))



Date html generated: 2018_05_21-PM-06_20_38
Last ObjectModification: 2018_05_19-PM-05_32_49

Theory : list!


Home Index