namespace http://cds.omdoc.org/examples❚
/T regular bands and views between them
mostly following the wikipedia page on Bands
Notes:
- some names that were not given on Wikipedia are made up
- most views do not actually use (all of) the Band properties
- LeftX and RightX are stronger than X, not weaker
❚
theory Regular : ?FOLEQNatDed =
include ?Band ❙
regular: {x,y,z} ⊦ z∘x∘z∘y∘z ≐ z∘x∘y∘z ❙
❚
theory LeftNormal : ?FOLEQNatDed =
include ?Band ❙
leftregular1: {x,y,z} ⊦ z∘x∘z∘y ≐ z∘x∘y ❙
❚
theory LeftRegular : ?FOLEQNatDed =
include ?Band ❙
leftregular: {x,z} ⊦ z∘x∘z ≐ z∘x ❙
❚
theory RightNormal : ?FOLEQNatDed =
include ?Band ❙
rightregular1: {x,y,z} ⊦ x∘z∘y∘z ≐ x∘y∘z ❙
❚
theory RightRegular : ?FOLEQNatDed =
include ?Band ❙
rightregular: {y,z} ⊦ z∘y∘z ≐ y∘z ❙
❚
/T views for the three stages of regular band theories ❚
implicit view Regular2LeftNormal : ?Regular -> ?LeftNormal =
include ?Band❙
regular = [x,y,z] congT leftregular1 [u]u∘z❙
❚
implicit view LeftNormal2LeftRegular : ?LeftNormal -> ?LeftRegular =
include ?Band❙
leftregular1 = [x,y,z] congT leftregular [u]u∘y❙
❚
implicit view Regular2RightNormal : ?Regular -> ?RightNormal =
include ?Band❙
regular = [x,y,z] trans3 assoc5 (congT (trans3 assoc4R rightregular1 assoc) [u]z∘u) assoc4R❙
❚
implicit view RightNormal2RightRegular : ?RightNormal -> ?RightRegular =
include ?Band❙
rightregular1 = [x,y,z] trans3 assoc4 (congT (trans assocR rightregular) [u] x∘u) assocR❙
❚
/T normal bands ❚
theory Normal : ?FOLEQNatDed =
include ?Band ❙
normal: {x,y,z} ⊦ z∘(x∘y)∘z ≐ z∘(y∘x)∘z ❙
❚
theory RightCommutative : ?FOLEQNatDed =
include ?Band ❙
leftnormal: {x,y,z} ⊦ z∘(x∘y) ≐ z∘(y∘x) ❙
❚
theory LeftCommutative : ?FOLEQNatDed =
include ?Band ❙
rightnormal: {x,y,z} ⊦ (x∘y)∘z ≐ (y∘x)∘z ❙
❚
/T views for the diamond of normal band theories (with semilattices at the bottom) ❚
implicit view Normal2RightCommutative : ?Normal -> ?RightCommutative =
include ?Band❙
normal = [x,y,z] congT leftnormal [u]u∘z❙
❚
implicit view Normal2LeftCommutative : ?Normal -> ?LeftCommutative =
include ?Band❙
normal = [x,y,z] trans3 assoc (congT rightnormal [u]z∘u) assocR❙
❚
view RightCommutative2Semilattice : ?RightCommutative -> ?Semilattice =
include ?Band❙
leftnormal = [x,y,z] congT comm [u]z∘u❙
❚
implicit view LeftCommutative2Semilattice : ?LeftCommutative -> ?Semilattice =
include ?Band❙
rightnormal = [x,y,z] congT comm [u]u∘z❙
❚
/T views from regular to normal band theories ❚
implicit view LeftNormal2Normal : ?LeftNormal -> ?Normal =
include ?Band❙
// zxzy = zxzyzxzy = zx yz zxzy = zxy zx zy = zxy xz zy = zxy zxy = zxy❙
leftregular1 = [x,y,z] trans3 (sym idempotent) _ idempotent❙
❚
implicit view LeftRegular2RightCommutative : ?LeftRegular -> ?RightCommutative =
include ?Band❙
leftregular = [x,z] trans4 assoc leftnormal assocR (congT idempotent [u]u∘x)❙
❚
implicit view RightNormal2Normal : ?RightNormal -> ?Normal =
include ?Band❙
// xzyz = xzyz xzyz = x yz zxzyz = xy zxzyz = xyz zx yz = xyz xyz = xyz❙
rightregular1 = [x,y,z] trans3 (sym idempotent) _ idempotent❙
❚
implicit view RightRegular2LeftCommutative : ?RightRegular -> ?LeftCommutative =
include ?Band❙
rightregular = [y,z] trans3 rightnormal assoc (congT idempotent [u]y∘u)❙
❚
/T rectangular bands (the axioms here already imply idempotency)❚
theory Rectangular : ?FOLEQNatDed =
include ?Band ❙
rectangular: {x,y} ⊦ x∘y∘x ≐ x ❙
// provable ❙
rectangularAny: {x,y,z} ⊦ x∘y∘z ≐ x∘z❙
❚
theory LeftZero : ?FOLEQNatDed =
include ?Band ❙
leftsingular: {x,y} ⊦ x∘y ≐ x ❙
❚
theory RightZero : ?FOLEQNatDed =
include ?Band ❙
rightsingular: {x,y} ⊦ x∘y ≐ y ❙
❚