---

Step * 1 1 1 of Lemma ancestral-logic-example1


9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
10. x : Dom@i
11. y : Dom@i
12. P x y@i
⊢ TC(λa,b.Q a b)(x,y)
BY
{ (FOAllElim (-4) `x'  THEN FOAllElim (-1) `y'  THEN FOImpliesElim (-1)) }

1
9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
10. x : Dom@i
11. y : Dom@i
12. P x y@i
13. ∀y:Dom. ((P x y) ⇒ (Q x y))@i
14. (P x y) ⇒ (Q x y)@i
⊢ P x y

2
9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
10. x : Dom@i
11. y : Dom@i
12. P x y@i
13. ∀y:Dom. ((P x y) ⇒ (Q x y))@i
14. (P x y) ⇒ (Q x y)@i
15. Q x y@i
⊢ TC(λa,b.Q a b)(x,y)

---

Latex:



9.  \mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  (Q  x  y))@i
10.  x  :  Dom@i
11.  y  :  Dom@i
12.  P  x  y@i
\mvdash{}  TC(\mlambda{}a,b.Q  a  b)(x,y)


By

(FOAllElim  (-4)  `x'    THEN  FOAllElim  (-1)  `y'    THEN  FOImpliesElim  (-1))

---

Home Index