• if the positive integer is a member of the other list,
• then there exist a quantity, the quantityMINUSONE,, , another positive integer and a third positive integer such that the quantity is greater than 1 and the quantity is less than or equal to length of the other list and the positive integerth element of the other list is equal to the quantity and the other positive integer is a member of the list and the quantity is equal to the other positive integerth element of the list and the third positive integer is a member of the other list and the quantityMINUSONE is equal to (the quantity and 1) and the quantityMINUSONE is equal to the third positive integerth element of the other list and the positive integer is equal to (the other positive integer and the third positive integer)

• if the listITEM is a member of the list,
• then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string

• if the listITEM is a member of the list,
• then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string

• if the listITEM is a member of the list,
• then the listITEM is an instance of a symbolic string and there doesn't exist another entity such that the other entity is an instance of the symbolic string and the other entity is not a member of the list and the other integer is equal to the number of instances in the class described by the symbolic string

• If a cognitive agent is a performer on an album,
• then there exist a content bearing object and a process such that the content bearing object is an instance of recording and the content bearing object is a member of the album and the content bearing object is a record of the process and the cognitive agent is an agent of the process

• If a kind of DataStorageDevice is equal to the set of copies on a kind of DataStorageDeviceS of an album and an entity is an instance of the kind of DataStorageDevice,
• then for all an object
  • if the object is a member of the album,
  • then there exists a content bearing object such that the content bearing object is a copy of the object and the content bearing object is stored on the kind of DataStorageDevice

• If a relational attribute is an instance of recording attribute and an album is a the relational attribute,
• then for all an object
  • if the object is a member of a list,
  • then the album is an attribute of the object

• If an object is an instance of DigitalDataStorageDevice and a symbolic string is a part of the object and the symbolic string is an instance of digital data,
• then there exist a CodeMap and a list such that the symbolic string in the CodeMap denotes an entity and the list expresses the CodeMap and
  • if the entity is a member of the list,
  • then the entity is an instance of binary number

• If a real number is an average of a list,
• then for all the listITEM
  • if the listITEM is a member of the list,
  • then the listITEM is an instance of real number

( ! [V__ROW2,V__ELEMENT] :
   (s__instance(V__ROW2,s__Attribute)s__=>(s__contraryAttribute__1(V__ROW2)
    s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW3,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__2(V__ROW2,V__ROW3)
    s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

• If @ROW is the opposite of ,
• then
  • if another entity is a member of (@ROW),
  • then the other entity is an instance of attribute

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

• If a class is disjointly decomposed into @ROW,
• then for all a set or class
  • if the set or class is a member of (@ROW),
  • then the set or class is a subclass of the class

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__and__ms__inList(V__ITEM2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__1Fn(V__ROW2))
        s__and__ms__inList(V__ITEM2,s__ListFn__1Fn(V__ROW2))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__and__ms__inList(V__ITEM2,s__ListFn__2Fn(V__ROW2,V__ROW3))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__and__ms__inList(V__ITEM2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__and__ms__inList(V__ITEM2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

• If a class is disjointly decomposed into @ROW,
• then for all a set or class and another set or class
  • if the set or class is a member of (@ROW) and the other set or class is a member of (@ROW) and the set or class is not equal to the other set or class,
  • then the set or class is disjoint from the other set or class

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__2(V__ROW2,V__ROW3)
    s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW8,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW2,V__ELEMENT] :
   (s__instance(V__ROW2,s__Class)s__=>(s__disjointDecomposition__1(V__ROW2)
    s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

• If @ROW is disjointly decomposed into @ROW,
• then
  • if another entity is a member of (@ROW),
  • then the other entity is an instance of class

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

• If the greatest common divisor of @ROW is equal to an integer,
• then
  • if another entity is a member of (@ROW),
  • then the other entity is an instance of number

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

• If the greatest common divisor of @ROW is equal to an integer,
• then for all another integer
  • if the other integer is a member of (@ROW),
  • then the other integer mod the integer is equal to 0

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

• If the greatest common divisor of @ROW is equal to an integer,
• then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer
  • if the third integer is a member of (@ROW),
  • then the third integer mod the other integer is equal to 0

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

• If the least common multiple of @ROW is equal to an integer,
• then
  • if another entity is a member of (@ROW),
  • then the other entity is an instance of number

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

• If the least common multiple of @ROW is equal to an integer,
• then for all another integer
  • if the other integer is a member of (@ROW),
  • then the integer mod the other integer is equal to 0

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

• If the least common multiple of @ROW is equal to an integer,
• then there doesn't exist another integer such that the other integer is less than the integer and for all a third integer
  • if the third integer is a member of (@ROW),
  • then the other integer mod the third integer is equal to 0

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ATTR,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ATTR,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ATTR,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
    s__=>(s__inList(V__ATTR,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__inList(V__ATTR,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

• If @ROW are all the attributes of another kind of attribute,
• then
  • if an entity is a member of (@ROW),
  • then the entity is an instance of attribute

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

• If @ROW are all the attributes of another kind of attribute,
• then for all an entity
  • if the entity is an instance of another kind of attribute,
  • then there exists another entity such that the other entity is a member of (@ROW) and the entity is equal to the other entity

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

• If a class is covered by @ROW,
• then for all an entity
  • if the entity is an instance of the class,
  • then there exists a set or class such that the set or class is a member of (@ROW) and the entity is an instance of the set or class

( ! [V__ROW2,V__ELEMENT] :
   (s__instance(V__ROW2,s__Class)s__=>(s__exhaustiveDecomposition__1(V__ROW2)
    s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW8,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__2(V__ROW2,V__ROW3)
    s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

• If @ROW is covered by @ROW,
• then
  • if another entity is a member of (@ROW),
  • then the other entity is an instance of class

• If a list is an instance of album,
• then for all an entity
  • if the entity is a member of the list,
  • then the entity is an instance of recording

• If a process is an instance of shuttle,
• then there exist a list, an object and an agent such that the agent is an agent of the process and the agent possesses the object and the object is an instance of automobile and the list is an instance of list and for all an entity
  • if the entity is a member of the list,
  • then the entity is an instance of PostalPlace and there exists another process such that the other process is an instance of transportation and the agent is an agent of the other process and the object is an instrument for the other process and the other process ends up at the entity