Step * 2 1 1 1 1 of Lemma weakly-safe-extension

.....antecedent..... 
1. : ℕ ⟶ ℕ ⟶ ℙ
2. : ℕ
3. : ℕn ⟶ ℕ
4. weakly-safe-seq(R;n;s)
5. ¬(∀p,q:ℕ.
       (homogeneous(R;n 1;s.p@n)  homogeneous(R;n 1;s.q@n)  p <  (¬¬homogeneous(R;n 2;s.p@n.q@n 1))))
6. : ℕ
7. : ℕ
8. homogeneous(R;n 1;s.p@n)
9. homogeneous(R;n 1;s.q@n)
10. p < q
11. ¬homogeneous(R;n 2;s.p@n.q@n 1)
⊢ w∃∞x.homogeneous(R;n 2;s.p@n.x@n 1) ∨ homogeneous(R;n 2;s.q@n.x@n 1)
BY
TACTIC:((D THEN Auto)
          THEN (Assert ∃m:ℕ(x < m ∧ q < m) BY
                      (Decide ⌜x ≤ q⌝⋅
                       THEN Auto
                       THEN Try ((With ⌜1⌝ (D 0)⋅ THEN Complete (Auto)))
                       THEN Try ((With ⌜1⌝ (D 0)⋅ THEN Complete (Auto)))))
          THEN -1
          THEN (With ⌜m⌝ (D 4)⋅ THENA Auto)) }

1
1. : ℕ ⟶ ℕ ⟶ ℙ
2. : ℕ
3. : ℕn ⟶ ℕ
4. ¬(∀p,q:ℕ.
       (homogeneous(R;n 1;s.p@n)  homogeneous(R;n 1;s.q@n)  p <  (¬¬homogeneous(R;n 2;s.p@n.q@n 1))))
5. : ℕ
6. : ℕ
7. homogeneous(R;n 1;s.p@n)
8. homogeneous(R;n 1;s.q@n)
9. p < q
10. ¬homogeneous(R;n 2;s.p@n.q@n 1)
11. : ℕ
12. : ℕ
13. x < m ∧ q < m
14. ¬¬(∃q@0:ℕ(m < q@0 ∧ homogeneous(R;n 1;s.q@0@n)))
⊢ ¬¬(∃q@0:ℕ(x < q@0 ∧ (homogeneous(R;n 2;s.p@n.q@0@n 1) ∨ homogeneous(R;n 2;s.q@n.q@0@n 1))))


Latex:


Latex:
.....antecedent..... 
1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  weakly-safe-seq(R;n;s)
5.  \mneg{}(\mforall{}p,q:\mBbbN{}.
              (homogeneous(R;n  +  1;s.p@n)
              {}\mRightarrow{}  homogeneous(R;n  +  1;s.q@n)
              {}\mRightarrow{}  p  <  q
              {}\mRightarrow{}  (\mneg{}\mneg{}homogeneous(R;n  +  2;s.p@n.q@n  +  1))))
6.  p  :  \mBbbN{}
7.  q  :  \mBbbN{}
8.  homogeneous(R;n  +  1;s.p@n)
9.  homogeneous(R;n  +  1;s.q@n)
10.  p  <  q
11.  \mneg{}homogeneous(R;n  +  2;s.p@n.q@n  +  1)
\mvdash{}  w\mexists{}\minfty{}x.homogeneous(R;n  +  2;s.p@n.x@n  +  1)  \mvee{}  homogeneous(R;n  +  2;s.q@n.x@n  +  1)


By


Latex:
TACTIC:((D  0  THEN  Auto)
                THEN  (Assert  \mexists{}m:\mBbbN{}.  (x  <  m  \mwedge{}  q  <  m)  BY
                                        (Decide  \mkleeneopen{}x  \mleq{}  q\mkleeneclose{}\mcdot{}
                                          THEN  Auto
                                          THEN  Try  ((With  \mkleeneopen{}q  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Complete  (Auto)))
                                          THEN  Try  ((With  \mkleeneopen{}x  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Complete  (Auto)))))
                THEN  D  -1
                THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto))




Home Index