Nuprl Lemma : mFOL-abstract-functionality

[fmla:mFOL()]. ∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a1,a2:FOAssignment(Dom)].
  Dom,S,a1 |= mFOL-abstract(fmla) Dom,S,a2 |= mFOL-abstract(fmla) ∈ ℙ 
  supposing ∀z:ℤ((z ∈ mFOL-freevars(fmla))  ((a1 z) (a2 z) ∈ Dom))


Proof




Definitions occuring in Statement :  mFOL-abstract: mFOL-abstract(fmla) mFOL-freevars: mFOL-freevars(fmla) mFOL: mFOL() FOSatWith: Dom,S,a |= fmla FOStruct: FOStruct(Dom) FOAssignment: FOAssignment(Dom) l_member: (x ∈ l) uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] implies:  Q apply: a int: universe: Type equal: t ∈ T
Lemmas :  mFOL-induction all_wf FOAssignment_wf l_member_wf mFOL-freevars_wf FOSatWith_wf mFOL-abstract_wf mFOL_wf mFOatomic_wf list_wf mFOconnect_wf mFOquant_wf bool_wf FOStruct_wf member-remove-repeats int-deq_wf list_induction map_wf map_nil_lemma nil_wf map_cons_lemma cons_wf squash_wf true_wf cons_member equal_wf iff_weakening_equal eq_atom_wf eqtt_to_assert assert_of_eq_atom and_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom or_wf int-valueall-type val-union-l-union member-union update-assignment_wf eq_int_wf assert_of_eq_int neg_assert_of_eq_int member_filter bnot_wf iff_transitivity assert_wf not_wf equal-wf-base int_subtype_base iff_weakening_uiff assert_of_bnot exists_wf
\mforall{}[fmla:mFOL()].  \mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].  \mforall{}[a1,a2:FOAssignment(Dom)].
    Dom,S,a1  |=  mFOL-abstract(fmla)  =  Dom,S,a2  |=  mFOL-abstract(fmla) 
    supposing  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(fmla))  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))



Date html generated: 2015_07_17-AM-07_54_27
Last ObjectModification: 2015_02_03-PM-09_38_54

Home Index