Nuprl Rule : int_eqEquality
H ⊢ if a1=b1 then s1 else t1 = if a2=b2 then s2 else t2 ∈ T
BY int_eqEquality v
H ⊢ a1 = a2 ∈ ℤ
H ⊢ b1 = b2 ∈ ℤ
H v:(a1 = b1 ∈ ℤ) ⊢ s1 = s2 ∈ T
H v:((a1 = b1 ∈ ℤ) ⟶ Void) ⊢ t1 = t2 ∈ T
Definitions occuring in rule :
int_eq: if a=b then c else d,
function: x:A ⟶ B[x],
int: ℤ,
void: Void,
equal: s = t ∈ T,
axiom: Ax
Latex:
H \mvdash{} if a1=b1 then s1 else t1 = if a2=b2 then s2 else t2
BY int\_eqEquality v
H \mvdash{} a1 = a2
H \mvdash{} b1 = b2
H v:(a1 = b1) \mvdash{} s1 = s2
H v:((a1 = b1) {}\mrightarrow{} Void) \mvdash{} t1 = t2
Date html generated:
2019_06_20-PM-04_11_50
Last ObjectModification:
2015_11_25-PM-03_37_42
Theory : rules
Home
Index