---

Step * 1 2 2 1 1 1 of Lemma non-homogeneous-add


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
16. ¬(i < n + 1 ∧ j < n + 1)
17. ¬m < n - 1
18. m = (n - 1) ∈ ℤ
⊢ R (s (n - 1)) if i=n + 1 then q else if i=n then p else (s i)
⇐⇒ R (s (n - 1)) if j=n + 1 then q else if j=n then p else (s j)
BY
{ TACTIC:(((Decide i = (n + 1) ∈ ℤ THENA Auto) THEN Reduce 0) THEN (Decide j = (n + 1) ∈ ℤ THENA Auto) THEN Reduce 0) }

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
16. ¬(i < n + 1 ∧ j < n + 1)
17. ¬m < n - 1
18. m = (n - 1) ∈ ℤ
19. i = (n + 1) ∈ ℤ
20. j = (n + 1) ∈ ℤ
⊢ R (s (n - 1)) q ⇐⇒ R (s (n - 1)) q

2
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
16. ¬(i < n + 1 ∧ j < n + 1)
17. ¬m < n - 1
18. m = (n - 1) ∈ ℤ
19. i = (n + 1) ∈ ℤ
20. ¬(j = (n + 1) ∈ ℤ)
⊢ R (s (n - 1)) q ⇐⇒ R (s (n - 1)) if j=n then p else (s j)

3
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
16. ¬(i < n + 1 ∧ j < n + 1)
17. ¬m < n - 1
18. m = (n - 1) ∈ ℤ
19. ¬(i = (n + 1) ∈ ℤ)
20. j = (n + 1) ∈ ℤ
⊢ R (s (n - 1)) if i=n then p else (s i) ⇐⇒ R (s (n - 1)) q

4
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
16. ¬(i < n + 1 ∧ j < n + 1)
17. ¬m < n - 1
18. m = (n - 1) ∈ ℤ
19. ¬(i = (n + 1) ∈ ℤ)
20. ¬(j = (n + 1) ∈ ℤ)
⊢ R (s (n - 1)) if i=n then p else (s i) ⇐⇒ R (s (n - 1)) if j=n then p else (s j)

---

Latex:

---

Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  p  :  \mBbbN{}
5.  q  :  \mBbbN{}
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  \mLeftarrow{}{}\mRightarrow{}  R  (s  (n  -  1))  q
11.  m  :  \mBbbN{}n  +  2
12.  i  :  \mBbbN{}n  +  2
13.  j  :  \mBbbN{}n  +  2
14.  m  <  i
15.  m  <  j
16.  \mneg{}(i  <  n  +  1  \mwedge{}  j  <  n  +  1)
17.  \mneg{}m  <  n  -  1
18.  m  =  (n  -  1)
\mvdash{}  R  (s  (n  -  1))  if  i=n  +  1  then  q  else  if  i=n  then  p  else  (s  i)
\mLeftarrow{}{}\mRightarrow{}  R  (s  (n  -  1))  if  j=n  +  1  then  q  else  if  j=n  then  p  else  (s  j)


By

---

Latex:
TACTIC:(((Decide  i  =  (n  +  1)  THENA  Auto)  THEN  Reduce  0)
                THEN  (Decide  j  =  (n  +  1)  THENA  Auto)
                THEN  Reduce  0)

---

Home Index