environ
    A1: P[] implies Q[];
    A2: P[] or not R[];
    A3: not R[] implies S[];
begin
                == At this point A1, A2, A3 are all visible
    1: now
                == At this point A1, A2, A3 are all visible, but 1 is not,
                == as the statement it labels is not completed yet.
                == 2, 3 are not visible because they follow this point
          assume 2: not P[];
                 3: not R[] by A2, 2;
                == At this point, 2 and 3 are now visible.
          thus S[] by 3,A3;
       end;        

    not P[] implies S[] by 1;
       == At this point A1, A2, A3, and 1 are all visible.
       == 2, 3 are not because they are inside a justification.

    4: now
          assume 5: R[];
                 6: now
                       assume 7: P[];
                       thus R[] by 5;
                    end;
                 8: now
                       == A1, A2, A3, 1, 5, and 6 are visible.
                       == 7 is not because it is inside a justification.
                       == 4 is not because we are inside the `formula` it
                       == labels.
                     assume 9: not P[];
                     thus R[] by 5;
                    end;
          thus (P[] implies R[]) & (not P[] implies R[]) by 6,8;
       end;

    R[] implies (P[] implies R[]) & (not P[] implies R[]) by 4;

       == This next statement redefines A1, so the previous
       == formula referred to by A1 is no longer visible.
    A1: not R[] or R[];