Nuprl Definition : coW-game

coW-game(a.B[a];w;w') ==
  <copath(a.B[a];w) × copath(a.B[a];w')
  , <(), ()>
  , λx,y. let u,v = x 
          in let u',v' = y 
             in ((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                ∧ copathAgree(a.B[a];w;u;u')
                ∧ (v = v' ∈ copath(a.B[a];w')))
                ∨ ((u = u' ∈ copath(a.B[a];w))
                  ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                  ∧ copathAgree(a.B[a];w';v;v'))
  , λx,y. let u,v = x 
          in let u',v' = y 
             in (((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                ∧ copathAgree(a.B[a];w;u;u')
                ∧ (v = v' ∈ copath(a.B[a];w')))
                ∨ ((u = u' ∈ copath(a.B[a];w))
                  ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                  ∧ copathAgree(a.B[a];w';v;v')))
                ∧ (copath-length(u') = copath-length(v') ∈ ℤ)>


Definitions occuring in Statement :  copathAgree: copathAgree(a.B[a];w;x;y),  copath-nil: (),  copath-length: copath-length(p),  copath: copath(a.B[a];w),  or: P ∨ Q,  and: P ∧ Q,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  product: x:A × B[x],  add: n + m,  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions occuring in definition :  product: x:A × B[x],  copath-nil: (),  pair: <a, b>,  lambda: λx.A[x],  spread: spread def,  or: P ∨ Q,  copath: copath(a.B[a];w),  and: P ∧ Q,  add: n + m,  natural_number: $n,  copathAgree: copathAgree(a.B[a];w;x;y),  equal: s = t ∈ T,  int: ℤ,  copath-length: copath-length(p)
FDL editor aliases :  coW-game
Latex:
coW-game(a.B[a];w;w')  ==
    <copath(a.B[a];w)  \mtimes{}  copath(a.B[a];w')
    ,  <(),  ()>
    ,  \mlambda{}x,y.  let  u,v  =  x 
                    in  let  u',v'  =  y 
                          in  ((copath-length(u')  =  (copath-length(u)  +  1))
                                \mwedge{}  copathAgree(a.B[a];w;u;u')
                                \mwedge{}  (v  =  v'))
                                \mvee{}  ((u  =  u')
                                    \mwedge{}  (copath-length(v')  =  (copath-length(v)  +  1))
                                    \mwedge{}  copathAgree(a.B[a];w';v;v'))
    ,  \mlambda{}x,y.  let  u,v  =  x 
                    in  let  u',v'  =  y 
                          in  (((copath-length(u')  =  (copath-length(u)  +  1))
                                \mwedge{}  copathAgree(a.B[a];w;u;u')
                                \mwedge{}  (v  =  v'))
                                \mvee{}  ((u  =  u')
                                    \mwedge{}  (copath-length(v')  =  (copath-length(v)  +  1))
                                    \mwedge{}  copathAgree(a.B[a];w';v;v')))
                                \mwedge{}  (copath-length(u')  =  copath-length(v'))>


Date html generated: 2019_06_20-PM-00_57_43
Last ObjectModification: 2019_01_02-PM-01_34_22

Theory : co-recursion-2


Home Index