----- 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)
----- End of proof-tree -----