---

Step * of Lemma fset-max_property

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f:T ⟶ ℕ]. ∀[s:fset(T)].
  ((∀[x:T]. (f x) ≤ fset-max(f;s) supposing x ∈ s)
  ∧ (¬((∀x:T. (x ∈ s ⇒ f x < fset-max(f;s))) ∧ (¬(s = {} ∈ fset(T))))))
BY
{ (UniformUnivCD Auto
   THEN InstLemma `decidable-equal-deq` [⌜T⌝]⋅
   THEN Auto
   THEN ((DNot 0 THENA Auto) ORELSE SupposeNot)
   THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅
   THEN Auto
   THEN Dquotient2 4⋅
   THEN Auto
   THEN All (Unfolds ``fset-member fset-max fset-null``)⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ ℕ
4. T List ∈ Type
5. ∀x1,y:T List.  (set-equal(T;x1;y) ∈ Type)
6. ∀x1:T List. set-equal(T;x1;x1)
7. a : Base
8. b : Base
9. c : a = b ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
10. a ∈ T List
11. b ∈ T List
12. set-equal(T;a;b)
13. ∀x,y:T.  Dec(x = y ∈ T)
14. x : T
15. ↑x ∈b a
16. ¬((f x) ≤ imax-list([0 / map(f;a)]))
⊢ 0 = 1 ∈ ℤ

2
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ ℕ
4. T List ∈ Type
5. ∀x,y:T List.  (set-equal(T;x;y) ∈ Type)
6. ∀x:T List. set-equal(T;x;x)
7. a : Base
8. b : Base
9. c : a = b ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
10. a ∈ T List
11. b ∈ T List
12. set-equal(T;a;b)
13. ∀x,y:T.  Dec(x = y ∈ T)
14. ∀[x:T]. (f x) ≤ imax-list([0 / map(f;a)]) supposing ↑x ∈b a
15. ∀x:T. ((↑x ∈b a) ⇒ f x < imax-list([0 / map(f;a)]))
16. ¬(a = {} ∈ fset(T))
⊢ 0 = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[s:fset(T)].
    ((\mforall{}[x:T].  (f  x)  \mleq{}  fset-max(f;s)  supposing  x  \mmember{}  s)
    \mwedge{}  (\mneg{}((\mforall{}x:T.  (x  \mmember{}  s  {}\mRightarrow{}  f  x  <  fset-max(f;s)))  \mwedge{}  (\mneg{}(s  =  \{\})))))


By

---

Latex:
(UniformUnivCD  Auto
  THEN  InstLemma  `decidable-equal-deq`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ((DNot  0  THENA  Auto)  ORELSE  SupposeNot)
  THEN  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Dquotient2  4\mcdot{}
  THEN  Auto
  THEN  All  (Unfolds  ``fset-member  fset-max  fset-null``)\mcdot{})

---

Home Index