Bit ::= ✘ | ✔︎

not ✔︎ == ✘
not ✘ == ✔︎

not (not x) == x

FNil x := not (not x) NB. alternative: FNil := not $ not

FNil ✔︎ == ✔︎
FNil ✘ == ✘

Exercise: "prove" FNil (FNil x) == x

✔︎ || ✔︎ == ✔︎
✔︎ || ✘ == ✔︎
✘ || ✔︎ == ✔︎
✘ || ✘ == ✘

Exercise: properties of (||)

x <= y := x||y == y

✔︎ <= ✔︎
✘ <= ✘
✘ <= ✔︎

left implicit: (✔︎ <= ✘) == ✘

(x ==> y) := x <= y

x <= x
x <= y ==> y <= z ==> x <= z
x <= y ==> y <= x ==> x == y

z <= x ==> z <= y ==> (a <=x ==> a<=y ==> a<=z) ==> x && y == z

✔︎ && ✔︎ == ✔︎
✔︎ && ✘ == ✘
✘ && ✔︎ == ✘
✘ && ✘ == ✘

Exercise: properties of (&&)

Exericise: continuity of (||) and (&&)

(a ==> b ==> c) <=> (a && b) ==> c

(x <=> y) := x <= y && y <= x