---

Step * 1 of Lemma implies-bigrel

.....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])
BY
{ (InductionOnNat THEN (RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoSplit) }

1
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. 0 < 1
⊢ R' => λx,y. True

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 : ℤ
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])]

---

Latex:

---

Latex:
.....assertion..... 
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']
\mvdash{}  \mforall{}n:\mBbbN{}.  R'  =>  primrec(n;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])


By

---

Latex:
(InductionOnNat  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)  THEN  OldAutoSplit)

---

Home Index