---

Step * 2 1 of Lemma bag-ordering-wellfounded


1. p : ℕ@i
2. [T] : Type
3. T ~ ℕp@i
4. [R] : bag(T) ⟶ bag(T) ⟶ ℙ
5. Trans(bag(T);a,b.R[a;b])@i
6. ∀a,b:bag(T).  Dec(R[a;b])@i
7. ∀a,b:bag(T).  (sub-bag(T;a;b) ⇒ (¬R[b;a]))@i
8. f : ℕ ⟶ bag(T)@i
⊢ ∃j:ℕ. ∃i:ℕj. (¬((f j) R (f i)))
BY
{ ((InstLemma `bag-dickson-lemma` [⌜p⌝;⌜T⌝;⌜f⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN FHyp (-5) [-1]
   THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}@i
2.  [T]  :  Type
3.  T  \msim{}  \mBbbN{}p@i
4.  [R]  :  bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}
5.  Trans(bag(T);a,b.R[a;b])@i
6.  \mforall{}a,b:bag(T).    Dec(R[a;b])@i
7.  \mforall{}a,b:bag(T).    (sub-bag(T;a;b)  {}\mRightarrow{}  (\mneg{}R[b;a]))@i
8.  f  :  \mBbbN{}  {}\mrightarrow{}  bag(T)@i
\mvdash{}  \mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  (\mneg{}((f  j)  R  (f  i)))


By

---

Latex:
((InstLemma  `bag-dickson-lemma`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  FHyp  (-5)  [-1]
  THEN  Auto)

---

Home Index