Nuprl Rule : lessEquality
H ⊢ if (a1) < (b1) then s1 else t1 = if (a2) < (b2) then s2 else t2 ∈ T
BY lessEquality 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 :
less: if (a) < (b) then c else d,
int: ℤ,
function: x:A ⟶ B[x],
less_than: a < b,
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 lessEquality 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:
2017_09_29-PM-05_44_49
Last ObjectModification:
2015_11_25-PM-03_37_45
Theory : rules
Home
Index