% Below we show various distributivity properties and properties about negation
% We give in the comments the justification for each step. These justifications
% are not needed when you write your own proofs.
% Convention: Hi are hypotheses, Ci are conclusions.

% Note: (A | B | C) is implicitly parenthesized by tutch as (A | (B | C))
% Similarly for A & B & C.

proof implAndDsitrib : ((A => D) & (B => D) & (C => D)) => ((A | B | C) => D) =
begin
  % Assume (A => D) & (B => D) & (C => D), derive (A | B | C) => D
  [ (A => D) & (B => D) & (C => D);                       % H1
    A => D;                                               % C1: &E1 on H1

    (B => D) & (C => D);                                  % C2: &E2 on H1
    B => D;                                               % C3: &E1 on C2
    C => D;                                               % C4: &E2 on C2

    % Assume (A | B | C), derive D.
    [ A | B | C;                                          % H2

      % We're going to use |E on A | B | C = A | (B | C)
      % Branch A
      [ A;                                                % H3
	D ];                                              % C5: =>E on C1 and H3

      % Branch B | C
      [ B | C;                                            % H4
	% | eliminate this too

	% Branch B
	[ B;                                              % H5
	  D ];                                            % C6: =>E on C3 and H5

	% Branch C
	[ C;                                              % H6
	  D ];                                            % C7: =>E on C4 and H6

	D ];                                              % C8: |E on H4, H5..C6, and H6..C7

      D ];                                                % C9: |E on H2, H3..C5, and H4..C8
    (A | B | C) => D ];                                   % C10: =>I on H2..C9
 ((A => D) & (B => D) & (C => D)) => ((A | B | C) => D);  % C11: =>I on H1..C10
end;

proof implOrDistrib : ((A | B | C) => D) => ((A => D) & (B => D) & (C => D)) =
begin
  [ (A | B | C) => D;                                     % H1

    [ A;                                                  % H2
      A | B | C;                                          % C1: |I1 on H2
      D; ];                                               % C2: =>E on H1 and C1
    A => D;                                               % C3: =>I on H2..C2

    [ B;                                                  % H3
      B | C;                                              % C4: |I1 on H3
      A | B | C;                                          % C5: |I2 on C4
      D ];                                                % C6: =>E on H1 and C5
    B => D;                                               % C7: =>I on H3..C6

    [ C;                                                  % H4
      B | C;                                              % C8: |I2 on H4
      A | B | C;                                          % C9: |I2 on C8
      D ];                                                % C10: =>E on H1 and C9
    C => D;                                               % C11: =>I on H4..C10

    (B => D) & (C => D);                                  % C12: &I on C7 and C11

    (A => D) & (B => D) & (C => D) ];                     % C13: =>I on C3 and C12

  ((A | B | C) => D) => ((A => D) & (B => D) & (C => D)); % C14: =>I on H1..C13
end;

proof diagAndProj : (A => (A & A)) & ((A & A) => A) =
begin
  [ A;                                                    % H1
    A & A ];                                              % C1: &I on H1 and H1
  A => (A & A);                                           % C2: =>I on H1..C1

  [ A & A;                                                % H2
    A ];                                                  % C3: &E1 on H2
  (A & A) => A;                                           % C4: =>I on H2..C3

  (A => (A & A)) & ((A & A) => A);                        % &I on C2 and C4
end;

proof doubleNeg : ~~(A | ~A) =
begin
  [ ~(A | ~A);                                            % H1
    [ A;                                                  % H2
      A | ~A;                                             % C1: |I1 on H2
      F ];                                                % C2: =>E on H1 and C1
    ~A;                                                   % C3: ~I on H2..C2
    A | ~A;                                               % C4: |I2 on C3
    F ];                                                  % C5: =>E on H1 and C4
  ~~(A | ~A);                                             % C7: ~I on H1..C5
end;

proof tripleNegSimpl : ~~~A => ~A =
begin
  [ ~~~A;                                                 % H1
    [ A;                                                  % H2
      [ ~A;                                               % H3
	 F ];                                             % C1: =>E on H3 and H2
      ~~A;                                                % C2: ~I on H3..C1
      F ];                                                % C3: =>E on H1 and C2
    ~A ];                                                 % C4: ~I on H2..C3
  ~~~A => ~A;                                             % C5: =>I on H1..C4
end;