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 ∈ ℤ
  v:(a1 b1 ∈ ℤ) ⊢ s1 s2 ∈ T
  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: 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: 2016_12_14-AM-08_53_31
Last ObjectModification: 2015_11_25-PM-03_37_42

Theory : rules


Home Index