---

Step * of Lemma oalist_pr_length_ind

∀a:LOSet. ∀b:AbDMon. ∀Q:((|a| × |b|) List) ⟶ ((|a| × |b|) List) ⟶ ℙ.
  ((∀ps,qs:|oal(a;b)|.  ((∀us,vs:|oal(a;b)|.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ Q[us;vs])) ⇒ Q[ps;qs]))
  ⇒ {∀ps,qs:|oal(a;b)|.  Q[ps;qs]})
BY
{ ((RepD) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. Q : ((|a| × |b|) List) ⟶ ((|a| × |b|) List) ⟶ ℙ
4. ∀ps,qs:|oal(a;b)|.  ((∀us,vs:|oal(a;b)|.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ Q[us;vs])) ⇒ Q[ps;qs])
⊢ ∀ps,qs:|oal(a;b)|.  Q[ps;qs]

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}Q:((|a|  \mtimes{}  |b|)  List)  {}\mrightarrow{}  ((|a|  \mtimes{}  |b|)  List)  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}ps,qs:|oal(a;b)|.
            ((\mforall{}us,vs:|oal(a;b)|.    (||us||  +  ||vs||  <  ||ps||  +  ||qs||  {}\mRightarrow{}  Q[us;vs]))  {}\mRightarrow{}  Q[ps;qs]))
    {}\mRightarrow{}  \{\mforall{}ps,qs:|oal(a;b)|.    Q[ps;qs]\})


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index