---

Step * of Lemma bag-ordering-wellfounded

∀p:ℕ
  ∀[T:Type]
    (T ~ ℕp
    ⇒ (∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]
          (Trans(bag(T);a,b.R[a;b])
          ⇒ (∀a,b:bag(T).  Dec(R[a;b]))
          ⇒ (∀a,b:bag(T).  (sub-bag(T;a;b) ⇒ (¬R[b;a])))
          ⇒ WellFnd{i}(bag(T);a,b.R[a;b]))))
BY
{ (Auto THEN BLemma `no-descending-chain-implies-wellfounded` 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. a : bag(T)@i
9. b : bag(T)@i
10. z : bag(T)@i
11. a R b@i
12. b R z@i
⊢ a R z

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

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}
    \mforall{}[T:Type]
        (T  \msim{}  \mBbbN{}p
        {}\mRightarrow{}  (\mforall{}[R:bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}]
                    (Trans(bag(T);a,b.R[a;b])
                    {}\mRightarrow{}  (\mforall{}a,b:bag(T).    Dec(R[a;b]))
                    {}\mRightarrow{}  (\mforall{}a,b:bag(T).    (sub-bag(T;a;b)  {}\mRightarrow{}  (\mneg{}R[b;a])))
                    {}\mRightarrow{}  WellFnd\{i\}(bag(T);a,b.R[a;b]))))


By

---

Latex:
(Auto  THEN  BLemma  `no-descending-chain-implies-wellfounded`  THEN  Auto)

---

Home Index