---

Step * of Lemma bag-maximal?-append

∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[b1,b2:bag(T)]. ∀[x:T].
  uiff(↑bag-maximal?(b1 + b2;x;R);(↑bag-maximal?(b1;x;R)) ∧ (↑bag-maximal?(b2;x;R)))
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList (-3) THENA Auto)
   THEN (BagToList (-2) THENA Auto)
   THEN (RepUR ``bag-maximal? bag-accum bag-append`` 0
         THEN (RWO "list_accum_append" 0 THENA Auto)
         THEN (Assert ⌜Dec(↑accumulate (with value b and list item y):
                             b ∧b R[x;y]
                            over list:
                              b1
                            with starting value:
                             tt))⌝⋅
               THENA Auto
               )
         THEN D (-1)
         THEN Try (Complete (((Assert ⌜accumulate (with value b and list item y):
                                        b ∧b R[x;y]
                                       over list:
                                         b1
                                       with starting value:
                                        tt) 
                                       = tt⌝⋅
                               THENA Auto
                               )
                              THEN HypSubst' (-1) 0
                              THEN Auto)))
         THEN (Assert 
               ⌜accumulate (with value b and list item y): b ∧b R[x;y]over list:  b1with starting value: tt) = ff⌝⋅
               THENA Auto
               )
         THEN HypSubst' (-1) 0
         THEN Reduce 0
         THEN (InstLemma `list_accum_invariant` [⌜T⌝;⌜𝔹⌝;⌜λb,y. (b ∧b R[x;y])⌝;⌜λz.(¬↑z)⌝;⌜b2⌝;⌜ff⌝]⋅ THENA Auto)
         THEN All (RepUR ``so_apply``)
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b1,b2:bag(T)].  \mforall{}[x:T].
    uiff(\muparrow{}bag-maximal?(b1  +  b2;x;R);(\muparrow{}bag-maximal?(b1;x;R))  \mwedge{}  (\muparrow{}bag-maximal?(b2;x;R)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagToList  (-3)  THENA  Auto)
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  (RepUR  ``bag-maximal?  bag-accum  bag-append``  0
              THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
              THEN  (Assert  \mkleeneopen{}Dec(\muparrow{}accumulate  (with  value  b  and  list  item  y):
                                                      b  \mwedge{}\msubb{}  R[x;y]
                                                    over  list:
                                                        b1
                                                    with  starting  value:
                                                      tt))\mkleeneclose{}\mcdot{}
                          THENA  Auto
                          )
              THEN  D  (-1)
              THEN  Try  (Complete  (((Assert  \mkleeneopen{}accumulate  (with  value  b  and  list  item  y):
                                                                            b  \mwedge{}\msubb{}  R[x;y]
                                                                          over  list:
                                                                              b1
                                                                          with  starting  value:
                                                                            tt) 
                                                                          =  tt\mkleeneclose{}\mcdot{}
                                                          THENA  Auto
                                                          )
                                                        THEN  HypSubst'  (-1)  0
                                                        THEN  Auto)))
              THEN  (Assert  \mkleeneopen{}accumulate  (with  value  b  and  list  item  y):
                                            b  \mwedge{}\msubb{}  R[x;y]
                                          over  list:
                                              b1
                                          with  starting  value:
                                            tt) 
                                          =  ff\mkleeneclose{}\mcdot{}
                          THENA  Auto
                          )
              THEN  HypSubst'  (-1)  0
              THEN  Reduce  0
              THEN  (InstLemma  `list\_accum\_invariant`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}b,y.  (b  \mwedge{}\msubb{}  R[x;y])\mkleeneclose{};\mkleeneopen{}\mlambda{}z.(\mneg{}\muparrow{}z)\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}ff\mkleeneclose{}]\mcdot{}
                          THENA  Auto
                          )
              THEN  All  (RepUR  ``so\_apply``)
              THEN  Auto)\mcdot{})

---

Home Index