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