Step
*
1
2
1
of Lemma
qless-witness
.....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
BY
{ (RW (AddrC [1] (TagC (mk_tag_term 3))) 0 THEN Auto) }
Latex:
Latex:
.....equality.....
1. a : \mBbbQ{}
2. b : \mBbbQ{}
3. a < b
4. TERMOF\{decidable\_\_qless:o, 1:l\} a b \mmember{} Dec(a < b)
\mvdash{} TERMOF\{decidable\_\_qless:o, 1:l\} a b \msim{} if qpositive(b - a) then tt else inr (\mlambda{}x.\mcdot{}) fi
By
Latex:
(RW (AddrC [1] (TagC (mk\_tag\_term 3))) 0 THEN Auto)
Home
Index