---

Step * of Lemma wellfounded-llex-ext

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ((∀a,b:A.  SqStable(<[a;b]))
  ⇒ WellFnd{i}(A;a,b.<[a;b])
  ⇒ WellFnd{i}(Des(A;a,b.<[a;b]);L1,L2.L1 llex(A;a,b.<[a;b]) L2))
BY
{ Extract of Obid: wellfounded-llex
  not unfolding  listops 
  finishing with Auto
  normalizes to:
  
  λ%,%1,%2,n.
             if n = Ax then %2 [] 
                            (λk,%. case %
                                   of inl(%9) =>
                                   let %11,%12 = %9 
                                   in %2 k (λk1,%. (%1 (λj,%13. (%13 j Ax)) k1))
                                   | inr(%10) =>
                                   let i,%12,%14,%16,%17 = %10 in Ax)
             otherwise let u,v = n 
                       in %1 
                          (λj,%5,m,%6,k.
                                        if k = Ax
                                        then %2 (m @ [j]) 
                                             (λl,%8. case %8
                                                     of inl(x) =>
                                                     if (||l||) < (||m||)
                                                        then %6 l let %2,%3 = x in inl <Ax, λi.Ax>
                                                        else (%2 m %6)
                                                     | inr(x) =>
                                                     let x,%3 = x 
                                                     in if (x) < (||m||)
                                                           then %6 l let %4,%6,%8,%9 = %3 in inr <x, Ax, Ax, λj.Ax, %9> \000C  
                                                           else let x,x,x,%11 = %3 
                                                                in let x,%13 =
                                                                    rec-case(m) of
                                                                    [] => λl2.<λ%.<<λv.Ax, Ax, Ax>, λi.Ax>, λ%.<l2, Ax>>
                                                                    a::L =>
                                                                     r.λl2.rec-case(l2) of
                                                                           [] => <λ%1.let l,%2 = %1 
                                                                                      in <Ax, λi.Ax>
                                                                                 , λ%1.let %2,%3 = %1 
                                                                                       in Ax
                                                                                 >
                                                                           a::L@0 =>
                                                                            r@0.<λ%2.let %11,%12 = r L@0 
                                                                                     in let %13,%14 = %11 
                                                                                                      let l,%1 = %2 
                                                                                                      in <l, Ax> 
                                                                                        in let %15,%16 = r@0 
                                                                                           in <if (||L@0|| + 1) < (||L||
                                                                                                 + 1)
                                                                                                  then Ax
                                                                                                  else <λ%.Ax, Ax, Ax>
                                                                                              , λi.Ax
                                                                                              >
                                                                                , λ%2.let %3,%4 = %2 
                                                                                      in let %5,%6 = r@0 
                                                                                         in let %9,%10 = r L@0 
                                                                                            in let l,%3 =
                                                                                                %10 
                                                                                                <if (||L@0||) < (||L||)
                                                                                                    then Ax
                                                                                                    else <λ%.Ax, Ax, Ax>
                                                                                                , λi.Ax
                                                                                                > 
                                                                                               in <l, Ax>
                                                                                > 
                                                                    l 
                                                                   in let x,%13 = %13 
                                                                                  <if (||l||) < (||m||)
                                                                                      then Ax
                                                                                      else <λ%.Ax, Ax, Ax>
                                                                                  , λi.Ax
                                                                                  > 
                                                                      in if (0) < (||x||)
                                                                            then if x = Ax then Ax
                                                                                 otherwise let u,v = x 
                                                                                           in %5 u %11 m %6 v
                                                                            else (%2 m %6)  )
                                        otherwise let u,v = k 
                                                  in %5 u (% u j Ax) (m @ [j]) 
                                                     (λl,%8. case %8
                                                             of inl(x) =>
                                                             if (||l||) < (||m||)
                                                                then %6 l let %2,%3 = x in inl <Ax, λi.Ax>
                                                                else (%2 m %6)
                                                             | inr(x) =>
                                                             let x,%3 = x 
                                                             in if (x) < (||m||)
                                                                   then %6 l 
                                                                        let %4,%6,%8,%9 = %3 
                                                                        in inr <x, Ax, Ax, λj.Ax, %9>   
                                                                   else let x,x,x,%11 = %3 
                                                                        in let x,%13 =
                                                                            rec-case(m) of
                                                                            [] => λl2.<λ%.<<λv.Ax, Ax, Ax>, λi.Ax>
                                                                                      , λ%.<l2, Ax>
                                                                                      >
                                                                            a::L =>
                                                                             r.λl2.rec-case(l2) of
                                                                                   [] => <λ%1.let l,%2 = %1 
                                                                                              in <Ax, λi.Ax>
                                                                                         , λ%1.let %2,%3 = %1 
                                                                                               in Ax
                                                                                         >
                                                                                   a::L@0 =>
                                                                                    r@0.<λ%2.let %11,%12 = r L@0 
                                                                                             in let %13,%14 =
                                                                                                 %11 
                                                                                                 let l,%1 = %2 
                                                                                                 in <l, Ax> 
                                                                                                in let %15,%16 = r@0 
                                                                                                   in <if (||L@0||
                                                                                                         + 1) < (||L||
                                                                                                         + 1)
                                                                                                          then Ax
                                                                                                          else <λ%.Ax
                                                                                                               , Ax
                                                                                                               , Ax>
                                                                                                      , λi.Ax
                                                                                                      >
                                                                                        , λ%2.let %3,%4 = %2 
                                                                                              in let %5,%6 = r@0 
                                                                                                 in let %9,%10 = r L@0 
                                                                                                    in let l,%3 =
                                                                                                        %10 
                                                                                                        <...
                                                                                                        , λi.Ax
                                                                                                        > 
                                                                                                       in <l, Ax>
                                                                                        > 
                                                                            l 
                                                                           in let x,%13 = %13 
                                                                                          <if (||l||) < (||m||)
                                                                                              then Ax
                                                                                              else <λ%.Ax, Ax, Ax>
                                                                                          , λi.Ax
                                                                                          > 
                                                                              in if (0) < (||x||)
                                                                                    then if x = Ax then Ax
                                                                                         otherwise let u,v = x 
                                                                                                   in %5 u %11 m %6 v
                                                                                    else (%2 m %6)  ) 
                                                     v) 
                          u 
                          [] 
                          (λL,%. case %
                                 of inl(%9) =>
                                 let %10,%11 = %9 
                                 in %2 L (λk,%. (%1 (λj,%12. (%12 j Ax)) k))
                                 | inr(%10) =>
                                 let i,%12,%14,%16,%17 = %10 in Ax) 
                          v }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a,b:A.    SqStable(<[a;b]))
    {}\mRightarrow{}  WellFnd\{i\}(A;a,b.<[a;b])
    {}\mRightarrow{}  WellFnd\{i\}(Des(A;a,b.<[a;b]);L1,L2.L1  llex(A;a,b.<[a;b])  L2))


