---

Step * of Lemma bag-admissable-well-founded

∀k:ℕ
  ∀[T:Type]
    (T ~ ℕk
    ⇒ (∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]
          ((∀as,bs:bag(T).  Dec(R[as;bs]))
          ⇒ Order(bag(T);as,bs.R[as;bs])
          ⇒ bag-admissable(T;as,bs.R[as;bs])
          ⇒ WellFnd{i}(bag(T);as,bs.R[as;bs] ∧ (¬(as = bs ∈ bag(T)))))))
BY
{ (Auto THEN Using [`p',⌜k⌝] (BLemma `bag-ordering-wellfounded`)⋅ THEN Auto) }

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

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

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

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}
    \mforall{}[T:Type]
        (T  \msim{}  \mBbbN{}k
        {}\mRightarrow{}  (\mforall{}[R:bag(T)  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  \mBbbP{}]
                    ((\mforall{}as,bs:bag(T).    Dec(R[as;bs]))
                    {}\mRightarrow{}  Order(bag(T);as,bs.R[as;bs])
                    {}\mRightarrow{}  bag-admissable(T;as,bs.R[as;bs])
                    {}\mRightarrow{}  WellFnd\{i\}(bag(T);as,bs.R[as;bs]  \mwedge{}  (\mneg{}(as  =  bs))))))


By

---

Latex:
(Auto  THEN  Using  [`p',\mkleeneopen{}k\mkleeneclose{}]  (BLemma  `bag-ordering-wellfounded`)\mcdot{}  THEN  Auto)

---

Home Index