---

Step * of Lemma extend-seq1-all-dec

No Annotations
∀n,n0:finite-nat-seq(). ∀beta:ℕ ⟶ ℕ.
  Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);n)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);n)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))) ∈ ℙ BY
               Auto)
   THEN D 2
   THEN D 1
   THEN RenameVar `n' (-6)
   THEN RenameVar `s' (-5)
   THEN RenameVar `m' (-4)
   THEN RenameVar `r' (-3)
   THEN (Decide ⌜(m + 1) ≤ n⌝⋅ THENA Auto)) }

1
1. n : ℕ
2. s : ℕn ⟶ ℕ
3. m : ℕ
4. r : ℕm ⟶ ℕ
5. beta : ℕ ⟶ ℕ
6. ∃x:ℕ. ((↑init-seg-nat-seq(<m, r>**λi.x^(1);<n, s>)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))) ∈ ℙ
7. (m + 1) ≤ n
⊢ Dec(∃x:ℕ. ((↑init-seg-nat-seq(<m, r>**λi.x^(1);<n, s>)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))

2
1. n : ℕ
2. s : ℕn ⟶ ℕ
3. m : ℕ
4. r : ℕm ⟶ ℕ
5. beta : ℕ ⟶ ℕ
6. ∃x:ℕ. ((↑init-seg-nat-seq(<m, r>**λi.x^(1);<n, s>)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))) ∈ ℙ
7. ¬((m + 1) ≤ n)
⊢ Dec(∃x:ℕ. ((↑init-seg-nat-seq(<m, r>**λi.x^(1);<n, s>)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}n,n0:finite-nat-seq().  \mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
    Dec(\mexists{}x:\mBbbN{}.  ((\muparrow{}init-seg-nat-seq(n0**\mlambda{}i.x\^{}(1);n))  \mwedge{}  (\mneg{}((beta  x)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x.  ((beta  y)  =  0))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mexists{}x:\mBbbN{}
                              ((\muparrow{}init-seg-nat-seq(n0**\mlambda{}i.x\^{}(1);n))  \mwedge{}  (\mneg{}((beta  x)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x.  ((beta  y)  =  0)))
                            \mmember{}  \mBbbP{}  BY
                          Auto)
  THEN  D  2
  THEN  D  1
  THEN  RenameVar  `n'  (-6)
  THEN  RenameVar  `s'  (-5)
  THEN  RenameVar  `m'  (-4)
  THEN  RenameVar  `r'  (-3)
  THEN  (Decide  \mkleeneopen{}(m  +  1)  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index