Nuprl Definition : coW-game2
coW-game2(a.B[a];w;w'';w') ==
<copath(a.B[a];w) × copath(a.B[a];w'') × copath(a.B[a];w')
, <(), (), ()>
, λx,y. let u,z,v = x in
let u',z',v' = y in
((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;u;u')
∧ (v = v' ∈ copath(a.B[a];w'))
∧ (z = z' ∈ copath(a.B[a];w'')))
∨ (((u = u' ∈ copath(a.B[a];w)) ∧ (z = z' ∈ copath(a.B[a];w'')))
∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w';v;v'))
, λx,y. let u,z,v = x in
let u',z',v' = y in
((copath-length(z') = (copath-length(z) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w'';z;z')
∧ (((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') ∈ ℤ)
∧ (copath-length(z') = 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),
spreadn: spread3,
or: P ∨ Q,
and: P ∧ Q,
lambda: λx.A[x],
pair: <a, b>,
product: x:A × B[x],
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
copath-length: copath-length(p),
int: ℤ,
equal: s = t ∈ T,
and: P ∧ Q,
copathAgree: copathAgree(a.B[a];w;x;y),
natural_number: $n,
add: n + m,
copath: copath(a.B[a];w),
or: P ∨ Q,
spreadn: spread3,
lambda: λx.A[x],
pair: <a, b>,
copath-nil: (),
product: x:A × B[x]
FDL editor aliases :
coW-game2
Latex:
coW-game2(a.B[a];w;w'';w') ==
<copath(a.B[a];w) \mtimes{} copath(a.B[a];w'') \mtimes{} copath(a.B[a];w')
, <(), (), ()>
, \mlambda{}x,y. let u,z,v = x in
let u',z',v' = y in
((copath-length(u') = (copath-length(u) + 1))
\mwedge{} copathAgree(a.B[a];w;u;u')
\mwedge{} (v = v')
\mwedge{} (z = z'))
\mvee{} (((u = u') \mwedge{} (z = z'))
\mwedge{} (copath-length(v') = (copath-length(v) + 1))
\mwedge{} copathAgree(a.B[a];w';v;v'))
, \mlambda{}x,y. let u,z,v = x in
let u',z',v' = y in
((copath-length(z') = (copath-length(z) + 1))
\mwedge{} copathAgree(a.B[a];w'';z;z')
\mwedge{} (((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'))
\mwedge{} (copath-length(z') = copath-length(v'))>
Date html generated:
2018_07_25-PM-01_43_16
Last ObjectModification:
2018_06_22-PM-05_14_16
Theory : co-recursion
Home
Index