Nuprl Lemma : update-assignment_wf

[Dom:Type]. ∀[a:FOAssignment(Dom)]. ∀[x:ℤ]. ∀[v:Dom].  (a[x := v] ∈ FOAssignment(Dom))


Proof




Definitions occuring in Statement :  update-assignment: a[x := v] FOAssignment: FOAssignment(Dom) uall: [x:A]. B[x] member: t ∈ T int: universe: Type
Lemmas :  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 FOAssignment_wf
\mforall{}[Dom:Type].  \mforall{}[a:FOAssignment(Dom)].  \mforall{}[x:\mBbbZ{}].  \mforall{}[v:Dom].    (a[x  :=  v]  \mmember{}  FOAssignment(Dom))



Date html generated: 2015_07_17-AM-07_53_09
Last ObjectModification: 2015_01_27-AM-10_07_13

Home Index