Nuprl Lemma : int_term_ind-var

[C,V,A,S,M,MN,k: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]) 
   vk V[k])


Proof




Definitions occuring in Statement :  int-term-ind-fun: int-term-ind-fun itermVar: vvar 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 itermVar: vvar 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,k: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]) 
      vk  \msim{}  V[k])



Date html generated: 2017_09_29-PM-05_51_57
Last ObjectModification: 2017_05_12-PM-00_02_29

Theory : omega


Home Index