---

Step * of Lemma bigrel-induction-monotone

∀[T:Type]
  ∀P:(T ⟶ T ⟶ ℙ) ⟶ ℙ. ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ.
    (rel-monotone{i:l}(T;R.F[R])
    ⇒ (∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ. ((∀n:ℕ. Rs[n + 1] => Rs[n]) ⇒ (∀n:ℕ. P[Rs[n]]) ⇒ P[isect-rel(ℕ;n.Rs[n])]))
    ⇒ (∀R:T ⟶ T ⟶ ℙ. (P[R] ⇒ P[F[R]]))
    ⇒ P[λx,y. True]
    ⇒ P[∨R.F[R]])
BY
{ (Auto
   THEN Unfold `bigrel` 0
   THEN BackThruSomeHyp
   THEN InductionOnNat
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Repeat (AutoSplit)) }

1
1. 0 + 1 ≠ 0
2. [T] : Type
3. P : (T ⟶ T ⟶ ℙ) ⟶ ℙ
4. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
5. rel-monotone{i:l}(T;R.F[R])
6. ∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ. ((∀n:ℕ. Rs[n + 1] => Rs[n]) ⇒ (∀n:ℕ. P[Rs[n]]) ⇒ P[isect-rel(ℕ;n.Rs[n])])
7. ∀R:T ⟶ T ⟶ ℙ. (P[R] ⇒ P[F[R]])
8. P[λx,y. True]
⊢ F[λx,y. True] => λx,y. True

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
        (rel-monotone\{i:l\}(T;R.F[R])
        {}\mRightarrow{}  (\mforall{}Rs:\mBbbN{}  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
                    ((\mforall{}n:\mBbbN{}.  Rs[n  +  1]  =>  Rs[n])  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  P[Rs[n]])  {}\mRightarrow{}  P[isect-rel(\mBbbN{};n.Rs[n])]))
        {}\mRightarrow{}  (\mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (P[R]  {}\mRightarrow{}  P[F[R]]))
        {}\mRightarrow{}  P[\mlambda{}x,y.  True]
        {}\mRightarrow{}  P[\mvee{}R.F[R]])


By

---

Latex:
(Auto
  THEN  Unfold  `bigrel`  0
  THEN  BackThruSomeHyp
  THEN  InductionOnNat
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Repeat  (AutoSplit))

---

Home Index