Nuprl Rule : lessTrichotomy

H  ⊢ a = b ∈ ℤ

  BY lessTrichotomy ()

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

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

Latex:
H \mvdash{} a = b BY lessTrichotomy () H \mvdash{} if (a) < (b) then False else True H \mvdash{} if (b) < (a) then False else True H \mvdash{} a \mmember{} \mBbbZ{} H \mvdash{} b \mmember{} \mBbbZ{} Date html generated: 2019_06_20-PM-04_12_29 Last ObjectModification: 2018_09_10-PM-03_21_35 Theory : rules Home Index