---

Step * 1 1 1 1 of Lemma AF-uniform-induction4

.....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) ∈ ℙ
BY
{ (RepUR ``so_apply`` 0 THEN RepeatFor 3 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
.....assertion..... 
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]  =  (\mlambda{}\msubtwo{}x  y.R[x;y]\msupplus{}  x  y)


By

---

Latex:
(RepUR  ``so\_apply``  0  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index