Alloy model that demonstrate every non-distributive lattice contains one of the two particular lattices as a subpseudolattice.

DistributiveLattice.als

sig L {
  join, meet : L -> one L
}
one sig top, bot in L {}

fact {
  all x, y, z : L {
    -- commutativity
    x.join[y] = y.join[x]
    x.meet[y] = y.meet[x]

    -- associativity
    x.join[y].join[z] = x.join[y.join[z]]
    x.meet[y].meet[z] = x.meet[y.meet[z]]

    -- unit laws
    x.meet[top] = x
    x.join[bot] = x

    -- idempotence
    x.join[x] = x
    x.meet[x] = x

    -- absorption
    x.meet[x.join[y]] = x
    x.join[x.meet[y]] = x
  }
}

pred show {}
run show for 5 L

pred le[x, y : L] { x.join[y]=y }
pred le'[x, y : L] { x.meet[y]=x }

assert le_welldefined {
  all x, y : L | le[x,y] <=> le'[x,y]
}
check le_welldefined for 8 L

assert le_poset {
  -- reflexivity
  all x : L | le[x,x]

  -- transitivity
  all x, y, z : L | le[x,y] and le[y,z] => le[x,z]

  -- antisymmetry
  all x, y : L | le[x,y] and le[y,x] => x=y
}
check le_poset for 8 L

assert le_top { all x : L | le[x,top] }
check le_top for 8 L

assert le_bot { all x : L | le[bot,x] }
check le_bot for 8 L

pred distributivity {
  all x, y, z : L | x.meet[y.join[z]] = x.meet[y].join[x.meet[z]]
}
run distributivity for 5 L

pred distributivity' {
  all x, y, z : L | x.join[y.meet[z]] = x.join[y].meet[x.join[z]] 
}

assert dualDistributivityHolds{ distributivity => distributivity' }
check dualDistributivityHolds for 8 L

pred p1 {
  some disj a,b,c,d,e : L {
    a = a.join[b] 
    d = a.join[c]
    d = b.join[c]
    e = a.meet[c]
    e = b.meet[c]
  }
}

pred p2 {
  some disj a,b,c,d,e : L {
    d = a.join[b]
    d = a.join[c]
    d = b.join[c]
    e = a.meet[b]
    e = a.meet[c]
    e = b.meet[c]
  }
}

assert nondistributiveSubPseudoLattice {
  !distributivity <=> (p1 || p2)
}

check nondistributiveSubPseudoLattice for 8 L