---

Step * of Lemma decidable__squash-list-match-aux-ext

∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
  ((∀a:A. ∀b:B.  Dec(R[a;b])) ⇒ (∀bs:B List. ∀as:A List. ∀used:ℤ List.  Dec(↓list-match-aux(as;bs;used;a,b.R[a;b]))))
BY
{ Extract of Obid: decidable__squash-list-match-aux
  not unfolding  listops int_seg_decide int-deq deq-member
  finishing with Auto
  normalizes to:
  
  λdcdr,bs,as. rec-case(as) of
               [] => λused.(inl Ax)
               a::L =>
                r.λused.eval j' = ||bs|| in
                        if int_seg_decide(λj.if j ∈b used
                                             then inr (λ%.let %4,%5 = % 
                                                          in Ax) 
                                             else case dcdr a bs[j]
                                                   of inl(x) =>
                                                   case r [j / used]
                                                    of inl(y) =>
                                                    inl <λ_.Ax, x, y>
                                                    | inr(_) =>
                                                    inr (λx.let _,_ = x 
                                                            in Ax) 
                                                   | inr(_) =>
                                                   inr (λx.let _,_ = x 
                                                           in Ax) 
                                             fi ;0;j')
                        then inl Ax
                        else inr (λ_.Ax) 
                        fi  }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:A.  \mforall{}b:B.    Dec(R[a;b]))
    {}\mRightarrow{}  (\mforall{}bs:B  List.  \mforall{}as:A  List.  \mforall{}used:\mBbbZ{}  List.    Dec(\mdownarrow{}list-match-aux(as;bs;used;a,b.R[a;b]))))


By

---

Latex:
Extract  of  Obid:  decidable\_\_squash-list-match-aux
not  unfolding    listops  int\_seg\_decide  int-deq  deq-member
finishing  with  Auto
normalizes  to:

\mlambda{}dcdr,bs,as.  rec-case(as)  of
                          []  =>  \mlambda{}used.(inl  Ax)
                          a::L  =>
                            r.\mlambda{}used.eval  j'  =  ||bs||  in
                                            if  int\_seg\_decide(\mlambda{}j.if  j  \mmember{}\msubb{}  used
                                                                                      then  inr  (\mlambda{}\%.let  \%4,\%5  =  \% 
                                                                                                                in  Ax) 
                                                                                      else  case  dcdr  a  bs[j]
                                                                                                  of  inl(x)  =>
                                                                                                  case  r  [j  /  used]
                                                                                                    of  inl(y)  =>
                                                                                                    inl  <\mlambda{}$_{}$.Ax,  x,  y>
                                                                                                    |  inr($_{}$)  =>
                                                                                                    inr  (\mlambda{}x.let  $_{}$,$_\mbackslash{}f\000Cf7b}$  =  x 
                                                                                                                    in  Ax) 
                                                                                                  |  inr($_{}$)  =>
                                                                                                  inr  (\mlambda{}x.let  $_{}$,$_\mbackslash{}ff\000C7b}$  =  x 
                                                                                                                  in  Ax) 
                                                                                      fi  ;0;j')
                                            then  inl  Ax
                                            else  inr  (\mlambda{}$_{}$.Ax) 
                                            fi 

---

Home Index