---

Step * 1 1 1 1 of Lemma fan-implies-barred-not-unbounded


1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. ∀bs,as:T List.  (as ≤ bs ⇒ (¬(A) bs) ⇒ (¬(A) as))
5. k : ℕ
6. as : T List
7. ||as|| = (k + 1) ∈ ℤ
8. ¬(A) as
9. n : ℕk
10. A map(λi.if i <z k then as[i] else as[0] fi ;upto(n))
11. n ≤ ||as||
12. i : ℕ
13. i < n
⊢ map(λi.if i <z k then as[i] else as[0] fi ;upto(n))[i] = as[i] ∈ T
BY
{ ((RWO "select-map" 0 THENA Auto) THEN Reduce 0 THEN RWO "length_upto select-upto" 0 THEN Auto THEN AutoSplit)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  dbar(T;A)
4.  \mforall{}bs,as:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (\mneg{}(A)  bs)  {}\mRightarrow{}  (\mneg{}(A)  as))
5.  k  :  \mBbbN{}
6.  as  :  T  List
7.  ||as||  =  (k  +  1)
8.  \mneg{}(A)  as
9.  n  :  \mBbbN{}k
10.  A  map(\mlambda{}i.if  i  <z  k  then  as[i]  else  as[0]  fi  ;upto(n))
11.  n  \mleq{}  ||as||
12.  i  :  \mBbbN{}
13.  i  <  n
\mvdash{}  map(\mlambda{}i.if  i  <z  k  then  as[i]  else  as[0]  fi  ;upto(n))[i]  =  as[i]


By

---

Latex:
((RWO  "select-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWO  "length\_upto  select-upto"  0
  THEN  Auto
  THEN  AutoSplit)\mcdot{}

---

Home Index