Step
*
1
2
of Lemma
qless-witness
1. a : ℚ
2. b : ℚ
3. a < b
4. TERMOF{decidable__qless:o, 1:l} a b ∈ Dec(a < b)
⊢ ⋅ ∈ a < b
BY
{ Subst ⌜TERMOF{decidable__qless:o, 1:l} a b ~ if qpositive(b - a) then tt else inr (λx.⋅)  fi ⌝ (-1)⋅ }
1
.....equality..... 
1. a : ℚ
2. b : ℚ
3. a < b
4. TERMOF{decidable__qless:o, 1:l} a b ∈ Dec(a < b)
⊢ TERMOF{decidable__qless:o, 1:l} a b ~ if qpositive(b - a) then tt else inr (λx.⋅)  fi 
2
1. a : ℚ
2. b : ℚ
3. a < b
4. if qpositive(b - a) then tt else inr (λx.⋅)  fi  ∈ Dec(a < b)
⊢ ⋅ ∈ a < b
Latex:
Latex:
1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  a  <  b
4.  TERMOF\{decidable\_\_qless:o,  1:l\}  a  b  \mmember{}  Dec(a  <  b)
\mvdash{}  \mcdot{}  \mmember{}  a  <  b
By
Latex:
Subst  \mkleeneopen{}TERMOF\{decidable\_\_qless:o,  1:l\}  a  b  \msim{}  if  qpositive(b  -  a)  then  tt  else  inr  (\mlambda{}x.\mcdot{})    fi  \mkleeneclose{}  (-1)\mcdot{}
Home
Index