Commit 9cf8728f authored by Florian Rabe's avatar Florian Rabe

no message

parent c092ceb2
......@@ -61,9 +61,6 @@ implicit view RightRegular12RightRegular : ?RightRegular1 -> ?RightRegular =
theory Normal : ?FOLEQNatDed =
include ?Band ❙
normal: {x,y,z} ⊦ z∘(x∘y)∘z ≐ z∘(y∘x)∘z ❙
lr: {x,y,z} ⊦ z∘x∘z∘y ≐ z∘(z∘x)∘y ❘= [x,y,z] trans (congT assoc [u]u∘y) normal❙
theory LeftNormal : ?FOLEQNatDed =
......@@ -88,7 +85,7 @@ implicit view Normal2RightNormal : ?Normal -> ?RightNormal =
normal = [x,y,z] trans3 assoc (congT rightnormal [u]z∘u) assocR❙
implicit view LeftNormal2Semilattice : ?LeftNormal -> ?Semilattice =
view LeftNormal2Semilattice : ?LeftNormal -> ?Semilattice =
include ?Band = ?Band❙
leftnormal = [x,y,z] congT comm [u]z∘u❙
......@@ -103,7 +100,7 @@ implicit view RightNormal2Semilattice : ?RightNormal -> ?Semilattice =
implicit view LeftRegular12Normal : ?LeftRegular1 -> ?Normal =
include ?Band = ?Band❙
// zxzy = zxzyzxzy = zx yz zxzy = zxy zx zy = zxy xz zy = zxy zxy = zxy❙
leftregular1 = [x,y,z] _
leftregular1 = [x,y,z] trans3 (sym idempotent) _ idempotent
implicit view LeftRegular2LeftNormal : ?LeftRegular -> ?LeftNormal =
......@@ -113,7 +110,8 @@ implicit view LeftRegular2LeftNormal : ?LeftRegular -> ?LeftNormal =
implicit view RightRegular12Normal : ?RightRegular1 -> ?Normal =
include ?Band = ?Band❙
rightregular1 = [x,y,z] _❙
// xzyz = xzyz xzyz = x yz zxzyz = xy zxzyz = xyz zx yz = xyz xyz = xyz❙
rightregular1 = [x,y,z] trans3 (sym idempotent) _ idempotent❙
implicit view RightRegular2RightNormal : ?RightRegular -> ?RightNormal =
......@@ -139,4 +137,4 @@ theory LeftSingular : ?FOLEQNatDed =
theory RightSingular : ?FOLEQNatDed =
include ?Band ❙
rightsingular: {x,y} ⊦ x∘y ≐ y ❙
\ No newline at end of file
......@@ -16,7 +16,8 @@ theory Semigroup : ?FOLEQNatDed =
assoc4R: {w,x,y,z} ⊦ w∘(x∘(y∘z)) ≐ ((w∘x)∘y)∘z❘
= [w,x,y,z] sym assoc4❙
assoc5: {v,w,x,y,z} ⊦ (((v∘w)∘x)∘y)∘z ≐ v∘(w∘(x∘(y∘z)))❘
= [v,w,x,y,z] trans3 (congT assoc4 [u]u∘z) assoc (congT assoc4 [u]v∘u)❙
= [v,w,x,y,z] trans4 (congT assoc4 [u]u∘z) assoc
(congT assoc [u]v∘u) (congT assoc [u]v∘(w∘u))❙
theory Commutative : ?FOLEQNatDed =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment