💾 Archived View for oortcloud.flounder.online › junk › Afoundations.gmi captured on 2024-02-05 at 09:24:09. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
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