---

Step * 1 1 1 of Lemma list_pr_length_ind


1. T : Type
2. Q : (T List) ⟶ (T List) ⟶ ℙ
3. ∀ps,qs:T List.  ((∀us,vs:T List.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ Q[us;vs])) ⇒ Q[ps;qs])
4. rs : T List × (T List)
5. ∀r1:T List × (T List). (||fst(r1)|| + ||snd(r1)|| < ||fst(rs)|| + ||snd(rs)|| ⇒ Q[fst(r1);snd(r1)])
⊢ Q[fst(rs);snd(rs)]
BY
{ ((BHyp 3 THENM RepD) THENA Auto) }

1
1. T : Type
2. Q : (T List) ⟶ (T List) ⟶ ℙ
3. ∀ps,qs:T List.  ((∀us,vs:T List.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ Q[us;vs])) ⇒ Q[ps;qs])
4. rs : T List × (T List)
5. ∀r1:T List × (T List). (||fst(r1)|| + ||snd(r1)|| < ||fst(rs)|| + ||snd(rs)|| ⇒ Q[fst(r1);snd(r1)])
6. us : T List
7. vs : T List
8. ||us|| + ||vs|| < ||fst(rs)|| + ||snd(rs)||
⊢ Q[us;vs]

---

Latex:

---

Latex:

1.  T  :  Type
2.  Q  :  (T  List)  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}ps,qs:T  List.    ((\mforall{}us,vs:T  List.    (||us||  +  ||vs||  <  ||ps||  +  ||qs||  {}\mRightarrow{}  Q[us;vs]))  {}\mRightarrow{}  Q[ps;qs])
4.  rs  :  T  List  \mtimes{}  (T  List)
5.  \mforall{}r1:T  List  \mtimes{}  (T  List)
          (||fst(r1)||  +  ||snd(r1)||  <  ||fst(rs)||  +  ||snd(rs)||  {}\mRightarrow{}  Q[fst(r1);snd(r1)])
\mvdash{}  Q[fst(rs);snd(rs)]


By

---

Latex:
((BHyp  3  THENM  RepD)  THENA  Auto)

---

Home Index