Commit b4e33143 by Florian Rabe

### no message

parent e01ca943
 ... ... @@ -41,12 +41,12 @@ implicit view LeftRegular12LeftRegular : ?LeftRegular1 -> ?LeftRegular = implicit view Regular2RightRegular1 : ?Regular -> ?RightRegular1 = include ?Band = ?Band❙ regular = [x,y,z] congT ([u] z∘u) rightregular1❙ regular = [x,y,z] trans3 assoc5 (congT ([u] z∘u) trans3 assoc4R rightregular1 assoc) assoc4R❙ ❚ implicit view RightRegular12RightRegular : ?RightRegular1 -> ?RightRegular = include ?Band = ?Band❙ rightregular1 = [x,y,z] congT ([u] x∘u) rightregular❙ rightregular1 = [x,y,z] trans3 assoc4 (congT ([u] x∘u) trans assocR rightregular) assocR❙ ❚ /T normal bands ❚ ... ... @@ -75,7 +75,7 @@ implicit view Normal2LeftNormal : ?Normal -> ?LeftNormal = implicit view Normal2RightNormal : ?Normal -> ?RightNormal = include ?Band = ?Band❙ normal = [x,y,z] congT ([u] z∘u) rightnormal❙ normal = [x,y,z] trans3 assoc (congT ([u] z∘u) rightnormal) assocR❙ ❚ implicit view LeftNormal2Semilattice : ?LeftNormal -> ?Semilattice = ... ...
 ... ... @@ -32,4 +32,9 @@ theory FOLEQNatDed : http://cds.omdoc.org/urtheories?LF = congF : {x,y}{F: term ⟶ prop} ⊦ x ≐ y ⟶ ⊦ (F x) ⟶ ⊦ (F y)❘# congF 3 4 5❙ sym : {x,y} ⊦ x ≐ y ⟶ ⊦ y ≐ x❙ trans : {x,y,z} ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ x ≐ z❙ trans3 : {w,x,y,z} ⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ w ≐ z❘ = [w,x,y,z,p,q,r] trans (trans p q) r❙ trans4 : {v,w,x,y,z} ⊦ v ≐ w ⟶⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ v ≐ z❘ = [v,w,x,y,z,p,q,r,s] trans3 (trans p q) r s❙ ❚ \ No newline at end of file
 ... ... @@ -7,6 +7,16 @@ theory Magma : ?FOLEQNatDed = theory Semigroup : ?FOLEQNatDed = include ?Magma❙ assoc: {x,y,z} ⊦ (x∘y)∘z ≐ x∘(y∘z)❙ assocR: {x,y,z} ⊦ x∘(y∘z) ≐ (x∘y)∘z❘ = [x,y,z] sym assoc❙ assoc4: {w,x,y,z} ⊦ ((w∘x)∘y)∘z ≐ w∘(x∘(y∘z))❘ = [w,x,y,z] trans3 (congT ([u]u∘z) assoc) assoc (congT ([u]w∘u) assoc)❙ 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 ([u]u∘z) assoc4) assoc (congT ([u]v∘u) assoc4)❙ ❚ 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!