---

Step * of Lemma decidable__squash-list-match-ext

∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
  ((∀a:A. ∀b:B.  Dec(R[a;b])) ⇒ (∀as:A List. ∀bs:B List.  Dec(↓list-match(as;bs;a,b.R[a;b]))))
BY
{ Extract of Obid: decidable__squash-list-match
  not unfolding  int_seg_decide listops deq-member int-deq
  finishing with (RepUR ``let btrue`` 0 THEN Auto)
  normalizes to:
  
  let xx = inr (λx.let _,_ = x 
                   in Ax)  in
      λdcdr,as,bs. if rec-case(as) of
                      [] => λused.tt
                      a::L =>
                       r.λused.eval j' = ||bs|| in
                               if int_seg_decide(λj.if j ∈b used
                                                    then xx
                                                    else case dcdr a bs[j]
                                                          of inl(x) =>
                                                          case r [j / used] of inl(y) => inl <λ_.Ax, x, y> | inr(_) => x\000Cx
                                                          | inr(_) =>
                                                          xx
                                                    fi ;0;j')
                               then tt
                               else inr (λ_.Ax) 
                               fi  
                      []
                  then tt
                  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{}as:A  List.  \mforall{}bs:B  List.    Dec(\mdownarrow{}list-match(as;bs;a,b.R[a;b]))))


By

---

Latex:
Extract  of  Obid:  decidable\_\_squash-list-match
not  unfolding    int\_seg\_decide  listops  deq-member  int-deq
finishing  with  (RepUR  ``let  btrue``  0  THEN  Auto)
normalizes  to:

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

---

Home Index