Problem:
 or(x,x) -> x
 and(x,x) -> x
 not(not(x)) -> x
 not(and(x,y)) -> or(not(x),not(y))
 not(or(x,y)) -> and(not(x),not(y))

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {6,4,3,2}
   transitions:
    or0(6,6) -> 2*
    or0(1,6) -> 2*
    or0(6,1) -> 2*
    or0(1,1) -> 2*
    and0(6,6) -> 3*
    and0(1,6) -> 3*
    and0(6,1) -> 3*
    and0(1,1) -> 3*
    not0(6) -> 4*
    not0(1) -> 4*
    f60() -> 6*,2,3,1
    1 -> 3,2
    6 -> 3,2
  problem:
   
  Qed