Nuprl Lemma : int_term_ind-add

[C,V,A,S,M,MN,a,b:Top].
  (int-term-ind-fun(c.C[c];
                    v.V[v];
                    l,r,rl,rr.A[l;r;rl;rr];
                    l,r,rl,rr.S[l;r;rl;rr];
                    l,r,rl,rr.M[l;r;rl;rr];
                    x,rx.MN[x;rx]) 
   (a (+) b) A[a;b;int-term-ind-fun(c.C[c];
                                      v.V[v];
                                      l,r,rl,rr.A[l;r;rl;rr];
                                      l,r,rl,rr.S[l;r;rl;rr];
                                      l,r,rl,rr.M[l;r;rl;rr];
                                      x,rx.MN[x;rx]) 
                     a;int-term-ind-fun(c.C[c];
                                        v.V[v];
                                        l,r,rl,rr.A[l;r;rl;rr];
                                        l,r,rl,rr.S[l;r;rl;rr];
                                        l,r,rl,rr.M[l;r;rl;rr];
                                        x,rx.MN[x;rx]) 
                       b])


Proof




Definitions occuring in Statement :  int-term-ind-fun: int-term-ind-fun itermAdd: left (+) right uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] so_apply: x[s] apply: a sqequal: t
Definitions unfolded in proof :  int-term-ind-fun: int-term-ind-fun itermAdd: left (+) right int_term_ind: int_term_ind uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalAxiom extract_by_obid hypothesis sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality because_Cache

Latex:
\mforall{}[C,V,A,S,M,MN,a,b:Top].
    (int-term-ind-fun(c.C[c];
                                        v.V[v];
                                        l,r,rl,rr.A[l;r;rl;rr];
                                        l,r,rl,rr.S[l;r;rl;rr];
                                        l,r,rl,rr.M[l;r;rl;rr];
                                        x,rx.MN[x;rx]) 
      (a  (+)  b)  \msim{}  A[a;b;int-term-ind-fun(c.C[c];
                                                                            v.V[v];
                                                                            l,r,rl,rr.A[l;r;rl;rr];
                                                                            l,r,rl,rr.S[l;r;rl;rr];
                                                                            l,r,rl,rr.M[l;r;rl;rr];
                                                                            x,rx.MN[x;rx]) 
                                          a;int-term-ind-fun(c.C[c];
                                                                                v.V[v];
                                                                                l,r,rl,rr.A[l;r;rl;rr];
                                                                                l,r,rl,rr.S[l;r;rl;rr];
                                                                                l,r,rl,rr.M[l;r;rl;rr];
                                                                                x,rx.MN[x;rx]) 
                                              b])



Date html generated: 2017_09_29-PM-05_52_01
Last ObjectModification: 2017_05_12-PM-00_04_24

Theory : omega


Home Index