---

Step * 2 1 1 of Lemma unshuffle-odd-length


1. v1 : ℕ
2. v2 : ℕ
⊢ (v1 + 1) + 1 <z 2 ~ (v2 + 1) + 1 <z 2
BY
{ (((Subst' (v1 + 1) + 1 <z 2 ~ ff 0 THENA Auto) THEN (Subst' (v2 + 1) + 1 <z 2 ~ ff 0 THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:

1.  v1  :  \mBbbN{}
2.  v2  :  \mBbbN{}
\mvdash{}  (v1  +  1)  +  1  <z  2  \msim{}  (v2  +  1)  +  1  <z  2


By

---

Latex:
(((Subst'  (v1  +  1)  +  1  <z  2  \msim{}  ff  0  THENA  Auto)  THEN  (Subst'  (v2  +  1)  +  1  <z  2  \msim{}  ff  0  THENA  Auto))
  THEN  Auto
  )

---

Home Index