---

Step * of Lemma RankEx2_ind-unroll

∀[S,T,A:Type]. ∀[R:A ─→ RankEx2(S;T) ─→ ℙ]. ∀[LeafT,LeafS,Prod,Union,ListProd,UnionList:Top]. ∀[t:RankEx2(S;T)].
  (RankEx2_ind(t;
               RankEx2_LeafT(leaft)⇒ LeafT[leaft];
               RankEx2_LeafS(leafs)⇒ LeafS[leafs];
               RankEx2_Prod(prod)⇒ rec1.Prod[prod;rec1];
               RankEx2_Union(union)⇒ rec2.Union[union;rec2];
               RankEx2_ListProd(listprod)⇒ rec3.ListProd[listprod;rec3];
               RankEx2_UnionList(unionlist)⇒ rec4.UnionList[unionlist;rec4])  
  ~ let F = λt.RankEx2_ind(t;
                           RankEx2_LeafT(leaft)⇒ LeafT[leaft];
                           RankEx2_LeafS(leafs)⇒ LeafS[leafs];
                           RankEx2_Prod(prod)⇒ rec1.Prod[prod;rec1];
                           RankEx2_Union(union)⇒ rec2.Union[union;rec2];
                           RankEx2_ListProd(listprod)⇒ rec3.ListProd[listprod;rec3];
                           RankEx2_UnionList(unionlist)⇒ rec4.UnionList[unionlist;rec4])  in
        if RankEx2_LeafT?(t) then LeafT RankEx2_LeafT-leaft(t)
        if RankEx2_LeafS?(t) then LeafS RankEx2_LeafS-leafs(t)
        if RankEx2_Prod?(t) then Prod RankEx2_Prod-prod(t) (F (fst(fst(RankEx2_Prod-prod(t)))))
        if RankEx2_Union?(t)
          then Union RankEx2_Union-union(t) 
               case RankEx2_Union-union(t) of inl(x) => let x1,x2 = x in F x2 | inr(y) => F y
        if RankEx2_ListProd?(t)
          then ListProd RankEx2_ListProd-listprod(t) (λi.let u2,u3 = RankEx2_ListProd-listprod(t)[i] in F u3)
        else UnionList RankEx2_UnionList-unionlist(t) 
             case RankEx2_UnionList-unionlist(t) of inl(x) => Ax | inr(y) => λi.(F y[i])
        fi )
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] RecUnfoldTopAbC) 0
   THEN D -1
   THEN RepUR ``let so_apply`` 0
   THEN Try (Trivial)
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Try (Trivial)) }

---

Latex:


\mforall{}[S,T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx2(S;T)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[LeafT,LeafS,Prod,Union,ListProd,UnionList:Top].
\mforall{}[t:RankEx2(S;T)].
    (RankEx2\_ind(t;
                              RankEx2\_LeafT(leaft){}\mRightarrow{}  LeafT[leaft];
                              RankEx2\_LeafS(leafs){}\mRightarrow{}  LeafS[leafs];
                              RankEx2\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                              RankEx2\_Union(union){}\mRightarrow{}  rec2.Union[union;rec2];
                              RankEx2\_ListProd(listprod){}\mRightarrow{}  rec3.ListProd[listprod;rec3];
                              RankEx2\_UnionList(unionlist){}\mRightarrow{}  rec4.UnionList[unionlist;rec4])   
    \msim{}  let  F  =  \mlambda{}t.RankEx2\_ind(t;
                                                      RankEx2\_LeafT(leaft){}\mRightarrow{}  LeafT[leaft];
                                                      RankEx2\_LeafS(leafs){}\mRightarrow{}  LeafS[leafs];
                                                      RankEx2\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                                                      RankEx2\_Union(union){}\mRightarrow{}  rec2.Union[union;rec2];
                                                      RankEx2\_ListProd(listprod){}\mRightarrow{}  rec3.ListProd[listprod;rec3];
                                                      RankEx2\_UnionList(unionlist){}\mRightarrow{}  rec4.UnionList[unionlist;rec4])    in
                if  RankEx2\_LeafT?(t)  then  LeafT  RankEx2\_LeafT-leaft(t)
                if  RankEx2\_LeafS?(t)  then  LeafS  RankEx2\_LeafS-leafs(t)
                if  RankEx2\_Prod?(t)  then  Prod  RankEx2\_Prod-prod(t)  (F  (fst(fst(RankEx2\_Prod-prod(t)))))
                if  RankEx2\_Union?(t)
                    then  Union  RankEx2\_Union-union(t) 
                              case  RankEx2\_Union-union(t)  of  inl(x)  =>  let  x1,x2  =  x  in  F  x2  |  inr(y)  =>  F  y
                if  RankEx2\_ListProd?(t)
                    then  ListProd  RankEx2\_ListProd-listprod(t) 
                              (\mlambda{}i.let  u2,u3  =  RankEx2\_ListProd-listprod(t)[i] 
                                      in  F  u3)
                else  UnionList  RankEx2\_UnionList-unionlist(t) 
                          case  RankEx2\_UnionList-unionlist(t)  of  inl(x)  =>  Ax  |  inr(y)  =>  \mlambda{}i.(F  y[i])
                fi  )


By

((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  0
  THEN  D  -1
  THEN  RepUR  ``let  so\_apply``  0
  THEN  Try  (Trivial)
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index