---

Step * 1 of Lemma pv11_p1_pmax_wf


1. Cmd : ValueAllType
2. ldrs_uid : Id ─→ ℤ
⊢ λpvals.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) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) ─→ ((ℤ × Cmd) List)
BY
{ (MemCD THEN Try (CompleteAuto)) }

1
.....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

---

Latex:

---

Latex:

1.  Cmd  :  ValueAllType
2.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  \mlambda{}pvals.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{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)
    {}\mrightarrow{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List)


By

---

Latex:
(MemCD  THEN  Try  (CompleteAuto))

---

Home Index