Nuprl Lemma : simple-swap-correct
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:A-map Unit].
∀i,j:ℕn. simple-swap-specification(AType;n;simple-swap(array-model(AType);i;j);i;j)
Proof
Definitions occuring in Statement :
simple-swap: simple-swap(AModel;i;j),
simple-swap-specification: simple-swap-specification(AType;n;prog;i;j),
A-map: A-map,
array-model: array-model(AType),
array: array{i:l}(Val;n),
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
unit: Unit,
apply: f a,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
simple-swap-specification: simple-swap-specification(AType;n;prog;i;j),
simple-swap: simple-swap(AModel;i;j),
simple-swap-test2: simple-swap-test2(AModel;prog;i;j;k),
array-model: array-model(AType),
A-return: A-return(AModel),
A-fetch': A-fetch'(AModel),
A-coerce: A-coerce(AModel),
A-bind: A-bind(AModel),
A-assign: A-assign(AModel),
A-eval: A-eval(AModel),
pi2: snd(t),
pi1: fst(t),
array-monad: array-monad(AType),
M-return: M-return(Mnd),
M-bind: M-bind(Mnd),
let: let,
mk_monad: mk_monad(M;return;bind),
array: array{i:l}(Val;n),
Arr: Arr(AType),
idx: idx(AType),
upd: upd(AType),
nat: ℕ,
subtype_rel: A ⊆r B,
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
bfalse: ff,
prop: ℙ,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
int_seg: {i..j-},
bnot: ¬bb,
assert: ↑b,
false: False,
iff: P ⇐⇒ Q,
not: ¬A,
rev_implies: P ⇐ Q,
true: True,
so_lambda: λ2x.t[x],
so_apply: x[s],
cand: A c∧ B,
squash: ↓T,
ge: i ≥ j ,
lelt: i ≤ j < k,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
top: Top,
nequal: a ≠ b ∈ T
Lemmas referenced :
Arr_wf,
int_seg_wf,
assert_witness,
A-eval_wf,
bool_wf,
A-map_wf,
simple-swap-test2_wf,
simple-swap_wf,
unit_wf2,
array_wf,
nat_wf,
assert_wf,
eq_int_wf,
eqtt_to_assert,
assert_of_eq_int,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
bimplies_wf,
bnot_wf,
eqff_to_assert,
assert-bnot,
neg_assert_of_eq_int,
iff_transitivity,
not_wf,
iff_weakening_uiff,
assert_of_band,
assert_of_bnot,
isect_wf,
band_wf,
assert_of_bimplies,
squash_wf,
true_wf,
iff_weakening_equal,
equal-wf-T-base,
int_subtype_base,
int_seg_properties,
nat_properties,
decidable__equal_int,
satisfiable-full-omega-tt,
intformnot_wf,
intformeq_wf,
itermVar_wf,
int_formula_prop_not_lemma,
int_formula_prop_eq_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
uiff_transitivity,
bool_cases
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
extract_by_obid,
isectElimination,
intEquality,
hypothesisEquality,
hypothesis,
because_Cache,
natural_numberEquality,
setElimination,
rename,
lambdaEquality,
dependent_functionElimination,
applyEquality,
equalityTransitivity,
equalitySymmetry,
isectEquality,
universeEquality,
cumulativity,
functionEquality,
independent_functionElimination,
isect_memberEquality,
functionExtensionality,
unionElimination,
equalityElimination,
independent_isectElimination,
dependent_pairFormation,
promote_hyp,
instantiate,
voidElimination,
productEquality,
independent_pairFormation,
impliesFunctionality,
imageElimination,
imageMemberEquality,
baseClosed,
dependent_set_memberEquality,
int_eqEquality,
voidEquality,
computeAll
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[AType:array\{i:l\}(\mBbbZ{};n)]. \mforall{}[prog:A-map Unit].
\mforall{}i,j:\mBbbN{}n. simple-swap-specification(AType;n;simple-swap(array-model(AType);i;j);i;j)
Date html generated:
2017_10_01-AM-08_44_34
Last ObjectModification:
2017_07_26-PM-04_30_15
Theory : monads
Home
Index