Nuprl Lemma : update-assignment_wf
∀[vs:ℤ List]. ∀[z:ℤ]. ∀[Dom:Type]. ∀[a:FOAssignment(filter(λx.(¬b(x =z z));vs),Dom)]. ∀[v:Dom].
(a[z := v] ∈ FOAssignment(vs,Dom))
Proof
Definitions occuring in Statement :
update-assignment: a[x := v],
FOAssignment: FOAssignment(vs,Dom),
filter: filter(P;l),
list: T List,
bnot: ¬bb,
eq_int: (i =z j),
uall: ∀[x:A]. B[x],
member: t ∈ T,
lambda: λx.A[x],
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
FOAssignment: FOAssignment(vs,Dom),
update-assignment: a[x := v],
all: ∀x:A. B[x],
prop: ℙ,
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
false: False,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
not: ¬A,
nequal: a ≠ b ∈ T
Lemmas referenced :
l_member_wf,
eq_int_wf,
bool_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
filter_wf5,
bnot_wf,
member_filter,
iff_transitivity,
assert_wf,
not_wf,
iff_weakening_uiff,
assert_of_bnot,
assert_of_eq_int,
FOAssignment_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
lambdaEquality,
lambdaFormation,
extract_by_obid,
isectElimination,
thin,
intEquality,
hypothesisEquality,
hypothesis,
setElimination,
rename,
unionElimination,
equalityElimination,
sqequalRule,
productElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
dependent_pairFormation,
promote_hyp,
dependent_functionElimination,
instantiate,
cumulativity,
independent_functionElimination,
because_Cache,
voidElimination,
applyEquality,
functionExtensionality,
setEquality,
dependent_set_memberEquality,
independent_pairFormation,
impliesFunctionality,
axiomEquality,
isect_memberEquality,
universeEquality
Latex:
\mforall{}[vs:\mBbbZ{} List]. \mforall{}[z:\mBbbZ{}]. \mforall{}[Dom:Type]. \mforall{}[a:FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x =\msubz{} z));vs),Dom)]. \mforall{}[v:Dom].
(a[z := v] \mmember{} FOAssignment(vs,Dom))
Date html generated:
2018_05_21-PM-10_20_31
Last ObjectModification:
2017_07_26-PM-06_37_30
Theory : minimal-first-order-logic
Home
Index