life.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Definition blinker := [[0;0;0;0;0];
                       [0;0;0;0;0];
                       [0;1;1;1;0];
                       [0;0;0;0;0];
                       [0;0;0;0;0]].
Compute take 3 (iter conway_life blinker).= [[[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
   [0; 1; 1; 1; 0]; [0; 0; 0; 0; 0];
   [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 1; 0; 0];
  [0; 0; 1; 0; 0]; [0; 0; 1; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 1; 1; 1; 0]; [0; 0; 0; 0; 0];
  [0; 0; 0; 0; 0]]]
: list (list (list bool))

Definition bipole := [[1;1;0;0;0];
                      [1;0;0;0;0];
                      [0;1;0;1;0];
                      [0;0;0;0;1];
                      [0;0;0;1;1]].
Compute take 3 (iter conway_life bipole).= [[[1; 1; 0; 0; 0]; [1; 0; 0; 0; 0];
   [0; 1; 0; 1; 0]; [0; 0; 0; 0; 1];
   [0; 0; 0; 1; 1]];
  [[1; 1; 0; 0; 0]; [1; 0; 1; 0; 0];
  [0; 0; 0; 0; 0]; [0; 0; 1; 0; 1];
  [0; 0; 0; 1; 1]];
  [[1; 1; 0; 0; 0]; [1; 0; 0; 0; 0];
  [0; 1; 0; 1; 0]; [0; 0; 0; 0; 1];
  [0; 0; 0; 1; 1]]]
: list (list (list bool))

Definition glider := [[0;1;0;0;0];
                      [0;0;1;0;0];
                      [1;1;1;0;0];
                      [0;0;0;0;0];
                      [0;0;0;0;0]].
Compute take 9 (iter conway_life glider).= [[[0; 1; 0; 0; 0]; [0; 0; 1; 0; 0];
   [1; 1; 1; 0; 0]; [0; 0; 0; 0; 0];
   [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [1; 0; 1; 0; 0];
  [0; 1; 1; 0; 0]; [0; 1; 0; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 1; 0; 0];
  [1; 0; 1; 0; 0]; [0; 1; 1; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 1; 0; 0; 0];
  [0; 0; 1; 1; 0]; [0; 1; 1; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 1; 0; 0];
  [0; 0; 0; 1; 0]; [0; 1; 1; 1; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 1; 0; 1; 0]; [0; 0; 1; 1; 0];
  [0; 0; 1; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 0; 0; 1; 0]; [0; 1; 0; 1; 0];
  [0; 0; 1; 1; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 0; 1; 0; 0]; [0; 0; 0; 1; 1];
  [0; 0; 1; 1; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 0; 0; 1; 0]; [0; 0; 0; 0; 1];
  [0; 0; 1; 1; 1]]]
: list (list (list bool))