---

Step * 2 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
{ ((Assert ⌜R[y;x] = ff⌝⋅ THENA Auto)
   THEN (HypSubst' (-1) (-3) THENA Auto)
   THEN (RWO "band-bfalse" (-3) THENA Auto)
   THEN (InstLemma `list_accum_invariant` [⌜T⌝;⌜𝔹⌝;⌜λb,z. (b ∧b R[y;z])⌝;⌜λz.(¬↑z)⌝;⌜l2⌝;⌜ff⌝]⋅ THENA Auto)
   THEN All (RepUR ``so_apply``)⋅
   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.  \mneg{}\muparrow{}R[y;x]
\mvdash{}  False


By

---

Latex:
((Assert  \mkleeneopen{}R[y;x]  =  ff\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
  THEN  (RWO  "band-bfalse"  (-3)  THENA  Auto)
  THEN  (InstLemma  `list\_accum\_invariant`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}b,z.  (b  \mwedge{}\msubb{}  R[y;z])\mkleeneclose{};\mkleeneopen{}\mlambda{}z.(\mneg{}\muparrow{}z)\mkleeneclose{};\mkleeneopen{}l2\mkleeneclose{};\mkleeneopen{}ff\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  All  (RepUR  ``so\_apply``)\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index