---

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

.....decidable?..... 
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)
⊢ Dec(R[as;bs] ∧ (¬(as = bs ∈ bag(T))))
BY
{ (InstLemma `decidable__equal_equipollent` [⌜T⌝;⌜k⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....decidable?..... 
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)
\mvdash{}  Dec(R[as;bs]  \mwedge{}  (\mneg{}(as  =  bs)))


By

---

Latex:
(InstLemma  `decidable\_\_equal\_equipollent`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index