---

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


1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. down-closed(T;¬(A))
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))
⊢ False
BY
{ OnMaybeHyp 4 (\h. (RepUR ``down-closed R-closed`` h
                     THEN ((InstHyp [⌜as⌝; ⌜map(λi.if i <z k then as[i] else as[0] fi ;upto(n))⌝] h⋅
                           THENM (RepUR ``predicate-not`` (-1) THEN Auto)
                           )
                           THENA (Auto
                                  THEN (BLemma `iseg_select`  THEN Auto)
                                  THEN (All (RWW "map-length length_upto")⋅ THENA Auto)
                                  THEN Auto')
                           )
                     )) }

1
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

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  dbar(T;A)
4.  down-closed(T;\mneg{}(A))
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))
\mvdash{}  False


By

---

Latex:
OnMaybeHyp  4  (\mbackslash{}h.  (RepUR  ``down-closed  R-closed``  h
                                      THEN  ((InstHyp  [\mkleeneopen{}as\mkleeneclose{};  \mkleeneopen{}map(\mlambda{}i.if  i  <z  k  then  as[i]  else  as[0]  fi  ;upto(n))\mkleeneclose{}]  h\mcdot{}
                                                  THENM  (RepUR  ``predicate-not``  (-1)  THEN  Auto)
                                                  )
                                                  THENA  (Auto
                                                                THEN  (BLemma  `iseg\_select`    THEN  Auto)
                                                                THEN  (All  (RWW  "map-length  length\_upto")\mcdot{}  THENA  Auto)
                                                                THEN  Auto')
                                                  )
                                      ))

---

Home Index