Many implications among properties of loops are built directly into LOOPS. A sizeable portion of these properties are of trivial character or are based on definitions (e.g., alternative loops = left alternative loops + right alternative loops). The remaining implications are theorems.
All filters of LOOPS are summarized below, using the GAP convention that the property on the left is implied by the property (properties) on the right.
( IsExtraLoop, IsAssociative and IsLoop )
( IsExtraLoop, IsCodeLoop )
( IsCCLoop, IsCodeLoop )
( HasTwosidedInverses, IsPowerAssociative and IsLoop )
( IsPowerAlternative, IsDiassociative )
( IsFlexible, IsDiassociative )
( HasAntiautomorphicInverseProperty, HasAutomorphicInverseProperty and IsCommutative )
( HasAutomorphicInverseProperty, HasAntiautomorphicInverseProperty and IsCommutative )
( HasLeftInverseProperty, HasInverseProperty )
( HasRightInverseProperty, HasInverseProperty )
( HasWeakInverseProperty, HasInverseProperty )
( HasAntiautomorphicInverseProperty, HasInverseProperty )
( HasTwosidedInverses, HasAntiautomorphicInverseProperty )
( HasInverseProperty, HasLeftInverseProperty and IsCommutative )
( HasInverseProperty, HasRightInverseProperty and IsCommutative )
( HasInverseProperty, HasLeftInverseProperty and HasRightInverseProperty )
( HasInverseProperty, HasLeftInverseProperty and HasWeakInverseProperty )
( HasInverseProperty, HasRightInverseProperty and HasWeakInverseProperty )
( HasInverseProperty, HasLeftInverseProperty and HasAntiautomorphicInverseProperty )
( HasInverseProperty, HasRightInverseProperty and HasAntiautomorphicInverseProperty )
( HasInverseProperty, HasWeakInverseProperty and HasAntiautomorphicInverseProperty )
( HasTwosidedInverses, HasLeftInverseProperty )
( HasTwosidedInverses, HasRightInverseProperty )
( HasTwosidedInverses, IsFlexible and IsLoop )
( IsMoufangLoop, IsExtraLoop )
( IsCLoop, IsExtraLoop )
( IsExtraLoop, IsMoufangLoop and IsLeftNuclearSquareLoop )
( IsExtraLoop, IsMoufangLoop and IsMiddleNuclearSquareLoop )
( IsExtraLoop, IsMoufangLoop and IsRightNuclearSquareLoop )
( IsLeftBolLoop, IsMoufangLoop )
( IsRightBolLoop, IsMoufangLoop )
( IsDiassociative, IsMoufangLoop )
( IsMoufangLoop, IsLeftBolLoop and IsRightBolLoop )
( IsLCLoop, IsCLoop )
( IsRCLoop, IsCLoop )
( IsDiassociative, IsCLoop and IsFlexible)
( IsCLoop, IsLCLoop and IsRCLoop )
( IsRightBolLoop, IsLeftBolLoop and IsCommutative )
( IsLeftPowerAlternative, IsLeftBolLoop )
( IsLeftBolLoop, IsRightBolLoop and IsCommutative )
( IsRightPowerAlternative, IsRightBolLoop )
( IsLeftPowerAlternative, IsLCLoop )
( IsLeftNuclearSquareLoop, IsLCLoop )
( IsMiddleNuclearSquareLoop, IsLCLoop )
( IsRCLoop, IsLCLoop and IsCommutative )
( IsRightPowerAlternative, IsRCLoop )
( IsRightNuclearSquareLoop, IsRCLoop )
( IsMiddleNuclearSquareLoop, IsRCLoop )
( IsLCLoop, IsRCLoop and IsCommutative )
( IsRightNuclearSquareLoop, IsLeftNuclearSquareLoop and IsCommutative )
( IsLeftNuclearSquareLoop, IsRightNuclearSquareLoop and IsCommutative )
( IsLeftNuclearSquareLoop, IsNuclearSquareLoop )
( IsRightNuclearSquareLoop, IsNuclearSquareLoop )
( IsMiddleNuclearSquareLoop, IsNuclearSquareLoop )
( IsNuclearSquareLoop, IsLeftNuclearSquareLoop and IsRightNuclearSquareLoop
and IsMiddleNuclearSquareLoop )
( IsFlexible, IsCommutative )
( IsRightAlternative, IsLeftAlternative and IsCommutative )
( IsLeftAlternative, IsRightAlternative and IsCommutative )
( IsLeftAlternative, IsAlternative )
( IsRightAlternative, IsAlternative )
( IsAlternative, IsLeftAlternative and IsRightAlternative )
( IsLeftAlternative, IsLeftPowerAlternative )
( HasLeftInverseProperty, IsLeftPowerAlternative )
( IsPowerAssociative, IsLeftPowerAlternative )
( IsRightAlternative, IsRightPowerAlternative )
( HasRightInverseProperty, IsRightPowerAlternative )
( IsPowerAssociative, IsRightPowerAlternative )
( IsLeftPowerAlternative, IsPowerAlternative )
( IsRightPowerAlternative, IsPowerAlternative )
( IsAssociative, IsLCCLoop and IsCommutative )
( IsExtraLoop, IsLCCLoop and IsMoufangLoop )
( IsAssociative, IsRCCLoop and IsCommutative )
( IsExtraLoop, IsRCCLoop and IsMoufangLoop )
( IsLCCLoop, IsCCLoop )
( IsRCCLoop, IsCCLoop )
( IsCCLoop, IsLCCLoop and IsRCCLoop )
( IsOsbornLoop, IsMoufangLoop )
( IsOsbornLoop, IsCCLoop )
( HasAutomorphicInverseProperty, IsLeftBruckLoop )
( IsLeftBolLoop, IsLeftBruckLoop )
( IsRightBruckLoop, IsLeftBruckLoop and IsCommutative )
( IsLeftBruckLoop, IsLeftBolLoop and HasAutomorphicInverseProperty )
( HasAutomorphicInverseProperty, IsRightBruckLoop )
( IsRightBolLoop, IsRightBruckLoop )
( IsLeftBruckLoop, IsRightBruckLoop and IsCommutative )
( IsRightBruckLoop, IsRightBolLoop and HasAutomorphicInverseProperty )
( IsCommutative, IsSteinerLoop )
( IsCLoop, IsSteinerLoop )
( IsLeftAutomorphicLoop, IsAutomorphicLoop )
( IsRightAutomorphicLoop, IsAutomorphicLoop )
( IsMiddleAutomorphicLoop, IsAutomorphicLoop )
( IsLeftAutomorphicLoop, IsRightAutomorphicLoop and HasAntiautomorphicInverseProperty )
( IsRightAutomorphicLoop, IsLeftAutomorphicLoop and HasAntiautomorphicInverseProperty )
( IsFlexible, IsMiddleAutomorphicLoop )
( HasAntiautomorphicInverseProperty, IsFlexible and IsLeftAutomorphicLoop )
( HasAntiautomorphicInverseProperty, IsFlexible and IsRightAutomorphicLoop )
( IsMoufangLoop, IsAutomorphicLoop and IsLeftAlternative )
( IsMoufangLoop, IsAutomorphicLoop and IsRightAlternative )
( IsMoufangLoop, IsAutomorphicLoop and HasLeftInverseProperty )
( IsMoufangLoop, IsAutomorphicLoop and HasRightInverseProperty )
( IsMoufangLoop, IsAutomorphicLoop and HasWeakInverseProperty )
( IsMiddleAutomorphicLoop, IsCommutative )
( IsLeftAutomorphicLoop, IsLeftBruckLoop )
( IsLeftAutomorphicLoop, IsLCCLoop )
( IsRightAutomorphicLoop, IsRightBruckLoop )
( IsRightAutomorphicLoop, IsRCCLoop )
( IsAutomorphicLoop, IsCommutative and IsMoufangLoop )
( IsAutomorphicLoop, IsLeftAutomorphicLoop and IsMiddleAutomorphicLoop )
( IsAutomorphicLoop, IsRightAutomorphicLoop and IsMiddleAutomorphicLoop )
( IsAutomorphicLoop, IsAssociative )
generated by GAPDoc2HTML