---

Step * 1 1 1 of Lemma divides_instance


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
BY
{ xxx(MemCD THEN Try (Fold `or` 0) THEN Auto)xxx }

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(MemCD  THEN  Try  (Fold  `or`  0)  THEN  Auto)xxx

---

Home Index