Nuprl Definition : coWtransInvariant
coWtransInvariant(x.B[x];w1;w2;w3;k;X;Y;a;b;moves) ==
(||a|| = ((2 * k) + 2) ∈ ℤ)
∧ (||b|| = ((2 * k) + 2) ∈ ℤ)
∧ (moves[(2 * k) + 1] = <fst(a[(2 * k) + 1]), snd(b[(2 * k) + 1])> ∈ Pos(coW-game(a.B[a];w1;w3)))
∧ ((snd((X a))) = (fst((Y b))) ∈ copath(a.B[a];w2))
∧ (((copath-length(snd(a[(2 * k) + 1])) = (copath-length(fst(b[(2 * k) + 1])) + 1) ∈ ℤ)
∧ (copath-length(snd(a[(2 * k) + 1])) = (copath-length(fst(a[(2 * k) + 1])) + 1) ∈ ℤ))
∨ ((copath-length(fst(b[(2 * k) + 1])) = (copath-length(snd(a[(2 * k) + 1])) + 1) ∈ ℤ)
∧ (copath-length(fst(b[(2 * k) + 1])) = (copath-length(snd(b[(2 * k) + 1])) + 1) ∈ ℤ)))
Definitions occuring in Statement :
coW-game: coW-game(a.B[a];w;w'),
copath-length: copath-length(p),
copath: copath(a.B[a];w),
play-len: ||moves||,
play-item: moves[i],
sg-pos: Pos(g),
seq-item: s[i],
pi1: fst(t),
pi2: snd(t),
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
pair: <a, b>,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
natural_number: $n,
multiply: n * m,
add: n + m,
play-item: moves[i],
pi2: snd(t),
copath-length: copath-length(p),
pi1: fst(t),
int: ℤ,
equal: s = t ∈ T,
and: P ∧ Q,
or: P ∨ Q,
apply: f a,
copath: copath(a.B[a];w),
pair: <a, b>,
seq-item: s[i],
coW-game: coW-game(a.B[a];w;w'),
sg-pos: Pos(g),
play-len: ||moves||
FDL editor aliases :
coWtransInvariant
Latex:
coWtransInvariant(x.B[x];w1;w2;w3;k;X;Y;a;b;moves) ==
(||a|| = ((2 * k) + 2))
\mwedge{} (||b|| = ((2 * k) + 2))
\mwedge{} (moves[(2 * k) + 1] = <fst(a[(2 * k) + 1]), snd(b[(2 * k) + 1])>)
\mwedge{} ((snd((X a))) = (fst((Y b))))
\mwedge{} (((copath-length(snd(a[(2 * k) + 1])) = (copath-length(fst(b[(2 * k) + 1])) + 1))
\mwedge{} (copath-length(snd(a[(2 * k) + 1])) = (copath-length(fst(a[(2 * k) + 1])) + 1)))
\mvee{} ((copath-length(fst(b[(2 * k) + 1])) = (copath-length(snd(a[(2 * k) + 1])) + 1))
\mwedge{} (copath-length(fst(b[(2 * k) + 1])) = (copath-length(snd(b[(2 * k) + 1])) + 1))))
Date html generated:
2019_06_20-PM-01_06_54
Last ObjectModification:
2019_01_02-PM-01_34_52
Theory : co-recursion-2
Home
Index