---

Step * 1 2 1 of Lemma W-type-ext


1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
10. n : ℕ
11. ↑isr(W-select(<a, x1>;map(λn.if (n =z 0) then λz.if eq z a then inl b else inr ⋅  fi  else p (n - 1) fi ;upto(n))))
12. ¬(n = 0 ∈ ℤ)
⊢ ↑isr(W-select(x1 b;map(p;upto(n - 1))))
BY
{ ((RWO "upto_decomp2" (-2) THENA Auto)
   THEN Reduce (-2)
   THEN RecUnfold `W-select` (-2)
   THEN Reduce (-2)
   THEN (SplitOnHypITE -2  THENA Auto)
   THEN Try ((D -1 THEN Auto))
   THEN (RWO "map-map" (-3) THENA Auto)
   THEN RepUR ``compose`` (-3)
   THEN NthHypSq (-3)
   THEN RepeatFor 3 (EqCD)
   THEN Try (Complete (Auto)))⋅ }

1
1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
10. n : ℕ
11. ↑isr(W-select(x1 b;map(λx.if (x + 1 =z 0) then λz.if eq z a then inl b else inr ⋅  fi  else p ((x + 1) - 1) fi ;
                           upto(n - 1))))
12. ¬(n = 0 ∈ ℤ)
13. a = a ∈ A
⊢ map(p;upto(n - 1)) ~ map(λx.if (x + 1 =z 0) then λz.if eq z a then inl b else inr ⋅  fi  else p ((x + 1) - 1) fi ;
                           upto(n - 1))

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mforall{}x,y:A.    Dec(x  =  y)
3.  B  :  A  {}\mrightarrow{}  Type
4.  a  :  A
5.  x1  :  B[a]  {}\mrightarrow{}  co-W(A;a.B[a])
6.  \mforall{}p:\mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?).  W-bars(<a,  x1>p)
7.  b  :  B[a]
8.  p  :  \mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?)@i
9.  eq  :  EqDecider(A)
10.  n  :  \mBbbN{}
11.  \muparrow{}isr(W-select(<a,  x1>map(\mlambda{}n.if  (n  =\msubz{}  0)  then  \mlambda{}z.if  eq  z  a  then  inl  b  else  inr  \mcdot{}    fi    else  p  (n  \000C-  1)  fi  ;
                        upto(n))))
12.  \mneg{}(n  =  0)
\mvdash{}  \muparrow{}isr(W-select(x1  b;map(p;upto(n  -  1))))


By

---

Latex:
((RWO  "upto\_decomp2"  (-2)  THENA  Auto)
  THEN  Reduce  (-2)
  THEN  RecUnfold  `W-select`  (-2)
  THEN  Reduce  (-2)
  THEN  (SplitOnHypITE  -2    THENA  Auto)
  THEN  Try  ((D  -1  THEN  Auto))
  THEN  (RWO  "map-map"  (-3)  THENA  Auto)
  THEN  RepUR  ``compose``  (-3)
  THEN  NthHypSq  (-3)
  THEN  RepeatFor  3  (EqCD)
  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index