---

Step * of Lemma bag-maximals-not-max

∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].
  (¬↑(R x y)) supposing 
     (y ↓∈ bag-maximals(b;R) and 
     x ↓∈ bag-maximals(b;R) and 
     (∀x,y:T.  ((↑(R x y)) ⇒ (↑(R y x)) ⇒ (x = y ∈ T))) and 
     (∀x:T. (¬↑(R x x))))
BY
{ ((UnivCD THENA Auto)
   THEN (D 0 THENA Auto)
   THEN BagMemberD (-2)
   THEN BagMemberD (-3)
   THEN RepD
   THEN (BagToList 2 THENA Auto)
   THEN Unfold `bag-member` (-5)
   THEN SquashExRepD
   THEN (RevHypSubst' (-6) (-2) THENA Auto)
   THEN (RevHypSubst' (-6) (-3) THENA Auto)
   THEN (RevHypSubst' (-6) (-4) THENA Auto)
   THEN ThinVar `b'
   THEN (FLemma `l_member_decomp` [-5] THENA Auto)
   THEN ExRepD
   THEN (RepUR ``bag-maximal? bag-accum`` (-5)
         THEN (HypSubst' (-1) (-5) THENA Auto)⋅
         THEN (RWW "list_accum_append list_accum_cons" (-1) THENA Auto)
         THEN Reduce (-1)
         THEN (Decide ↑R[y;x] THENA Auto))⋅) }

1
1. T : Type
2. R : T ⟶ T ⟶ 𝔹
3. x : T
4. y : T
5. ∀x:T. (¬↑(R x x))
6. ∀x,y:T.  ((↑(R x y)) ⇒ (↑(R y x)) ⇒ (x = y ∈ T))
7. L : T List
8. (x ∈ L)
9. ↑bag-maximal?(L;x;R)
10. y ↓∈ L
11. ↑(R x y)
12. l1 : T List
13. l2 : T List
14. L = (l1 @ [x] @ l2) ∈ (T List)
15. ↑accumulate (with value b and list item y@0):
      b ∧b R[y;y@0]
     over list:
       l2
     with starting value:
      accumulate (with value b and list item y@0): b ∧b R[y;y@0]over list:  l1with starting value: tt) ∧b R[y;x])
16. ↑R[y;x]
⊢ False

2
1. T : Type
2. R : T ⟶ T ⟶ 𝔹
3. x : T
4. y : T
5. ∀x:T. (¬↑(R x x))
6. ∀x,y:T.  ((↑(R x y)) ⇒ (↑(R y x)) ⇒ (x = y ∈ T))
7. L : T List
8. (x ∈ L)
9. ↑bag-maximal?(L;x;R)
10. y ↓∈ L
11. ↑(R x y)
12. l1 : T List
13. l2 : T List
14. L = (l1 @ [x] @ l2) ∈ (T List)
15. ↑accumulate (with value b and list item y@0):
      b ∧b R[y;y@0]
     over list:
       l2
     with starting value:
      accumulate (with value b and list item y@0): b ∧b R[y;y@0]over list:  l1with starting value: tt) ∧b R[y;x])
16. ¬↑R[y;x]
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x,y:T].
    (\mneg{}\muparrow{}(R  x  y))  supposing 
          (y  \mdownarrow{}\mmember{}  bag-maximals(b;R)  and 
          x  \mdownarrow{}\mmember{}  bag-maximals(b;R)  and 
          (\mforall{}x,y:T.    ((\muparrow{}(R  x  y))  {}\mRightarrow{}  (\muparrow{}(R  y  x))  {}\mRightarrow{}  (x  =  y)))  and 
          (\mforall{}x:T.  (\mneg{}\muparrow{}(R  x  x))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  BagMemberD  (-2)
  THEN  BagMemberD  (-3)
  THEN  RepD
  THEN  (BagToList  2  THENA  Auto)
  THEN  Unfold  `bag-member`  (-5)
  THEN  SquashExRepD
  THEN  (RevHypSubst'  (-6)  (-2)  THENA  Auto)
  THEN  (RevHypSubst'  (-6)  (-3)  THENA  Auto)
  THEN  (RevHypSubst'  (-6)  (-4)  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  (FLemma  `l\_member\_decomp`  [-5]  THENA  Auto)
  THEN  ExRepD
  THEN  (RepUR  ``bag-maximal?  bag-accum``  (-5)
              THEN  (HypSubst'  (-1)  (-5)  THENA  Auto)\mcdot{}
              THEN  (RWW  "list\_accum\_append  list\_accum\_cons"  (-1)  THENA  Auto)
              THEN  Reduce  (-1)
              THEN  (Decide  \muparrow{}R[y;x]  THENA  Auto))\mcdot{})

---

Home Index