Step
*
of Lemma
decidable__equal-int_seg
∀[a,b:ℤ]. ∀x,y:{a..b-}. Dec(x = y ∈ {a..b-})
BY
{ (Auto THEN Decide ⌜x = y ∈ ℤ⌝⋅ THEN Auto) }
1
.....decidable?.....
1. [a] : ℤ
2. [b] : ℤ
3. x : {a..b-}
4. y : {a..b-}
5. x = y ∈ ℤ
⊢ Dec(x = y ∈ {a..b-})
2
.....decidable?.....
1. [a] : ℤ
2. [b] : ℤ
3. x : {a..b-}
4. y : {a..b-}
5. ¬(x = y ∈ ℤ)
⊢ Dec(x = y ∈ {a..b-})
Latex:
Latex:
\mforall{}[a,b:\mBbbZ{}]. \mforall{}x,y:\{a..b\msupminus{}\}. Dec(x = y)
By
Latex:
(Auto THEN Decide \mkleeneopen{}x = y\mkleeneclose{}\mcdot{} THEN Auto)
Home
Index