---

Step * 1 of Lemma oalist_pr_length_ind


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]
BY
{ Assert ∀rs:|oal(a;b)| × |oal(a;b)|. Q[fst(rs);snd(rs)] 
THENM ((SeqOnM [RepD ; InstHyp [<ps, qs>] (-3) 
       ;Reduce (-1) ; BHyp (-1)]) THEN Auto) 
THEN ((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])
5. rs : |oal(a;b)| × |oal(a;b)|
⊢ Q[fst(rs);snd(rs)]

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mforall{}rs:|oal(a;b)|  \mtimes{}  |oal(a;b)|.  Q[fst(rs);snd(rs)] 
THENM  ((SeqOnM  [RepD  ;  InstHyp  [<ps,  qs>]  (-3) 
              ;Reduce  (-1)  ;  BHyp  (-1)])  THEN  Auto) 
THEN  ((RepD)  THENA  Auto) 

---

Home Index