---

Step * of 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]))
BY
{ ((Unfold `causal_order` 0 THEN Reduce 0) THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. [A] : Type
3. L : T List
4. [R] : ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ
5. [P] : A ⟶ ℕ||L|| ⟶ ℙ
6. [Q] : A ⟶ ℕ||L|| ⟶ ℙ
7. Trans(ℕ||L||)(R _1 _2)
8. ∀x:A. ∀i:ℕ||L||.  (Q[x;i] ⇒ (∃j:ℕ||L||. (((j ≤ i) ∧ P[x;j]) ∧ (R j i))))
9. i : ℕ||L||
10. x : A
11. Q[x;i]
⊢ ∃j:ℕ||L||. (((j ≤ i) ∧ (∃x:A. P[x;j])) ∧ (R j i))

---

Latex:

---

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]))


By

---

Latex:
((Unfold  `causal\_order`  0  THEN  Reduce  0)  THEN  Auto  THEN  ExRepD)

---

Home Index