namespace http://mathhub.info/MitM/core/algebra ❚
import base http://mathhub.info/MitM/Foundation ❚

theory IdempotentMagma : base:?Logic = 
	include ?OperationProps ❙
	include ☞base:?InformalProofs ❙
	include ?Magma ❙
		
	theory idempotent_theory : base:?Logic =
		include ?Magma/magma_theory ❙
		axiom_idempotent : ⊦ prop_idempotent op ❙
  ❚
  idempotentMagma = Mod ☞?IdempotentMagma/idempotent_theory ❘ role abbreviation ❙
❚

namespace http://mathhub.info/MitM/core/algebra/bands ❚

theory Band : base:?Logic = 
  include ☞../algebra?IdempotentMagma❙
  include ☞../algebra?SemiGroup ❙
  
  theory band_theory : base:?Logic = 
     include ☞../algebra?IdempotentMagma/idempotent_theory ❙
     include ☞../algebra?SemiGroup/semigroup_theory ❙
  ❚
  band = Mod ☞?Band/band_theory ❘ role abbreviation❙
❚

theory Regular : base:?Logic =
	include ?Band ❙
	
	theory regular_theory : base:?Logic =
		include ?Band/band_theory ❙
		axiom_regular : ⊦ ∀[x]∀[y]∀[z] 
			z ∘ x ∘ z ∘ y ∘ z ≐ z ∘ x ∘ y ∘ z ❙
	❚
❚

theory LeftNormal : base:?Logic =
	include ?Regular ❙
	
	theory leftnormal_theory : base:?Logic =
		include ?Band/band_theory ❙
		axiom_leftnormal : ⊦ ∀[x]∀[y]∀[z] 
			z ∘ x ∘ z ∘ y ≐ z ∘ x ∘ y ❙ 
	❚
	implicit view Reg2LeftNormal : ?Regular/regular_theory -> ?LeftNormal/leftnormal_theory =
		include ?Band/band_theory ❙
		axiom_regular = sketch "trivial" ❙
	❚
❚

theory RightNormal : base:?Logic =
	include ?Regular ❙
	
	theory rightnormal_theory : base:?Logic =
		include ?Band/band_theory ❙
		axiom_rightnormal : ⊦ ∀[x]∀[y]∀[z] 
			y ∘ z ∘ x ∘ z ≐ y ∘ x ∘ z ❙
	❚
	implicit view Reg2RightNormal : ?Regular/regular_theory -> ?RightNormal/rightnormal_theory =
		include ?Band/band_theory ❙
	    axiom_regular = sketch "trivial" ❙
    ❚
❚

theory Normal : base:?Logic =

	include ?LeftNormal ❙
	include ?RightNormal ❙
	
	theory normal_theory : base:?Logic =
		include ?Band/band_theory ❙
		axiom_normal :  ⊦ ∀[x]∀[y]∀[z] 
			z ∘ x ∘ y ∘ z ≐ z ∘ y ∘ x ∘ z ❙
	❚
	implicit view LeftNormal2Normal : ?LeftNormal/leftnormal_theory -> ?Normal/normal_theory =
		include ?Band/band_theory ❙
		axiom_leftnormal = sketch "trivial" ❙
	❚

	 implicit view RightNormal2Normal : ?RightNormal/rightnormal_theory -> ?Normal/normal_theory =
		include ?Band/band_theory ❙
	 	axiom_rightnormal = sketch "trivial" ❙
    ❚
❚