---

Step * 1 1 2 2 2 2 1 of Lemma max-fst-property

.....equality..... 
1. Info : Type
2. A : Type
3. es : EO+(Info)@i'
4. X : EClass(ℤ × A)@i'
5. e : E@i
6. ↑e ∈b MaxFst(X)@i
7. fst(accum_list(p1,e.if fst(p1) <z fst(X(e)) then X(e) else p1 fi ;e.X(e);≤(X)(e))) 
~ imax-list(map(λe.(fst(X(e)));≤(X)(e)))
8. ∀L:E(X) List. ∀e:E(X).
     ∃e':E(X)
      (((e' ∈ L) ∨ (e' = e ∈ E(X)))
      ∧ (accumulate (with value p1 and list item e):
          if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
         over list:
           L
         with starting value:
          X(e))
        = X(e')
        ∈ (ℤ × A)))
9. u : E(X)
10. v : E(X) List
11. ≤(X)(e) = [u / v] ∈ (E(X) List)@i
12. e' : E(X)
13. (e' ∈ v) ∨ (e' = u ∈ E(X))
14. accumulate (with value p1 and list item e):
     if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
    over list:
      v
    with starting value:
     X(u))
= X(e')
∈ (ℤ × A)
15. e' ≤loc e 
16. accumulate (with value p1 and list item e):
     if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
    over list:
      v
    with starting value:
     X(u))
= X(e')
∈ (ℤ × A)
17. e'@0 : E(X)@i
18. e'@0 ≤loc e @i
⊢ fst(X(e')) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e)))
BY
{ \p. let x, y = dest_sqequal (concl p) in
         (Assert (mk_equal_term ⌈ℤ⌉ x y)
         THENL [Id; HypSubst' (-1) 0 THEN Trivial] ) p⋅ }

1
.....assertion..... 
1. Info : Type
2. A : Type
3. es : EO+(Info)@i'
4. X : EClass(ℤ × A)@i'
5. e : E@i
6. ↑e ∈b MaxFst(X)@i
7. fst(accum_list(p1,e.if fst(p1) <z fst(X(e)) then X(e) else p1 fi ;e.X(e);≤(X)(e))) 
~ imax-list(map(λe.(fst(X(e)));≤(X)(e)))
8. ∀L:E(X) List. ∀e:E(X).
     ∃e':E(X)
      (((e' ∈ L) ∨ (e' = e ∈ E(X)))
      ∧ (accumulate (with value p1 and list item e):
          if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
         over list:
           L
         with starting value:
          X(e))
        = X(e')
        ∈ (ℤ × A)))
9. u : E(X)
10. v : E(X) List
11. ≤(X)(e) = [u / v] ∈ (E(X) List)@i
12. e' : E(X)
13. (e' ∈ v) ∨ (e' = u ∈ E(X))
14. accumulate (with value p1 and list item e):
     if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
    over list:
      v
    with starting value:
     X(u))
= X(e')
∈ (ℤ × A)
15. e' ≤loc e 
16. accumulate (with value p1 and list item e):
     if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
    over list:
      v
    with starting value:
     X(u))
= X(e')
∈ (ℤ × A)
17. e'@0 : E(X)@i
18. e'@0 ≤loc e @i
⊢ (fst(X(e'))) = imax-list(map(λe.(fst(X(e)));≤(X)(e))) ∈ ℤ

---

Latex:

---

Latex:
.....equality..... 
1.  Info  :  Type
2.  A  :  Type
3.  es  :  EO+(Info)@i'
4.  X  :  EClass(\mBbbZ{}  \mtimes{}  A)@i'
5.  e  :  E@i
6.  \muparrow{}e  \mmember{}\msubb{}  MaxFst(X)@i
7.  fst(accum\_list(p1,e.if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi  ;e.X(e);\mleq{}(X)(e))) 
\msim{}  imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e)))
8.  \mforall{}L:E(X)  List.  \mforall{}e:E(X).
          \mexists{}e':E(X)
            (((e'  \mmember{}  L)  \mvee{}  (e'  =  e))
            \mwedge{}  (accumulate  (with  value  p1  and  list  item  e):
                    if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi 
                  over  list:
                      L
                  with  starting  value:
                    X(e))
                =  X(e')))
9.  u  :  E(X)
10.  v  :  E(X)  List
11.  \mleq{}(X)(e)  =  [u  /  v]@i
12.  e'  :  E(X)
13.  (e'  \mmember{}  v)  \mvee{}  (e'  =  u)
14.  accumulate  (with  value  p1  and  list  item  e):
          if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi 
        over  list:
            v
        with  starting  value:
          X(u))
=  X(e')
15.  e'  \mleq{}loc  e 
16.  accumulate  (with  value  p1  and  list  item  e):
          if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi 
        over  list:
            v
        with  starting  value:
          X(u))
=  X(e')
17.  e'@0  :  E(X)@i
18.  e'@0  \mleq{}loc  e  @i
\mvdash{}  fst(X(e'))  \msim{}  imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e)))


By

---

Latex:
\mbackslash{}p.  let  x,  y  =  dest\_sqequal  (concl  p)  in
                  (Assert  (mk\_equal\_term  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  x  y)
                  THENL  [Id;  HypSubst'  (-1)  0  THEN  Trivial]  )  p\mcdot{}

---

Home Index