---

Step * of Lemma implies-bigrel

No Annotations
∀[T:Type]
  ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ. (rel-monotone{i:l}(T;R.F[R]) ⇒ (∀R':T ⟶ T ⟶ ℙ. (R' => F[R'] ⇒ R' => νR.F[R])))
BY
{ (Auto THEN Unfold `bigrel` 0 THEN Assert ⌜∀n:ℕ. R' => primrec(n;λx,y. True;λm,R. F[R])⌝⋅) }

1
.....assertion..... 
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']
⊢ ∀n:ℕ. R' => primrec(n;λx,y. True;λm,R. F[R])

2
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:ℕ. R' => primrec(n;λx,y. True;λm,R. F[R])
⊢ R' => ⋂n:ℕ. primrec(n;λx,y. True;λm,R. F[R])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
        (rel-monotone\{i:l\}(T;R.F[R])  {}\mRightarrow{}  (\mforall{}R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (R'  =>  F[R']  {}\mRightarrow{}  R'  =>  \mnu{}R.F[R])))


By

---

Latex:
(Auto  THEN  Unfold  `bigrel`  0  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  R'  =>  primrec(n;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])\mkleeneclose{}\mcdot{})

---

Home Index