Nuprl Definition : eq_seq

eq_seq(eq) ==  λs1,s2. let k1,g1 = s1 in let k2,g2 = s2 in (k1 =z k2) ∧b primrec(k1;tt;λi,b. ((eq (g1 i) (g2 i)) ∧b b))


Definitions occuring in Statement :  band: p ∧b q,  primrec: primrec(n;b;c),  eq_int: (i =z j),  btrue: tt,  apply: f a,  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  spread: spread def,  eq_int: (i =z j),  primrec: primrec(n;b;c),  btrue: tt,  lambda: λx.A[x],  band: p ∧b q,  apply: f a
FDL editor aliases :  eq_seq
Latex:
eq\_seq(eq)  ==
    \mlambda{}s1,s2.  let  k1,g1  =  s1 
                    in  let  k2,g2  =  s2 
                          in  (k1  =\msubz{}  k2)  \mwedge{}\msubb{}  primrec(k1;tt;\mlambda{}i,b.  ((eq  (g1  i)  (g2  i))  \mwedge{}\msubb{}  b))


Date html generated: 2016_05_15-PM-04_44_33
Last ObjectModification: 2015_09_23-AM-07_50_14

Theory : general


Home Index