---

Step * 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. 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
BY
{ UseTrans ⌜b⌝⋅ }

---

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.  a  :  bag(T)@i
9.  b  :  bag(T)@i
10.  z  :  bag(T)@i
11.  a  R  b@i
12.  b  R  z@i
\mvdash{}  a  R  z


By

---

Latex:
UseTrans  \mkleeneopen{}b\mkleeneclose{}\mcdot{}

---

Home Index