---

Step * 3 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])
8. as : bag(T)
9. bs : bag(T)
10. sub-bag(T;as;bs)
⊢ ¬(R[bs;as] ∧ (¬(bs = as ∈ bag(T))))
BY
{ (InstLemma `sub-bag-admissable` [⌜T⌝;⌜R⌝;⌜as⌝;⌜bs⌝]⋅ 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])
8.  as  :  bag(T)
9.  bs  :  bag(T)
10.  sub-bag(T;as;bs)
\mvdash{}  \mneg{}(R[bs;as]  \mwedge{}  (\mneg{}(bs  =  as)))


By

---

Latex:
(InstLemma  `sub-bag-admissable`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index