---

Step * 2 1 of Lemma bigrel-iff


1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-continuous{i:l}(T;R.F[R])
4. ∨R.F[R] => F[∨R.F[R]]
5. x : T
6. y : T
7. x F[∨R.F[R]] y
8. n : {1...}
9. ∀R2:T ⟶ T ⟶ ℙ. ((∀x,y:T.  ((∨R.F[R] x y) ⇒ (R2 x y))) ⇒ (∀x,y:T.  ((F[∨R.F[R]] x y) ⇒ (F[R2] x y))))
10. ∨R.F[R] ∈ T ⟶ T ⟶ ℙ
11. x1 : T
12. y1 : T
13. ∨R.F[R] x1 y1
⊢ primrec(n - 1;λx,y. True;λm,R. F[R]) x1 y1
BY
{ (RepUR ``bigrel isect-rel`` (-1) THEN BHyp -1  THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  F  :  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  rel-continuous\{i:l\}(T;R.F[R])
4.  \mvee{}R.F[R]  =>  F[\mvee{}R.F[R]]
5.  x  :  T
6.  y  :  T
7.  x  F[\mvee{}R.F[R]]  y
8.  n  :  \{1...\}
9.  \mforall{}R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}x,y:T.    ((\mvee{}R.F[R]  x  y)  {}\mRightarrow{}  (R2  x  y)))  {}\mRightarrow{}  (\mforall{}x,y:T.    ((F[\mvee{}R.F[R]]  x  y)  {}\mRightarrow{}  (F[R2]  x  y))))
10.  \mvee{}R.F[R]  \mmember{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
11.  x1  :  T
12.  y1  :  T
13.  \mvee{}R.F[R]  x1  y1
\mvdash{}  primrec(n  -  1;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])  x1  y1


By

---

Latex:
(RepUR  ``bigrel  isect-rel``  (-1)  THEN  BHyp  -1    THEN  Auto)\mcdot{}

---

Home Index