# Re: completeness of the relational lattice

Date: Fri, 29 Jun 2007 23:42:00 -0000

Message-ID: <1183160520.469343.51250_at_w5g2000hsg.googlegroups.com>

On 30 jun, 00:00, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:

> On Jun 29, 1:40 pm, Jan Hidders <hidd..._at_gmail.com> wrote:

*>
**>
**>
**> > On 29 jun, 18:20, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
**>
**> > > On Jun 28, 3:41 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
**>
**> > > > > > I invite you to challenge me to show that it can prove an equation
**> > > > > > that holds. Of course you should also check if all these equations can
**> > > > > > be derived by you.
**>
**> > > One more challenge:
**>
**> > > <xy> + S + Q = <xy> + S
**>
**> > > where S * [] = [z], and Q header is unconstrained. (I don't see axioms
**> > > about the lattice bottom element:-)
**>
**> > Sorry. The rules axiomatize the algebra for relations with finite
**> > headers. [...]
**>
**> I'm OK with no W.
*

Ok. I misunderstood "unconstrained". You mean it is an arbitrary header.

It seems I forgot a rule :-( (it turns out I needed it in a part of
the proof I had no worked out yet)

This rule is of course:

(62) r + <> = <>

And then it is easy:

<xy> + S + Q

(20) = <xy> + S + (S * []) + Q (22) = <xy> + S + [z] + Q (26) = <> + S + Q (62) = <> (62) = <> + S (26) = <xy> + S + [z] (22) = <xy> + S + (S * []) (20) = <xy> + S

- Jan Hidders