TranspositionModule

The transpositions of the strict rules (module transposition), with autoTransposition: for a strict rule r : a, b -> c, the rules concluding a contradictory of each premise from a contradictory of the conclusion and the other premises (r_i : -c, b -> -a, r_ii : -c, a -> -b). The contradictories of a statement are its negation, and the statements the theory declares in conflict with it both ways, with no guard (conflict([c], [d]) and conflict([d], [c])): the transpositions through those are named transposed(Id, ConclusionContradictory, PremiseContradictory), Id the name of the one through negations.