---

Step * 1 of Lemma causal_order_sigma


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))
BY
{ (InstHyp [x;i] (-4) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  L  :  T  List
4.  [R]  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}
5.  [P]  :  A  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}
6.  [Q]  :  A  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}
7.  Trans(\mBbbN{}||L||)(R  $_{1}$  $_{2}$)
8.  \mforall{}x:A.  \mforall{}i:\mBbbN{}||L||.    (Q[x;i]  {}\mRightarrow{}  (\mexists{}j:\mBbbN{}||L||.  (((j  \mleq{}  i)  \mwedge{}  P[x;j])  \mwedge{}  (R  j  i))))
9.  i  :  \mBbbN{}||L||
10.  x  :  A
11.  Q[x;i]
\mvdash{}  \mexists{}j:\mBbbN{}||L||.  (((j  \mleq{}  i)  \mwedge{}  (\mexists{}x:A.  P[x;j]))  \mwedge{}  (R  j  i))


By

---

Latex:
(InstHyp  [x;i]  (-4)  THEN  Auto)

---

Home Index