---

{ StandardDS  DS({1..6}) }

{ Proof }

---

Definitions occuring in Statement :  standard-ds: StandardDS,  int_seg: {i..j},  member: t  T,  natural_number: $n,  discrete_struct: DS(A)
Definitions :  standard-ds: StandardDS,  member: t  T,  discrete_struct: DS(A),  prop: ,  ifthenelse: if b then t else f fi ,  implies: P  Q,  btrue: tt,  bfalse: ff,  all: x:A. B[x],  int_seg: {i..j},  bool: ,  iff: P  Q,  unit: Unit,  and: P  Q,  it:
Lemmas :  IdLnk_wf,  ifthenelse_wf,  idlnk-deq_wf,  int_seg_wf,  Id_wf,  assert_wf,  id-deq_wf,  deq_wf,  not_wf,  eq_int_wf,  bnot_wf,  bool_wf,  not_functionality_wrt_iff,  iff_transitivity,  eqff_to_assert,  eqtt_to_assert,  assert_of_eq_int,  assert_of_bnot

---

StandardDS  \mmember{}  DS(\{1..6\msupminus{}\})


Date html generated: 2010_08_26-PM-11_41_36
Last ObjectModification: 2008_02_27-PM-09_34_20

Home Index