Nuprl Rule : lessTransitive

H  ⊢ if (a) < (c)  then True  else False

  BY lessTransitive b
  
  H  ⊢ if (a) < (b)  then True  else False
  H  ⊢ if (b) < (c)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ
  H  ⊢ c ∈ ℤ



Definitions occuring in rule :  less: if (a) < (b)  then c  else d true: True false: False member: t ∈ T int: axiom: Ax

Latex:
H    \mvdash{}  if  (a)  <  (c)    then  True    else  False

    BY  lessTransitive  b
   
    H    \mvdash{}  if  (a)  <  (b)    then  True    else  False
    H    \mvdash{}  if  (b)  <  (c)    then  True    else  False
    H    \mvdash{}  a  \mmember{}  \mBbbZ{}
    H    \mvdash{}  b  \mmember{}  \mBbbZ{}
    H    \mvdash{}  c  \mmember{}  \mBbbZ{}



Date html generated: 2019_06_20-PM-04_12_24
Last ObjectModification: 2018_09_10-AM-11_39_16

Theory : rules


Home Index