---

Step * 1 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])
⊢ ∨R.F[R] => F[∨R.F[R]]
BY
{ ((With ⌜λn.primrec(n;λx,y. True;λm,R. F[R])⌝ (D 4)⋅ THEN Auto)
   THEN Reduce (-1)
   THEN Fold `bigrel` (-1)
   THEN RepeatFor 3 (ParallelLast)
   THEN All (Unfold `bigrel`)
   THEN ParallelLast
   THEN All (Unfold `isect-rel`)
   THEN All Reduce
   THEN Auto
   THEN (InstHyp [⌜n + 1⌝] (-2)⋅ THENA Auto)
   THEN (RWO "primrec-unroll" (-1) THENA Auto)
   THEN SplitOnHypITE -1 
   THEN Reduce (-2)
   THEN Auto
   THEN Subst' (n + 1) - 1 ~ n -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.  rel-continuous\{i:l\}(T;R.F[R])
\mvdash{}  \mvee{}R.F[R]  =>  F[\mvee{}R.F[R]]


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}n.primrec(n;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])\mkleeneclose{}  (D  4)\mcdot{}  THEN  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `bigrel`  (-1)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  All  (Unfold  `bigrel`)
  THEN  ParallelLast
  THEN  All  (Unfold  `isect-rel`)
  THEN  All  Reduce
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (RWO  "primrec-unroll"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Reduce  (-2)
  THEN  Auto
  THEN  Subst'  (n  +  1)  -  1  \msim{}  n  -2
  THEN  Auto)

---

Home Index