Nuprl Lemma : mFOL-abstract-rename

[Dom:Type]. ∀[S:FOStruct(Dom)].
  ∀x,y:ℤ. ∀fmla:mFOL().
    ((¬(x ∈ mFOL-boundvars(fmla)))
     (∀a1,a2:FOAssignment(Dom).
          ((a2 a1[y := a1 x] ∈ FOAssignment(Dom))
           (Dom,S,a2 |= mFOL-abstract(fmla) Dom,S,a1 |= mFOL-abstract(mFOL-rename(fmla;y;x)) ∈ ℙ))))


Proof




Definitions occuring in Statement :  mFOL-abstract: mFOL-abstract(fmla) mFOL-rename: mFOL-rename(fmla;old;new) mFOL-boundvars: mFOL-boundvars(fmla) mFOL: mFOL() FOSatWith: Dom,S,a |= fmla update-assignment: a[x := v] FOStruct: FOStruct(Dom) FOAssignment: FOAssignment(Dom) l_member: (x ∈ l) uall: [x:A]. B[x] prop: all: x:A. B[x] not: ¬A implies:  Q apply: a int: universe: Type equal: t ∈ T
Lemmas :  mFOL-induction not_wf l_member_wf mFOL-boundvars_wf all_wf FOAssignment_wf update-assignment_wf FOSatWith_wf mFOL-abstract_wf mFOL-rename_wf mFOL_wf list_induction equal_wf list_wf map_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int map_nil_lemma nil_wf map_cons_lemma cons_wf squash_wf true_wf iff_weakening_equal member-union int-deq_wf assert_of_eq_atom and_wf neg_assert_of_eq_atom eq_atom_wf or_wf mFOconnect_wf member-insert decidable__equal_int false_wf not-equal-2 le_antisymmetry_iff add_functionality_wrt_le add-swap add-commutes le-add-cancel add-associates equal-wf-base int_subtype_base exists_wf mFOquant_wf FOStruct_wf
\mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].
    \mforall{}x,y:\mBbbZ{}.  \mforall{}fmla:mFOL().
        ((\mneg{}(x  \mmember{}  mFOL-boundvars(fmla)))
        {}\mRightarrow{}  (\mforall{}a1,a2:FOAssignment(Dom).
                    ((a2  =  a1[y  :=  a1  x])
                    {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(fmla)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(fmla;y;x))))))



Date html generated: 2015_07_17-AM-07_54_28
Last ObjectModification: 2015_02_03-PM-09_39_04

Home Index