Step
*
1
1
1
of Lemma
extend-seq1-all-dec
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
8. ↑init-seg-nat-seq(r^(m);s^(n))
9. (beta (s m)) = 0 ∈ ℤ
⊢ Dec(∃x:ℕ. ((↑init-seg-nat-seq(<m, r>**λi.x^(1);<n, s>)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
BY
{ ((OrRight THENA Auto) THEN (D 0 THENA Auto) THEN ExRepD) }
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
8. ↑init-seg-nat-seq(r^(m);s^(n))
9. (beta (s m)) = 0 ∈ ℤ
10. x : ℕ
11. ↑init-seg-nat-seq(<m, r>**λi.x^(1);<n, s>)
12. ¬((beta x) = 0 ∈ ℤ)
13. ∀y:ℕx. ((beta y) = 0 ∈ ℤ)
⊢ False
Latex:
Latex:
1. n : \mBbbN{}
2. s : \mBbbN{}n {}\mrightarrow{} \mBbbN{}
3. m : \mBbbN{}
4. r : \mBbbN{}m {}\mrightarrow{} \mBbbN{}
5. beta : \mBbbN{} {}\mrightarrow{} \mBbbN{}
6. \mexists{}x:\mBbbN{}. ((\muparrow{}init-seg-nat-seq(<m, r>**\mlambda{}i.x\^{}(1);<n, s>)) \mwedge{} (\mneg{}((beta x) = 0)) \mwedge{} (\mforall{}y:\mBbbN{}x. ((beta y) = 0))\000C) \mmember{} \mBbbP{}
7. (m + 1) \mleq{} n
8. \muparrow{}init-seg-nat-seq(r\^{}(m);s\^{}(n))
9. (beta (s m)) = 0
\mvdash{} Dec(\mexists{}x:\mBbbN{}. ((\muparrow{}init-seg-nat-seq(<m, r>**\mlambda{}i.x\^{}(1);<n, s>)) \mwedge{} (\mneg{}((beta x) = 0)) \mwedge{} (\mforall{}y:\mBbbN{}x. ((beta y) = \000C0))))
By
Latex:
((OrRight THENA Auto) THEN (D 0 THENA Auto) THEN ExRepD)
Home
Index