---

Step * 2 of Lemma bigrel-iff


1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-monotone{i:l}(T;R.F[R])
4. rel-continuous{i:l}(T;R.F[R])
5. ∨R.F[R] => F[∨R.F[R]]
⊢ F[∨R.F[R]] => ∨R.F[R]
BY
{ ((D 0 THEN Auto)
   THEN RepUR ``bigrel isect-rel`` 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN (With ⌜∨R.F[R]⌝ (D 3)⋅ THENA Auto)
   THEN RepUR ``rel_implies infix_ap`` -1
   THEN BHyp -1 ⋅
   THEN InstLemma `bigrel_wf` [⌜T⌝;⌜F⌝]⋅
   THEN Auto) }

1
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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  F  :  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  rel-monotone\{i:l\}(T;R.F[R])
4.  rel-continuous\{i:l\}(T;R.F[R])
5.  \mvee{}R.F[R]  =>  F[\mvee{}R.F[R]]
\mvdash{}  F[\mvee{}R.F[R]]  =>  \mvee{}R.F[R]


By

---

Latex:
((D  0  THEN  Auto)
  THEN  RepUR  ``bigrel  isect-rel``  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (With  \mkleeneopen{}\mvee{}R.F[R]\mkleeneclose{}  (D  3)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``rel\_implies  infix\_ap``  -1
  THEN  BHyp  -1  \mcdot{}
  THEN  InstLemma  `bigrel\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index