----- Path 1: -----
        Main goal to prove:
(GOAL)  ( aīnat) ( bīnat) ( cīnat) ((a | b) & (a | c) => (a | (b + c)))
I      To show (GOAL) it suffices to show (SG1) for a new constant:
        Let constant 'a' be arbitrary, but fixed.
(SG1)   ( bīnat) ( cīnat) ((a | b) & (a | c) => (a | (b + c)))
I      To show (SG1) it suffices to show (SG2) for a new constant:
        Let constant 'b' be arbitrary, but fixed.
(SG2)   ( cīnat) ((a | b) & (a | c) => (a | (b + c)))
I      To show (SG2) it suffices to show (SG3) for a new constant:
        Let constant 'c' be arbitrary, but fixed.
(SG3)   (a | b) & (a | c) => (a | (b + c))
=>I     To show (SG3) it suffices to show (SG4) assuming (ASS1):
(ASS1)  (a | b) & (a | c)
&E1     By (ASS1) we know (KN1):
(KN1)   a | b
RDef    By (KN1) and by relation definition 'div' we know (KN2):
(KN2)   (EX qīnat) (a * q = b)
EXE     By (KN2) we may assume (KN3) for a new constant:
        Let constant 'q_b' be such that
(KN3)   a * q_b = b
&E2     By (ASS1) we know (KN4):
(KN4)   a | c
RDef    By (KN4) and by relation definition 'div' we know (KN5):
(KN5)   (EX qīnat) (a * q = c)
EXE     By (KN5) we may assume (KN6) for a new constant:
        Let constant 'q_c' be such that
(KN6)   a * q_c = c
(SG4)   a | (b + c)
RDef    By (SG4) and by relation definition 'div' we have to show (SG5):
(SG5)   (EX qīnat) (a * q = b + c)
EXI     To show (SG5) it suffices to show (SG6):
        Substitute variable 'q' for term 'q_b+q_c':
(SG6)   a * (q_b + q_c) = b + c
RRApp   By (SG6) and by rewrite rule 'distr' we have to show (SG7):
(SG7)   a * q_b + a * q_c = b + c
=Sub    By (SG7) and by (KN6) we have to show (SG8):
(SG8)   a * q_b + a * q_c = b + a * q_c
=Sub    By (SG8) and by (KN3) we have to show (SG9):
(SG9)   a * q_b + a * q_c = a * q_b + a * q_c
=Id     By (SG9) the path is complete.
(SG10)  <nothing>
----- End of proof-tree -----