Step
*
of Lemma
causal_order_or
∀[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;P1;P3)
⇒ causal_order(L;R;P1;λi.((P2 i) ∨ (P3 i))))
BY
{ (((Unfold `causal_order` 0 THEN Reduce 0 THEN Auto THEN ((D (-1)) THENL [FwdThruHyp 8 [(-1)]; FwdThruHyp 9 [(-1)]]))
THENA Auto
)
THEN ExRepD
THEN InstConcl [j]⋅
THEN Auto) }
Latex:
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;P1;P3)
{}\mRightarrow{} causal\_order(L;R;P1;\mlambda{}i.((P2 i) \mvee{} (P3 i))))
By
Latex:
(((Unfold `causal\_order` 0
THEN Reduce 0
THEN Auto
THEN ((D (-1)) THENL [FwdThruHyp 8 [(-1)]; FwdThruHyp 9 [(-1)]]))
THENA Auto
)
THEN ExRepD
THEN InstConcl [j]\mcdot{}
THEN Auto)
Home
Index