By

---

Latex:
Extract  of  Obid:  wellfounded-llex
not  unfolding    listops 
finishing  with  Auto
normalizes  to:

\mlambda{}\%,\%1,\%2,n.
                      if  n  =  Ax  then  \%2  [] 
                                                    (\mlambda{}k,\%.  case  \%
                                                                  of  inl(\%9)  =>
                                                                  let  \%11,\%12  =  \%9 
                                                                  in  \%2  k  (\mlambda{}k1,\%.  (\%1  (\mlambda{}j,\%13.  (\%13  j  Ax))  k1))
                                                                  |  inr(\%10)  =>
                                                                  let  i,\%12,\%14,\%16,\%17  =  \%10  in  Ax)
                      otherwise  let  u,v  =  n 
                                          in  \%1 
                                                (\mlambda{}j,\%5,m,\%6,k.
                                                                            if  k  =  Ax
                                                                            then  \%2  (m  @  [j]) 
                                                                                      (\mlambda{}l,\%8.  case  \%8
                                                                                                      of  inl(x)  =>
                                                                                                      if  (||l||)  <  (||m||)
                                                                                                            then  \%6  l  let  \%2,\%3  =  x  in  inl  <Ax,  \mlambda{}i.Ax>
                                                                                                            else  (\%2  m  \%6)
                                                                                                      |  inr(x)  =>
                                                                                                      let  x,\%3  =  x 
                                                                                                      in  if  (x)  <  (||m||)
                                                                                                                  then  \%6  l 
                                                                                                                            let  \%4,\%6,\%8,\%9  =  \%3 
                                                                                                                            in  inr  <x,  Ax,  Ax,  \mlambda{}j.Ax,  \%9>     
                                                                                                                  else  let  x,x,x,\%11  =  \%3 
                                                                                                                            in  let  x,\%13  =
                                                                                                                                    rec-case(m)  of
                                                                                                                                    []  =>  \mlambda{}l2.<\mlambda{}\%.<<\mlambda{}v.Ax,  Ax,  Ax>
                                                                                                                                                                ,  \mlambda{}i.Ax
                                                                                                                                                                >
                                                                                                                                                        ,  \mlambda{}\%.<l2,  Ax>
                                                                                                                                                        >
                                                                                                                                    a::L  =>
                                                                                                                                      r.\mlambda{}l2.rec-case(l2)  of
                                                                                                                                                  []  =>  <\mlambda{}\%1.let  l,\%2  =  \%1 
                                                                                                                                                                        in  <Ax,  \mlambda{}i.Ax>
                                                                                                                                                              ,  \mlambda{}\%1.let  \%2,\%3  =  \%1 
                                                                                                                                                                          in  Ax
                                                                                                                                                              >
                                                                                                                                                  a::L@0  =>
                                                                                                                                                    r@0.<\mlambda{}\%2.let  \%11,\%12  =
                                                                                                                                                                        r  L@0 
                                                                                                                                                                      in  let  \%13,\%14  =
                                                                                                                                                                              \%11 
                                                                                                                                                                              let  l,\%1  =
                                                                                                                                                                                \%2 
                                                                                                                                                                              in  <l,  Ax> 
                                                                                                                                                                            in  ...
                                                                                                                                                            ,  \mlambda{}\%2.let  \%3,\%4  =  \%2 
                                                                                                                                                                        in  let  \%5,\%6  =
                                                                                                                                                                                r@0 
                                                                                                                                                                              in  ...
                                                                                                                                                            > 
                                                                                                                                    l 
                                                                                                                                  in  let  x,\%13  =
                                                                                                                                          \%13 
                                                                                                                                          <if  (||l||)  <  (||m||)
                                                                                                                                                  then  Ax
                                                                                                                                                  else  <\mlambda{}\%.Ax,  Ax,  Ax>
                                                                                                                                          ,  \mlambda{}i.Ax
                                                                                                                                          > 
                                                                                                                                        in  if  (0)  <  (||x||)
                                                                                                                                                    then  if  x  =  Ax  then  Ax
                                                                                                                                                              otherwise  let  u,v  =
                                                                                                                                                                                    x 
                                                                                                                                                                                  in  \%5  u 
                                                                                                                                                                                        \%11 
                                                                                                                                                                                        m 
                                                                                                                                                                                        \%6 
                                                                                                                                                                                        v
                                                                                                                                                    else  (\%2  m  \%6)    )
                                                                            otherwise  let  u,v  =  k 
                                                                                                in  \%5  u  (\%  u  j  Ax)  (m  @  [j]) 
                                                                                                      (\mlambda{}l,\%8.  case  \%8
                                                                                                                      of  inl(x)  =>
                                                                                                                      if  (||l||)  <  (||m||)
                                                                                                                            then  \%6  l 
                                                                                                                                      let  \%2,\%3  =  x 
                                                                                                                                      in  inl  <Ax,  \mlambda{}i.Ax>
                                                                                                                            else  (\%2  m  \%6)
                                                                                                                      |  inr(x)  =>
                                                                                                                      let  x,\%3  =  x 
                                                                                                                      in  if  (x)  <  (||m||)
                                                                                                                                  then  \%6  l 
                                                                                                                                            let  \%4,\%6,\%8,\%9  =  \%3 
                                                                                                                                            in  inr  <x,  Ax,  Ax,  \mlambda{}j.Ax,  \%9>  \000C   
                                                                                                                                  else  let  x,x,x,\%11  =  \%3 
                                                                                                                                            in  let  x,\%13  =
                                                                                                                                                    rec-case(m)  of
                                                                                                                                                    []  =>  \mlambda{}l2.<\mlambda{}\%.<<\mlambda{}v.Ax
                                                                                                                                                                                  ,  Ax
                                                                                                                                                                                  ,  Ax>
                                                                                                                                                                                ,  \mlambda{}i.Ax
                                                                                                                                                                                >
                                                                                                                                                                        ,  \mlambda{}\%.<l2,  Ax>
                                                                                                                                                                        >
                                                                                                                                                    a::L  =>
                                                                                                                                                      r.\mlambda{}l2.rec-case(l2)  of
                                                                                                                                                                  []  =>  <\mlambda{}\%1....
                                                                                                                                                                              ,  \mlambda{}\%1....
                                                                                                                                                                              >
                                                                                                                                                                  a::L@0  =>
                                                                                                                                                                    r@0.<\mlambda{}\%2....
                                                                                                                                                                            ,  \mlambda{}\%2....
                                                                                                                                                                            > 
                                                                                                                                                    l 
                                                                                                                                                  in  let  x,\%13  =
                                                                                                                                                          \%13 
                                                                                                                                                          <if  (||l||)  <  (||m||)
                                                                                                                                                                  then  Ax
                                                                                                                                                                  else  <\mlambda{}\%.Ax
                                                                                                                                                                            ,  Ax
                                                                                                                                                                            ,  Ax>
                                                                                                                                                          ,  \mlambda{}i.Ax
                                                                                                                                                          > 
                                                                                                                                                        in  if  (0)  <  (||x||)
                                                                                                                                                                    then  if  x  =  Ax
                                                                                                                                                                              then  Ax
                                                                                                                                                                              otherwise  ...
                                                                                                                                                                    else  (\%2  m  \%6)    ) 
                                                                                                      v) 
                                                u 
                                                [] 
                                                (\mlambda{}L,\%.  case  \%
                                                              of  inl(\%9)  =>
                                                              let  \%10,\%11  =  \%9 
                                                              in  \%2  L  (\mlambda{}k,\%.  (\%1  (\mlambda{}j,\%12.  (\%12  j  Ax))  k))
                                                              |  inr(\%10)  =>
                                                              let  i,\%12,\%14,\%16,\%17  =  \%10  in  Ax) 
                                                v

---

Home Index