Nuprl Rule : atomn_eqEquality
H ⊢ if a1=$n b1 then s1 else t1 = if a2=$n b2 then s2 else t2 ∈ T
BY atomn_eqEquality v
H ⊢ a1 = a2 ∈ Atom$n
H ⊢ b1 = b2 ∈ Atom$n
H v:(a1 = b1 ∈ Atom$n) ⊢ s1 = s2 ∈ T
H v:((a1 = b1 ∈ Atom$n) ⟶ Void) ⊢ t1 = t2 ∈ T
Definitions occuring in rule :
atom_eq: atomeqn def,
function: x:A ⟶ B[x],
atom: Atom$n,
void: Void,
equal: s = t ∈ T,
axiom: Ax
Latex:
H \mvdash{} if a1=\$n b1 then s1 else t1 = if a2=\$n b2 then s2 else t2
BY atomn\_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_12_29
Last ObjectModification:
2015_11_25-PM-03_55_42
Theory : rules
Home
Index