---

Step * 1 1 of Lemma W-sup_wf


1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. ↑isl(p 0 a)
8. W-bars(f outl(p 0 a);λn.(p (n + 1)))
⊢ W-bars(W-sup(a;f);p)
BY
{ (RepeatFor 2 (ParallelLast)
   THEN ExRepD
   THEN With ⌜n + 1⌝ (D 0)⋅
   THEN Auto
   THEN RecUnfold `W-select` 0
   THEN (RWO "null-map" 0 THENA Auto)
   THEN (RWO "null-upto" 0 THENA Auto)
   THEN AutoSplit
   THEN (RW (AddrC [1] (SweepUpC (LemmaC `upto_decomp2`))) 0 THENA Auto)⋅
   THEN Reduce 0)⋅ }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. ↑isl(p 0 a)
8. n : ℕ
9. n + 1 ≠ 0
10. ↑isr(W-select(f outl(p 0 a);map(λn.(p (n + 1));upto(n))))
⊢ ↑isr(case p 0 a of inl(b) => W-select(f b;map(p;map(λi.(i + 1);upto((n + 1) - 1)))) | inr(z) => inr z )

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  A
4.  f  :  B[a]  {}\mrightarrow{}  W-type(A;  a.B[a])
5.  p  :  \mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?)@i
6.  W-sup(a;f)  \mmember{}  co-W(A;a.B[a])
7.  \muparrow{}isl(p  0  a)
8.  W-bars(f  outl(p  0  a);\mlambda{}n.(p  (n  +  1)))
\mvdash{}  W-bars(W-sup(a;f);p)


By

---

Latex:
(RepeatFor  2  (ParallelLast)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}n  +  1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RecUnfold  `W-select`  0
  THEN  (RWO  "null-map"  0  THENA  Auto)
  THEN  (RWO  "null-upto"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (RW  (AddrC  [1]  (SweepUpC  (LemmaC  `upto\_decomp2`)))  0  THENA  Auto)\mcdot{}
  THEN  Reduce  0)\mcdot{}

---

Home Index