Nuprl Rule : intWeakElimination
H x:ℤ, J ⊢ a = b ∈ T
BY intWeakElimination #$i z y v
H x:ℤ, J, y:ℤ, v:y < 0, z:a = b ∈ T[y + 1/x] ⊢ a = b ∈ T[y/x]
H x:ℤ, J ⊢ a = b ∈ T[0/x]
H x:ℤ, J, y:ℤ, v:0 < y, z:a = b ∈ T[y - 1/x] ⊢ a = b ∈ T[y/x]
Definitions occuring in rule :
add: n + m,
int: ℤ,
less_than: a < b,
subtract: n - m,
natural_number: $n,
equal: s = t ∈ T,
axiom: Ax
Latex:
H x:\mBbbZ{}, J \mvdash{} a = b
BY intWeakElimination \#\$i z y v
H x:\mBbbZ{}, J, y:\mBbbZ{}, v:y < 0, z:a = b[y + 1/x] \mvdash{} a = b[y/x]
H x:\mBbbZ{}, J \mvdash{} a = b[0/x]
H x:\mBbbZ{}, J, y:\mBbbZ{}, v:0 < y, z:a = b[y - 1/x] \mvdash{} a = b[y/x]
Date html generated:
2019_06_20-PM-04_11_50
Last ObjectModification:
2015_11_25-PM-03_37_42
Theory : rules
Home
Index