---

Step * 1 of Lemma bag-admissable-well-founded


1. k : ℕ
2. [T] : Type
3. T ~ ℕk
4. [R] : bag(T) ⟶ bag(T) ⟶ ℙ
5. ∀as,bs:bag(T).  Dec(R[as;bs])
6. Order(bag(T);as,bs.R[as;bs])
7. bag-admissable(T;as,bs.R[as;bs])
⊢ Trans(bag(T);as,bs.R[as;bs] ∧ (¬(as = bs ∈ bag(T))))
BY
{ (D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  [T]  :  Type
3.  T  \msim{}  \mBbbN{}k
4.  [R]  :  bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}as,bs:bag(T).    Dec(R[as;bs])
6.  Order(bag(T);as,bs.R[as;bs])
7.  bag-admissable(T;as,bs.R[as;bs])
\mvdash{}  Trans(bag(T);as,bs.R[as;bs]  \mwedge{}  (\mneg{}(as  =  bs)))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index