Formulas and proofs syntax

Logical connectives
 & conjunction + disjunction
 => implication <=> equivalence
 - negation
 F false
A proof is a sequence of proof lines.
A proof line is either a formula, the word assume followed by a formula, or the word therefore followed by a formula.
This formula is the conclusion of the proof line. Each proof line is terminated by a period.
The word assume introduces an hypothesis.
The word therefore removed the last introduced hypothesis.
A formula is usable on a proof line, if it is the conclusion of a previous proof line whose hypotheses have not been removed.
Proof Line        Effects Conditions
assume A. adds A to the end of the list of the hypothesis of the previous proof line no conditions
therefore A => B. removes the last introduced hypothesis. This proof line is the application of the rule =>I The removed hypothesis must be A.
The formula B must be usable on the previous proof line.
A. no effects The formula A must be a copy of a formula usable on this proof line or must be obtained by application of a rule to formulas usable on this line.
Operator priority : (high) - & + => <=> (low)
Between two identical operations, the left operation is prioritary, except for implication

 A & B & C est (A & B)& C A + B + C est (A + B) + C A => B => C est A => (B => C)
 A & B + C est (A & B) + C A & B => C + D est (A & B) => (C + D) - A + B est (- A) + B