---

Step * 1 2 of Lemma implies-bigrel


1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-monotone{i:l}(T;R.F[R])
4. R' : T ⟶ T ⟶ ℙ
5. R' => F[R']
6. n : ℤ
7. [%3] : 0 < n
8. R' => primrec(n - 1;λx,y. True;λm,R. F[R])
9. 1 ≤ n
⊢ R' => F[primrec(n - 1;λx,y. True;λm,R. F[R])]
BY
{ (Unfold `rel-monotone` 3 THEN FHyp 3 [-2] THEN Auto) }

---

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.  R'  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  R'  =>  F[R']
6.  n  :  \mBbbZ{}
7.  [\%3]  :  0  <  n
8.  R'  =>  primrec(n  -  1;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])
9.  1  \mleq{}  n
\mvdash{}  R'  =>  F[primrec(n  -  1;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])]


By

---

Latex:
(Unfold  `rel-monotone`  3  THEN  FHyp  3  [-2]  THEN  Auto)

---

Home Index