---

Step * of Lemma non-homogeneous-add

∀[R:ℕ ⟶ ℕ ⟶ ℙ]
  ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀p,q:ℕ.
    (p < q
    ⇒ homogeneous(R;n + 1;s.p@n)
    ⇒ homogeneous(R;n + 1;s.q@n)
    ⇒ (¬homogeneous(R;n + 2;s.p@n.q@n + 1))
    ⇒ {0 < n ∧ (¬(R (s (n - 1)) p ⇐⇒ R (s (n - 1)) q))})
BY
{ TACTIC:(Intros
          THEN (Assert 0 < n BY
                      (SupposeNot
                       THEN D -2
                       THEN (BLemma `le2-homogeneous` THEN Auto)
                       THEN D 0
                       THEN RepUR ``seq-add`` 0
                       THEN Auto))
          THEN D 0
          THEN Try (Trivial)
          THEN ParallelOp -2
          THEN D 0
          THEN Try (Complete (EAuto 1))
          THEN (UnivCD THENA Auto)) }

1
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. p : ℕ
5. q : ℕ
6. p < q
7. homogeneous(R;n + 1;s.p@n)
8. homogeneous(R;n + 1;s.q@n)
9. 0 < n
10. R (s (n - 1)) p ⇐⇒ R (s (n - 1)) q
11. m : ℕn + 2
12. i : ℕn + 2
13. j : ℕn + 2
14. m < i
15. m < j
⊢ R (s.p@n.q@n + 1 m) (s.p@n.q@n + 1 i) ⇐⇒ R (s.p@n.q@n + 1 m) (s.p@n.q@n + 1 j)

---

Latex:

---

Latex:
\mforall{}[R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}]
    \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.  \mforall{}p,q:\mBbbN{}.
        (p  <  q
        {}\mRightarrow{}  homogeneous(R;n  +  1;s.p@n)
        {}\mRightarrow{}  homogeneous(R;n  +  1;s.q@n)
        {}\mRightarrow{}  (\mneg{}homogeneous(R;n  +  2;s.p@n.q@n  +  1))
        {}\mRightarrow{}  \{0  <  n  \mwedge{}  (\mneg{}(R  (s  (n  -  1))  p  \mLeftarrow{}{}\mRightarrow{}  R  (s  (n  -  1))  q))\})


By

---

Latex:
TACTIC:(Intros
                THEN  (Assert  0  <  n  BY
                                        (SupposeNot
                                          THEN  D  -2
                                          THEN  (BLemma  `le2-homogeneous`  THEN  Auto)
                                          THEN  D  0
                                          THEN  RepUR  ``seq-add``  0
                                          THEN  Auto))
                THEN  D  0
                THEN  Try  (Trivial)
                THEN  ParallelOp  -2
                THEN  D  0
                THEN  Try  (Complete  (EAuto  1))
                THEN  (UnivCD  THENA  Auto))

---

Home Index