---

Step * 1 of Lemma bag-maximals-not-max


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
BY
{ (Unfold `so_apply` (-1)
   THEN (InstHyp [⌜x⌝;⌜y⌝] 6⋅ THENA Auto)
   THEN (HypSubst' (-1) (-2) THENA Auto)
   THEN InstHyp [⌜y⌝] 5⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  y  :  T
5.  \mforall{}x:T.  (\mneg{}\muparrow{}(R  x  x))
6.  \mforall{}x,y:T.    ((\muparrow{}(R  x  y))  {}\mRightarrow{}  (\muparrow{}(R  y  x))  {}\mRightarrow{}  (x  =  y))
7.  L  :  T  List
8.  (x  \mmember{}  L)
9.  \muparrow{}bag-maximal?(L;x;R)
10.  y  \mdownarrow{}\mmember{}  L
11.  \muparrow{}(R  x  y)
12.  l1  :  T  List
13.  l2  :  T  List
14.  L  =  (l1  @  [x]  @  l2)
15.  \muparrow{}accumulate  (with  value  b  and  list  item  y@0):
            b  \mwedge{}\msubb{}  R[y;y@0]
          over  list:
              l2
          with  starting  value:
            accumulate  (with  value  b  and  list  item  y@0):
              b  \mwedge{}\msubb{}  R[y;y@0]
            over  list:
                l1
            with  starting  value:
              tt)
            \mwedge{}\msubb{}  R[y;x])
16.  \muparrow{}R[y;x]
\mvdash{}  False


By

---

Latex:
(Unfold  `so\_apply`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-2)  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  5\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index