Nuprl Definition : coPathAgree

coPathAgree(a.B[a];n;w;p;q) ==
  if (n =z 0)
  then True
  else let t,p' = p 
       in let t',q' = q 
          in (t = t' ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n - 1;coW-item(w;t);p';q')
  fi 


Definitions occuring in Statement :  coW-item: coW-item(w;b),  coW-dom: coW-dom(a.B[a];w),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  and: P ∧ Q,  true: True,  spread: spread def,  subtract: n - m,  natural_number: $n,  equal: s = t ∈ T
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  true: True,  spread: spread def,  and: P ∧ Q,  equal: s = t ∈ T,  coW-dom: coW-dom(a.B[a];w),  subtract: n - m,  natural_number: $n,  coW-item: coW-item(w;b)
FDL editor aliases :  coPathAgree
Latex:
coPathAgree(a.B[a];n;w;p;q)  ==
    if  (n  =\msubz{}  0)
    then  True
    else  let  t,p'  =  p 
              in  let  t',q'  =  q 
                    in  (t  =  t')  \mwedge{}  coPathAgree(a.B[a];n  -  1;coW-item(w;t);p';q')
    fi 


Date html generated: 2019_06_20-PM-00_56_14
Last ObjectModification: 2019_01_02-PM-01_32_55

Theory : co-recursion-2


Home Index