---

Step * of Lemma member-functions-list

∀n,b:ℕ. ∀f:ℕn ⟶ ℕb.  (f ∈ functions-list(n;b))
BY
{ (Auto
   THEN (GenConclTerm ⌜functions-list(n;b)⌝⋅ THENA Auto)
   THEN (InstLemma `decidable__l_member` [⌜ℕn ⟶ ℕb⌝;⌜f⌝;⌜v⌝]⋅ THEN Auto)
   THEN D -1
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto) }

1
.....assertion..... 
1. n : ℕ
2. b : ℕ
3. f : ℕn ⟶ ℕb
4. v : {P:(ℕn ⟶ ℕb) List| no_repeats(ℕn ⟶ ℕb;P) ∧ (∀f:ℕn ⟶ ℕb. (f ∈ P))} 
5. functions-list(n;b) = v ∈ {P:(ℕn ⟶ ℕb) List| no_repeats(ℕn ⟶ ℕb;P) ∧ (∀f:ℕn ⟶ ℕb. (f ∈ P))} 
6. ¬(f ∈ v)
⊢ False

---

Latex:

---

Latex:
\mforall{}n,b:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}b.    (f  \mmember{}  functions-list(n;b))


By

---

Latex:
(Auto
  THEN  (GenConclTerm  \mkleeneopen{}functions-list(n;b)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `decidable\_\_l\_member`  [\mkleeneopen{}\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index