---

{ 4 : 2  6 : 2  7 : 5
= <[4; 6; 7], x.if deq-member(IntDeq;x;[4; 6]) then 2 else 5 fi > }

{ Proof }

---

Definitions occuring in Statement :  fpf-single: x : v,  fpf-join: f  g,  fpf: a:A fp-> B[a],  ifthenelse: if b then t else f fi ,  lambda: x.A[x],  pair: <a, b>,  cons: [car / cdr],  nil: [],  natural_number: $n,  int: ,  equal: s = t,  deq-member: deq-member(eq;x;L),  int-deq: IntDeq
Definitions :  ifthenelse: if b then t else f fi ,  deq-member: deq-member(eq;x;L),  int-deq: IntDeq,  fpf-join: f  g,  fpf-single: x : v,  btrue: tt,  bfalse: ff,  bor: p q,  eqof: eqof(d),  reduce: reduce(f;k;as),  eq_int: (i = j),  append: as @ bs,  pi1: fst(t),  filter: filter(P;l),  bnot: b,  fpf-dom: x  dom(f),  fpf-cap: f(x)?z,  fpf-ap: f(x),  pi2: snd(t),  member: t  T,  so_lambda: x.t[x],  all: x:A. B[x],  so_apply: x[s]
Lemmas :  fpf-join_wf,  fpf-single_wf,  int-deq_wf

---

4  :  2  \moplus{}  6  :  2  \moplus{}  7  :  5  =  <[4;  6;  7],  \mlambda{}x.if  deq-member(IntDeq;x;[4;  6])  then  2  else  5  fi  >


Date html generated: 2010_08_26-PM-11_57_32
Last ObjectModification: 2009_06_17-PM-05_14_37

Home Index