Nuprl Lemma : mFOL-subst-abstract
The evidence that fmla[x/y] in Dom, S, a is the same as the evidence
that fmla is true in Dom, S, a[y := a x].⋅
∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(Dom)]. ∀[fmla:mFOL()]. ∀[x,y:ℤ].
(Dom,S,a |= mFOL-abstract(fmla[x/y]) = Dom,S,a[y := a x] |= mFOL-abstract(fmla) ∈ ℙ)
Proof
Definitions occuring in Statement :
mFOL-subst: fmla[nw/old],
mFOL-abstract: mFOL-abstract(fmla),
mFOL: mFOL(),
FOSatWith: Dom,S,a |= fmla,
update-assignment: a[x := v],
FOStruct: FOStruct(Dom),
FOAssignment: FOAssignment(Dom),
uall: ∀[x:A]. B[x],
prop: ℙ,
apply: f a,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
mFOL_wf,
equal_wf,
FOSatWith_wf,
mFOL-abstract_wf,
mFOL-rename_wf,
mFOL-rename-bound-to-avoid_wf,
cons_wf,
nil_wf,
AbstractFOFormula_wf,
l_disjoint_wf,
mFOL-boundvars_wf,
squash_wf,
true_wf,
FOAssignment_wf,
FOStruct_wf,
update-assignment_wf,
set_wf,
mFOL-abstract-rename,
cons_member,
l_member_wf
\mforall{}[Dom:Type]. \mforall{}[S:FOStruct(Dom)]. \mforall{}[a:FOAssignment(Dom)]. \mforall{}[fmla:mFOL()]. \mforall{}[x,y:\mBbbZ{}].
(Dom,S,a |= mFOL-abstract(fmla[x/y]) = Dom,S,a[y := a x] |= mFOL-abstract(fmla))
Date html generated:
2015_07_17-AM-07_54_41
Last ObjectModification:
2015_01_27-AM-10_07_12
Home
Index