---

Step * 2 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
⊢ no-descending-chain(bag(T);R)
BY
{ (D 0 THEN Auto) }

1
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)))

---

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
\mvdash{}  no-descending-chain(bag(T);R)


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index