Nuprl Definition : alt-swap-spec
alt-swap-spec(AType;n;prog) ==
∀A:Arr(AType). ∀i,j,k:ℕn.
(((A-post-val(AType;prog i j;A;j) = A-pre-val(AType;A;i) ∈ ℤ)
∧ (A-post-val(AType;prog i j;A;i) = A-pre-val(AType;A;j) ∈ ℤ))
∧ (((¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))) ⇒ (A-post-val(AType;prog i j;A;k) = A-pre-val(AType;A;k) ∈ ℤ)))
Definitions occuring in Statement :
A-post-val: A-post-val(AType;prog;A;i),
Arr: Arr(AType),
A-pre-val: A-pre-val(AType;A;i),
int_seg: {i..j-},
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
Arr: Arr(AType),
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
implies: P ⇒ Q,
and: P ∧ Q,
not: ¬A,
equal: s = t ∈ T,
int: ℤ,
A-post-val: A-post-val(AType;prog;A;i),
apply: f a,
A-pre-val: A-pre-val(AType;A;i)
FDL editor aliases :
alt-swap-spec
Latex:
alt-swap-spec(AType;n;prog) ==
\mforall{}A:Arr(AType). \mforall{}i,j,k:\mBbbN{}n.
(((A-post-val(AType;prog i j;A;j) = A-pre-val(AType;A;i))
\mwedge{} (A-post-val(AType;prog i j;A;i) = A-pre-val(AType;A;j)))
\mwedge{} (((\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))) {}\mRightarrow{} (A-post-val(AType;prog i j;A;k) = A-pre-val(AType;A;k))))
Date html generated:
2016_05_15-PM-02_20_49
Last ObjectModification:
2015_09_23-AM-07_38_51
Theory : monads
Home
Index