noNamespace
element CP

Documentation

A proofline that includes a conditional proof. This is a usage of the deduction theorem. If the hypothesis formulas are H1, H2 and H3 and the last proof is A the proved formula is H1 & H2 & H3 -> A
      Can be used with rule version 0.02.00.
      

Properties

This component is not nillable.

Model

<CP>
(HYPOTHESIS, LINES, CONCLUSION )
</CP>

Source

<xs:element name="CP" substitutionGroup="LINETYPE">
  <xs:complexType>
    <xs:sequence>
      <xs:element maxOccurs="unbounded" minOccurs="1" name="HYPOTHESIS">
        <xs:complexType>
          <xs:sequence>
            <xs:element maxOccurs="1" minOccurs="0" ref="FORMULA">
            </xs:element>
          </xs:sequence>
          <xs:attribute name="label" type="xs:NMTOKEN">
          </xs:attribute>
        </xs:complexType>
      </xs:element>
      <xs:element maxOccurs="1" minOccurs="1" ref="LINES">
      </xs:element>
      <xs:element maxOccurs="1" minOccurs="1" name="CONCLUSION">
        <xs:complexType>
          <xs:sequence>
            <xs:element maxOccurs="1" minOccurs="0" ref="FORMULA">
            </xs:element>
          </xs:sequence>
          <xs:attribute name="label" type="xs:NMTOKEN">
          </xs:attribute>
        </xs:complexType>
      </xs:element>
    </xs:sequence>
  </xs:complexType>
</xs:element>