---

{ [X:{j}]. [x:Pi_term]. [zero:X]. [comm:pre:pi_prefix()
                                              body:Pi_term
                                              rec1:X
                                              X].
  [option,par:left:Pi_term  right:Pi_term  rec1:X  rec2:X  X].
  [rep:body:Pi_term  rec1:X  X]. [new:name:Name
                                             body:Pi_term
                                             rec1:X
                                             X].
    (F(x) where 
     F(0) = zero  
     F(pre.body) = comm[pre;body;rec1] where  
                    rec1 = F(body)   
     F(left + right) = option[left;right;rec1;rec2] where  
                        rec1 = F(left)  
                        rec2 = F(right)  
     F(left | right) = par[left;right;rec1;rec2] where  
                        rec1 = F(left)  
                        rec2 = F(right)  
     F(!body) = rep[body;rec1] where  
                 rec1 = F(body)  
     F(new name.body) = new[name;body;rec1] where  
                         rec1 = F(body)  X) }

{ Proof }

---

Definitions occuring in Statement :  pi_term_ind: pi_term_ind,  pi_term: Pi_term,  pi_prefix: pi_prefix(),  name: Name,  uall: [x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2],  member: t  T,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  pi_term: Pi_term,  member: t  T,  pi_term_ind: pi_term_ind,  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  type-monotone: Monotone(T.F[T]),  uimplies: b supposing a,  ycomb: Y,  pi1: fst(t),  pi2: snd(t)
Lemmas :  unit_wf,  pi_prefix_wf,  name_wf,  subtype_rel_sum,  subtype_rel_simple_product,  pi_term_wf

---

\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:Pi\_term].  \mforall{}[zero:X].  \mforall{}[comm:pre:pi\_prefix()  {}\mrightarrow{}  body:Pi\_term  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  X].
\mforall{}[option,par:left:Pi\_term  {}\mrightarrow{}  right:Pi\_term  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  rec2:X  {}\mrightarrow{}  X].  \mforall{}[rep:body:Pi\_term
                                                                                                                                                        {}\mrightarrow{}  rec1:X
                                                                                                                                                        {}\mrightarrow{}  X].
\mforall{}[new:name:Name  {}\mrightarrow{}  body:Pi\_term  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  X].
    (F(x)  where 
      F(0)  =  zero   
      F(pre.body)  =  comm[pre;body;rec1]  where   
                                    rec1  =  F(body)     
      F(left  +  right)  =  option[left;right;rec1;rec2]  where   
                                            rec1  =  F(left)   
                                            rec2  =  F(right)   
      F(left  |  right)  =  par[left;right;rec1;rec2]  where   
                                            rec1  =  F(left)   
                                            rec2  =  F(right)   
      F(!body)  =  rep[body;rec1]  where   
                              rec1  =  F(body)   
      F(new  name.body)  =  new[name;body;rec1]  where   
                                              rec1  =  F(body)  \mmember{}  X)


Date html generated: 2011_08_17-PM-06_42_30
Last ObjectModification: 2011_06_18-PM-12_10_07

Home Index