---

Step * 1 1 of Lemma pv11_p1_pmax_wf

.....subterm..... T:t
1:n
1. Cmd : ValueAllType
2. ldrs_uid : Id ─→ ℤ
3. pvals : (pv11_p1_Ballot_Num() × ℤ × Cmd) List@i
⊢ let g = λbn,slt,z. let bn',z = z in let s',z = z in (slt =z s') ∧b (bn  < bn') in
   let P = λz.let bn,z = z 
              in let s,c = z 
                 in ¬b(∃zw∈pvals.g bn s zw)_b in
   mapfilter(λx.(snd(x));P;pvals) ∈ (ℤ × Cmd) List
BY
{ ((GenConclAtAddrType ⌈pv11_p1_Ballot_Num() ─→ ℤ ─→ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ 𝔹⌉ [2;1]⋅ THENA Auto)
   THEN Unfold `let` 0
   THEN Reduce 0
   THEN GenConclAtAddrType ⌈(pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ 𝔹⌉ [2;2]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Cmd  :  ValueAllType
2.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}
3.  pvals  :  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List@i
\mvdash{}  let  g  =  \mlambda{}bn,slt,z.  let  bn',z  =  z  in  let  s',z  =  z  in  (slt  =\msubz{}  s')  \mwedge{}\msubb{}  (bn    <  bn')  in
      let  P  =  \mlambda{}z.let  bn,z  =  z 
                            in  let  s,c  =  z 
                                  in  \mneg{}\msubb{}(\mexists{}zw\mmember{}pvals.g  bn  s  zw)\_b  in
      mapfilter(\mlambda{}x.(snd(x));P;pvals)  \mmember{}  (\mBbbZ{}  \mtimes{}  Cmd)  List


By

---

Latex:
((GenConclAtAddrType  \mkleeneopen{}pv11\_p1\_Ballot\_Num()  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}  [2;1]\mcdot{}
    THENA  Auto
    )
  THEN  Unfold  `let`  0
  THEN  Reduce  0
  THEN  GenConclAtAddrType  \mkleeneopen{}(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}  [2;2]\mcdot{}
  THEN  Auto)

---

Home Index