---

Step * 1 1 of Lemma divides_instance


1. TERMOF{decidable__divides_ext:o, \\v:l} 3 6 ∈ (3 | 6) ∨ (¬(3 | 6))
⊢ 3 | 6
BY
{ % Hyp 1 helps type inference along here %
UseWitness ⌜outl(TERMOF{decidable__divides_ext:o, \\v:l} 3 6)⌝ }

1
1. TERMOF{decidable__divides_ext:o, \\v:l} 3 6 ∈ (3 | 6) ∨ (¬(3 | 6))
⊢ outl(TERMOF{decidable__divides_ext:o, \\v:l} 3 6) ∈ 3 | 6

---

Latex:

---

Latex:

1.  TERMOF\{decidable\_\_divides\_ext:o,  \mbackslash{}\mbackslash{}v:l\}  3  6  \mmember{}  (3  |  6)  \mvee{}  (\mneg{}(3  |  6))
\mvdash{}  3  |  6


By

---

Latex:
\%  Hyp  1  helps  type  inference  along  here  \%
UseWitness  \mkleeneopen{}outl(TERMOF\{decidable\_\_divides\_ext:o,  \mbackslash{}\mbackslash{}v:l\}  3  6)\mkleeneclose{}

---

Home Index