---

Step * 1 1 1 of Lemma AF-induction4


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. R' : T ⟶ T ⟶ ℙ
4. AFx,y:T.R'[x;y]
5. ∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))
6. Q : T ⟶ ℙ
7. AFx,y:T.R'[x;y]
8. x : T
9. y : T
10. λ2x y.R[x;y]+ x y
⊢ R+[x;y]
BY
{ (NthHypEq (-1) THEN Auto) }

1
.....assertion..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. R' : T ⟶ T ⟶ ℙ
4. AFx,y:T.R'[x;y]
5. ∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))
6. Q : T ⟶ ℙ
7. AFx,y:T.R'[x;y]
8. x : T
9. y : T
10. λ2x y.R[x;y]+ x y
⊢ R+[x;y] = (λ2x y.R[x;y]+ x y) ∈ ℙ

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  R'  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  AFx,y:T.R'[x;y]
5.  \mforall{}x,y:T.    (R\msupplus{}[x;y]  {}\mRightarrow{}  (\mneg{}R'[x;y]))
6.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
7.  AFx,y:T.R'[x;y]
8.  x  :  T
9.  y  :  T
10.  \mlambda{}\msubtwo{}x  y.R[x;y]\msupplus{}  x  y
\mvdash{}  R\msupplus{}[x;y]


By

---

Latex:
(NthHypEq  (-1)  THEN  Auto)

---

Home Index