---

Step * of Lemma decidable__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__list-match
  not unfolding  int_seg_decide listops deq-member int-deq
  finishing with Auto
  normalizes to:
  
  λdcd,as,bs. case rec-case(as) of
                   [] => λused.(inl (λx.x))
                   a::L =>
                    r.λused.eval j' = ||bs|| in
                            case int_seg_decide(λj.if j ∈b used
                                                   then inr (λ%.let %4,%5 = % 
                                                                in Ax) 
                                                   else case dcd a bs[j]
                                                         of inl(a) =>
                                                         case r [j / used]
                                                          of inl(b) =>
                                                          inl <λ%.Ax, a, b>
                                                          | inr(_) =>
                                                          inr (λx.let _,_ = x 
                                                                  in Ax) 
                                                         | inr(_) =>
                                                         inr (λx.let _,_ = x 
                                                                 in Ax) 
                                                   fi ;0;j')
                             of inl(soln) =>
                             inl let j,_,_,f = soln 
                                 in λi.if i=0 then j else (f (i - 1))  
                             | inr(_) =>
                             inr (λ_.Ax)  
                   []
              of inl(f) =>
              inl f
              | inr(_) =>
              inr (λ_.Ax)  }

---

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(list-match(as;bs;a,b.R[a;b]))))


By

---

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

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

---

Home Index