Express What, not How.

[Albert Lai]

Albert Lai <trebla at vex.net> writes:

> Hung  : LiDui
> MoYun : LiDui -> Bool
> PaiDui: (LiDui,Object) -> LiDui
> DuiTau: LiDui -> Object
> LeiDui: LiDui -> LiDui
> 
> MoYun(Hung) is true.
> For any LiDui d:
>   If MoYun(d) is true, we have LeiDui(PaiDui(d,o))=d and DuiTau(PaiDui(d,o))=o.
>   If MoYun(d) is false, we have LeiDui(PaiDui(d,o))=PaiDui(LeiDui(d),o).
> 
> That's it.

I knew I forgot something.

If MoYun(d) is false, we have LeiDui(PaiDui(d,o))=PaiDui(LeiDui(d),o)
and DuiTau(PaiDui(d,o))=DuiTau(d).

MoYun(PaiDui(d,o)) is false.