Step
*
2
2
2
2
1
of Lemma
gamma-neighbourhood-prop1
.....assertion.....
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. ∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x)))
4. a : finite-nat-seq()
5. ¬↑init-seg-nat-seq(a;n0)
6. b : finite-nat-seq()
7. ¬↑init-seg-nat-seq(a**b;n0)
8. y : ¬(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
9. (TERMOF{extend-seq1-all-dec:o, 1:l} a n0 beta)
= (inr y )
∈ Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
10. x1 : ℕ
11. x3 : ↑init-seg-nat-seq(n0**λi.x1^(1);a**b)
12. x5 : ¬((beta x1) = 0 ∈ ℤ)
13. x6 : ∀y:ℕx1. ((beta y) = 0 ∈ ℤ)
14. (TERMOF{extend-seq1-all-dec:o, 1:l} a**b n0 beta)
= (inl <x1, x3, x5, x6>)
∈ Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a**b)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
⊢ ∀x:ℕ. ((¬↑init-seg-nat-seq(n0**λi.x^(1);a)) ∨ ((beta x) = 0 ∈ ℤ) ∨ (∃y:ℕx. (¬((beta y) = 0 ∈ ℤ))))
BY
{ ((D 0 THENA Auto) THEN (BoolCase ⌜init-seg-nat-seq(n0**λi.x^(1);a)⌝⋅ THENA Auto)) }
1
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. ∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x)))
4. a : finite-nat-seq()
5. ¬↑init-seg-nat-seq(a;n0)
6. b : finite-nat-seq()
7. ¬↑init-seg-nat-seq(a**b;n0)
8. y : ¬(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
9. (TERMOF{extend-seq1-all-dec:o, 1:l} a n0 beta)
= (inr y )
∈ Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
10. x1 : ℕ
11. x3 : ↑init-seg-nat-seq(n0**λi.x1^(1);a**b)
12. x5 : ¬((beta x1) = 0 ∈ ℤ)
13. x6 : ∀y:ℕx1. ((beta y) = 0 ∈ ℤ)
14. (TERMOF{extend-seq1-all-dec:o, 1:l} a**b n0 beta)
= (inl <x1, x3, x5, x6>)
∈ Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a**b)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
15. x : ℕ
16. ↑init-seg-nat-seq(n0**λi.x^(1);a)
⊢ (¬True) ∨ ((beta x) = 0 ∈ ℤ) ∨ (∃y:ℕx. (¬((beta y) = 0 ∈ ℤ)))
2
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. ∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x)))
4. a : finite-nat-seq()
5. ¬↑init-seg-nat-seq(a;n0)
6. b : finite-nat-seq()
7. ¬↑init-seg-nat-seq(a**b;n0)
8. y : ¬(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
9. (TERMOF{extend-seq1-all-dec:o, 1:l} a n0 beta)
= (inr y )
∈ Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
10. x1 : ℕ
11. x3 : ↑init-seg-nat-seq(n0**λi.x1^(1);a**b)
12. x5 : ¬((beta x1) = 0 ∈ ℤ)
13. x6 : ∀y:ℕx1. ((beta y) = 0 ∈ ℤ)
14. (TERMOF{extend-seq1-all-dec:o, 1:l} a**b n0 beta)
= (inl <x1, x3, x5, x6>)
∈ Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);a**b)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
15. x : ℕ
16. ¬↑init-seg-nat-seq(n0**λi.x^(1);a)
⊢ (¬False) ∨ ((beta x) = 0 ∈ ℤ) ∨ (∃y:ℕx. (¬((beta y) = 0 ∈ ℤ)))
Latex:
Latex:
.....assertion.....
1. beta : \mBbbN{} {}\mrightarrow{} \mBbbN{}
2. n0 : finite-nat-seq()
3. \mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mexists{}x:\mBbbN{}. (\muparrow{}isl(gamma-neighbourhood(beta;n0) a\^{}(x)))
4. a : finite-nat-seq()
5. \mneg{}\muparrow{}init-seg-nat-seq(a;n0)
6. b : finite-nat-seq()
7. \mneg{}\muparrow{}init-seg-nat-seq(a**b;n0)
8. y : \mneg{}(\mexists{}x:\mBbbN{}. ((\muparrow{}init-seg-nat-seq(n0**\mlambda{}i.x\^{}(1);a)) \mwedge{} (\mneg{}((beta x) = 0)) \mwedge{} (\mforall{}y:\mBbbN{}x. ((beta y) = 0))))
9. (TERMOF\{extend-seq1-all-dec:o, 1:l\} a n0 beta) = (inr y )
10. x1 : \mBbbN{}
11. x3 : \muparrow{}init-seg-nat-seq(n0**\mlambda{}i.x1\^{}(1);a**b)
12. x5 : \mneg{}((beta x1) = 0)
13. x6 : \mforall{}y:\mBbbN{}x1. ((beta y) = 0)
14. (TERMOF\{extend-seq1-all-dec:o, 1:l\} a**b n0 beta) = (inl <x1, x3, x5, x6>)
\mvdash{} \mforall{}x:\mBbbN{}. ((\mneg{}\muparrow{}init-seg-nat-seq(n0**\mlambda{}i.x\^{}(1);a)) \mvee{} ((beta x) = 0) \mvee{} (\mexists{}y:\mBbbN{}x. (\mneg{}((beta y) = 0))))
By
Latex:
((D 0 THENA Auto) THEN (BoolCase \mkleeneopen{}init-seg-nat-seq(n0**\mlambda{}i.x\^{}(1);a)\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index