Gates of Gates: 16 × 16 × 16

Every one of the 16 two-input logic gates, applied to every pair of gates.

For each gate G there is a 16 × 16 square. G sits at the origin in the top-left corner, the gates run left to right as the first input X and top to bottom as the second input Y, and each cell is G(X, Y): G applied row by row to the truth tables of X and Y. The result is always one of the same 16 gates. In lambda calculus a cell is the term

λp.λq.λa.λb. G (X p q) (Y p q) a b

with the three gates' terms from lambda16.txt plugged in. That makes 16 × 16 × 16 = 4,096 cells.

Everything here is also in one self-contained document, Gates of Gates, the document: this write-up with its images, both interactive pages, lambda16.txt and the data, with nothing loaded from the internet. Its file is docs/gates-of-gates-document.html at the top of the repository; saved to disk, it works offline.

Gates are numbered 0–15 in the boolean16.py order, where gate i and gate 15 − i are complements. Truth tables are written TT TF FT FF, for (p, q) = (T,T), (T,F), (F,T), (F,F).

The 1995 poster

The hand-made 1995 gates-of-gates poster

The same idea, drawn by hand in 1995: sixteen 16 × 16 squares in a 4 × 4 layout, F in the top-left corner and T in the bottom-right. Every gate, including the input gates along the top and left edges, is drawn as a square Venn diagram on graph paper. Each colour marks a position in the square Venn, one region of the truth table, and the Venn served as both logic and data. P and ~P show vertical stripes, Q and ~Q horizontal stripes, and the complement pairs sit in mirrored positions (counting the poster's squares 0–15 row by row from the top left, which is not the gate numbering used below: P and ~P are squares 5 and 10, Q and ~Q are 9 and 6, F and T are 0 and 15, each pair adding to 15).

The poster took some liberties and probably contains mistakes, so treat it with a grain of salt. The recomputation below is checked cell by cell. Two details are still open:

Grey: on the poster the T square is solid grey. It may be that grey meant "every region TRUE".
Which colour was which region: the mapping used in the recomputation (magenta, cyan, green, dark red for p and q, p only, q only, neither) is a guess.

The recomputation (2026)

Every cell was computed by lambda reduction (16,384 reductions: 4,096 cells × 4 inputs), using the gate terms read from lambda16.txt, and each result was cross-checked against plain bitwise arithmetic on the truth tables. All 4,096 agree. Each gate's own truth table was also re-derived by reduction and matched the file.

Interactive version: Gates of Gates on the public site. Its file is page/gates-of-gates.html. It has six cell views (truth table, Venn colours, square Venn, gate number, same term, one quarter), two axis orders, hover details, and a full table for any square.

Square Venn view, 1995 style

All 16 squares drawn as square Venn diagrams with Venn headers

The AND square as a full table with square-Venn headers

Truth-table view and Venn colours

Patterns

Each of these was checked across all cells before the page was built.

FALSE and TRUE ignore their inputs: every cell is FALSE, or every cell is TRUE.
P copies X (every column is one gate) and Q copies Y (every row is one gate). NOT P gives 15 − X and NOT Q gives 15 − Y, the complement of the input.
AND, OR, XOR, XNOR, NAND and NOR are symmetric: G(X, Y) = G(Y, X), so their squares mirror across the diagonal.
On the diagonal (X = Y), AND gives back X and XOR gives FALSE.
Complement squares: the square for gate 15 − G is the square for G with every truth table flipped, cell for cell.

Nested patterns: Sierpiński and A New Kind of Science

Sorting the axes by truth-table value (the truth table read as a binary number, 0000, 0001, 0010 … 1111) turns each square into G applied bit by bit to two 4-bit numbers, and nested, self-similar patterns appear.

All 16 squares in truth-table order, shaded by value

AND gives a Sierpiński-style triangle: the empty cells are exactly the pairs whose truth tables share no TRUE row (X AND Y = 0). On the right, the same rule on 6-bit numbers 0–63, computed bitwise (not from the gates), shows the pattern continuing at larger scale.

AND in truth-table order, the Sierpiński-style triangle

XOR is built from half-size copies of itself: four 8 × 8 blocks, each of four 4 × 4 blocks, and so on.

These are the patterns Stephen Wolfram's A New Kind of Science is full of. Its elementary cellular automata compute each new cell as a logic function of three cells above it, the three-input version of these 16 gates. Rule 90, where each cell is the XOR of its two neighbours, grows the Sierpiński triangle. Rules that just copy a neighbour give plain lines, like the P and Q stripes, and rules that ignore their inputs give uniform regions, like FALSE and TRUE.

One difference: these squares are tables, one operation applied to every pair, so they can show uniform, striped or nested patterns. Wolfram's most surprising pictures, such as rule 30's apparent randomness, come from running a rule over and over, feeding each row into the next, which a table never does.

A New Kind of Science, online edition: https://www.wolframscience.com/nks/
"How Do Simple Programs Behave?" (rule 90 and its nested pattern): https://www.wolframscience.com/nks/p25--how-do-simple-programs-behave/
MathWorld, Rule 90: https://mathworld.wolfram.com/Rule90.html
MathWorld, Sierpiński Sieve (Pascal's triangle mod 2, bitwise AND, rules 60, 90 and 102): https://mathworld.wolfram.com/SierpinskiSieve.html

Four kinds of pattern

Looking across all 16 squares, every gate makes one of four kinds of pattern. Which one depends on how the gate uses its two inputs:

Pattern	Gates	Why
Blank or solid	FALSE, TRUE	the output ignores both inputs
Stripes	P, Q, NOT P, NOT Q	the output follows one input
Triangles (Sierpiński-style)	the eight gates with one or three TRUE rows: AND, OR, NAND, NOR, p∧¬q, q∧¬p, p→q, q→p	each is AND with its inputs and/or output flipped, so each square is AND's triangle reflected or inverted
Checkerboards	XOR, XNOR	the output compares the two inputs: same or different

Checkerboards: XOR and XNOR

XOR's square is the hardest to read, because its pattern is spread across the four quarters of the cells. Take one quarter (one truth-table row) at a time. X's values run in stripes down the columns and Y's values in stripes across the rows, and XOR is TRUE where a TRUE stripe crosses a FALSE one. Crossing stripes that way makes a checkerboard. In truth-table order the four quarters are checkerboards of four sizes, with squares 8, 4, 2 and 1 cells wide. The whole square is those four laid on top of each other. XNOR is the same with TRUE and FALSE swapped.

XOR's four quarters in truth-table order: checkerboards with squares 8, 4, 2 and 1 cells wide

In the default complement order the rows and columns are shuffled, so the same crossing makes an irregular plaid instead of a clean checkerboard. That is why it's hard to see there.

Two more properties set XOR and XNOR apart:

Latin squares: every row and every column contains all 16 gates exactly once, like a row of a Sudoku. No other square does this. XOR's square is the addition table of 4-bit numbers where 1 + 1 = 0.
A constant diagonal: anything XOR itself is FALSE, so XOR's diagonal is all FALSE and XNOR's all TRUE.

All of these (the Latin squares, the diagonals, the four checkerboards, and the triangle family being exactly those eight gates) are checked by tools/gates.js on every build. The triangle-family check also confirms that the other eight gates fail the same test.

One quarter at a time, all 16 squares

The same view as the page's One quarter option, for every square: each figure shows a single truth-table row of every cell, in that region's Venn colour, in truth-table order. Within one quarter the four kinds of pattern are at their simplest:

FALSE, TRUE: blank or solid.
P, Q, NOT P, NOT Q: stripes.
AND, NOR, p∧¬q, q∧¬p (one TRUE row): one block in four is lit. OR, NAND, p→q, q→p (three TRUE rows): three blocks in four.
XOR, XNOR: checkerboards.

The blocks are 8 cells wide in the TT quarter, then 4, 2 and 1. Stacking the four quarters, each at its own scale, is what builds the patterns in the full squares: AND's four block patterns stack into the Sierpiński-style triangle, and XOR's four checkerboards stack into its nested table.

One quarter, TT (p and q): blocks 8 cells wide

One quarter, TF (p only): blocks 4 cells wide

One quarter, FT (q only): blocks 2 cells wide

One quarter, FF (neither): blocks 1 cell wide

Every cell in these figures was checked while drawing: quarter k of G(X, Y) must equal G applied to row k of X and row k of Y.

The 506 programs

Each cell is itself a lambda term. Reducing all 4,096 cell terms gives 506 different normal forms, and each one behaves exactly like one of the 16 gates:

Level	How many
Cell terms as written	4,096
Normal forms (different programs)	506
Behaviours (the gates)	16

For each gate, exactly one program is its term in lambda16.txt. 2,064 cells reduce to one of those; the other 2,032 reduce to a longer program with the same truth table. Terms that are the same program are β-equal; programs that give the same answers are extensionally equal. The cells show 16 behaviours but 506 programs.

Gate	Truth table	Programs	Cells	Its lambda16.txt program
0 FALSE	0000	63	680	`λpqab.b`
1 q AND NOT p	0010	32	216	`λpqab.p b (q a b)`
2 AND	1000	32	216	`λpqab.p (q a b) b`
3 Q	1010	21	168	`λpqab.q a b`
4 p AND NOT q	0100	32	216	`λpqab.p (q b a) b`
5 XOR	0110	20	168	`λpqab.p (q b a) (q a b)`
6 P	1100	21	168	`λpqab.p a b`
7 OR	1110	32	216	`λpqab.p a (q a b)`
8 NOR	0001	32	216	`λpqab.p b (q b a)`
9 NOT P	0011	21	168	`λpqab.p b a`
10 XNOR	1001	20	168	`λpqab.p (q a b) (q b a)`
11 IMPLIES (p -> q)	1011	32	216	`λpqab.p (q a b) a`
12 NOT Q	0101	21	168	`λpqab.q b a`
13 NAND	0111	32	216	`λpqab.p (q b a) a`
14 CONVERSE (q -> p)	1101	32	216	`λpqab.p a (q b a)`
15 TRUE	1111	63	680	`λpqab.a`

Every one of the 506 programs is drawn as a Tromp diagram, written in eight notations (lambda short and long form, de Bruijn, Tromp binary, Polish, reverse Polish, SKI combinators and JavaScript) and mapped back to the cells it comes from (all 16 squares, coloured by a chosen quarter) in The 506 Programs on the public site. Its file is page/programs-506.html. Each notation was checked: the text forms read back to the same term, and the lambda, SKI and JavaScript versions all reproduce the truth table.

Same term? Filled cells reduce to the lambda16.txt term

The programs for XOR, from the interactive page

Files

Path	What it is
`../docs/gates-of-gates-document.html`	everything below in one self-contained document (open it in any browser, works offline); also the public site's copy
`images/`	the poster photo, the figures above, and two screenshots of the page
`data/cells.csv`	all 4,096 cells: G, X, Y, the result, and which of the 506 programs it reduces to
`data/programs.csv`	the 506 programs: behaviour, number of cells, whether it is the lambda16.txt term, short form, an example cell
`data/gates-data.json`	the same data as used by the page
`page/gates-of-gates.html`	a local copy of the interactive page
`page/programs-506.html`	all 506 programs, each as a Tromp diagram, in eight notations, with a map of the cells it comes from
`tools/`	the scripts that regenerate everything

Truth-table columns in the CSV files start with an apostrophe ('1000) so spreadsheets keep the leading zeros.

To regenerate, from this folder:

node tools/gates.js                 # recompute every cell by lambda reduction; writes tools/gates.html and tools/gates-data.json
python3 tools/figures.py images     # redraw the figures from tools/gates-data.json
node tools/programs506.js           # rebuild the 506-programs page from tools/gates-data.json; writes tools/programs506.html
wrap() { printf '<!doctype html>\n<html lang="en">\n<head>\n<meta charset="utf-8">\n<meta name="viewport" content="width=device-width, initial-scale=1">\n<style>[hidden]{display:none!important} body{margin:0}</style>\n</head>\n<body>\n'; cat "$1"; printf '\n</body>\n</html>\n'; }
wrap tools/gates.html > page/gates-of-gates.html        # make the two standalone pages (see below)
wrap tools/programs506.html > page/programs-506.html
cp page/gates-of-gates.html page/programs-506.html ../docs/   # update the public site (GitHub Pages serves docs/)
cp tools/gates-data.json data/       # keep data/ in step (the page itself carries its data inline)
python3 tools/build_document.py PATH/TO/md2html.py   # rebuild ../docs/gates-of-gates-document.html and copy lambda16.txt and the poster photo to ../docs/ (md2html.py is in the lasermade-tools repository)

tools/gates.html and tools/programs506.html are page bodies: they were written to be published as claude.ai pages, which add the document skeleton themselves, so they have no <!doctype>, <head> or viewport tag. wrap adds that skeleton: the doctype, the character set, the viewport tag (without it, phones draw the page at desktop width) and the [hidden] rule the pages rely on. The result is page/gates-of-gates.html and page/programs-506.html, which open on their own in any browser; the copy in docs/ is what the public site serves, and build_document.py embeds the page/ files in the document. That is why build_document.py runs last. tools/gates.html, tools/programs506.html and tools/gates-data.json are only intermediate output; they are not in the repository, so delete them afterwards.

Nothing here writes data/cells.csv or data/programs.csv; they have no generator in the repository. Both agree with the regenerated data cell for cell.

tools/allreduce.js rebuilds the reduction half of lambda16.txt: run from any folder, it writes reductions.txt there, and that file appears verbatim in lambda16.txt from the "Beta reduction of all sixteen" heading on.

gates.js stops with an error if any cell, pattern or program count fails its check, and programs506.js stops if any notation fails its check.

Interactive: Gates of Gates

The full interactive page: six cell views, two axis orders, hover details and a table for any square. It runs inside this document.

All 506 programs

Every distinct normal form behind the 4,096 cells, as a Tromp diagram, in eight notations, and mapped back to the cells it comes from. The list scrolls inside its frame; use the controls at its top to pick a gate or hide notations.

Appendix: lambda16.txt

The sixteen functions as lambda terms, with every β-reduction, exactly as in the repository.

Show lambda16.txt (867 lines)

The sixteen boolean functions of two variables as pure lambda terms
====================================================================

No shortcuts: every λ takes exactly one argument, every application
(f x) is bracketed, and nothing is abbreviated (no TRUE/FALSE/NOT names).

Each gate is in η-long β-normal form: fully expanded, fully reduced, no
abbreviations. Every gate names all four inputs (λp.λq.λa.λb.), every p and q
is applied to two arguments, and nothing is left to reduce. P and Q have
shorter βη-normal forms, λp.(λq.p) and λp.(λq.q), but the long form keeps all
sixteen in the same shape so the complement rule works.

Church booleans:   true = λa.(λb.a)    false = λa.(λb.b)
Inside a body:     a = TRUE,  b = FALSE
                   ((q a) b) = q,  ((q b) a) = NOT q
Every body is ((p X) Y): X is the answer when p is true, Y when p is false.

idx = position in OPS (python/boolean16.py); entry i and 15 - i are complements.
TT TF FT FF = output for (p,q) = (T,T) (T,F) (F,T) (F,F).

idx  TT TF FT FF  name               lambda term
---  -----------  -----------------  ------------------------------------------------
  0   0  0  0  0  FALSE              λp.(λq.(λa.(λb.b)))
  1   0  0  1  0  q AND NOT p        λp.(λq.(λa.(λb.((p b) ((q a) b)))))
  2   1  0  0  0  AND                λp.(λq.(λa.(λb.((p ((q a) b)) b))))
  3   1  0  1  0  Q                  λp.(λq.(λa.(λb.((q a) b))))
  4   0  1  0  0  p AND NOT q        λp.(λq.(λa.(λb.((p ((q b) a)) b))))
  5   0  1  1  0  XOR                λp.(λq.(λa.(λb.((p ((q b) a)) ((q a) b)))))
  6   1  1  0  0  P                  λp.(λq.(λa.(λb.((p a) b))))
  7   1  1  1  0  OR                 λp.(λq.(λa.(λb.((p a) ((q a) b)))))
  8   0  0  0  1  NOR                λp.(λq.(λa.(λb.((p b) ((q b) a)))))
  9   0  0  1  1  NOT P              λp.(λq.(λa.(λb.((p b) a))))
 10   1  0  0  1  XNOR               λp.(λq.(λa.(λb.((p ((q a) b)) ((q b) a)))))
 11   1  0  1  1  IMPLIES (p -> q)   λp.(λq.(λa.(λb.((p ((q a) b)) a))))
 12   0  1  0  1  NOT Q              λp.(λq.(λa.(λb.((q b) a))))
 13   0  1  1  1  NAND               λp.(λq.(λa.(λb.((p ((q b) a)) a))))
 14   1  1  0  1  CONVERSE (q -> p)  λp.(λq.(λa.(λb.((p a) ((q b) a)))))
 15   1  1  1  1  TRUE               λp.(λq.(λa.(λb.a)))

Complement rule: swap every a and b in the body (after λb.) to get the
complement, idx 15 - i. Swapping the binders too only renames and changes nothing.


Beta reduction of all sixteen, on all four inputs
==================================================

TRUE = λx.(λy.x) and FALSE = λx.(λy.y) use x and y so they cannot clash with a and b.
Normal order: the leftmost, outermost redex is reduced first.
Each step says which variable was replaced and by what. "(thrown away)" means
the bound variable did not appear in the body, so the argument vanishes unreduced.
Every reduction ends at λa.(λb.a) = TRUE or λa.(λb.b) = FALSE.


--- 0  FALSE   λp.(λq.(λa.(λb.b)))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.b)))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.b))) (λx.(λy.x)))
        p := TRUE   (thrown away)
   2  λa.(λb.b)
        q := TRUE   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.b)))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.b))) (λx.(λy.y)))
        p := TRUE   (thrown away)
   2  λa.(λb.b)
        q := FALSE   (thrown away)

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.b)))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.b))) (λx.(λy.x)))
        p := FALSE   (thrown away)
   2  λa.(λb.b)
        q := TRUE   (thrown away)

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.b)))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.b))) (λx.(λy.y)))
        p := FALSE   (thrown away)
   2  λa.(λb.b)
        q := FALSE   (thrown away)


--- 1  q AND NOT p   λp.(λq.(λa.(λb.((p b) ((q a) b)))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) ((q a) b)))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) b) ((q a) b))))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) b) (((λx.(λy.x)) a) b)))
        q := TRUE
   3  λa.(λb.((λy.b) (((λx.(λy.x)) a) b)))
        x := b
   4  λa.(λb.b)
        y := (((λx.(λy.x)) a) b)   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) ((q a) b)))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) b) ((q a) b))))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) b) (((λx.(λy.y)) a) b)))
        q := FALSE
   3  λa.(λb.((λy.b) (((λx.(λy.y)) a) b)))
        x := b
   4  λa.(λb.b)
        y := (((λx.(λy.y)) a) b)   (thrown away)

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p b) ((q a) b)))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) b) ((q a) b))))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) b) (((λx.(λy.x)) a) b)))
        q := TRUE
   3  λa.(λb.((λy.y) (((λx.(λy.x)) a) b)))
        x := b   (thrown away)
   4  λa.(λb.(((λx.(λy.x)) a) b))
        y := (((λx.(λy.x)) a) b)
   5  λa.(λb.((λy.a) b))
        x := a
   6  λa.(λb.a)
        y := b   (thrown away)

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) ((q a) b)))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) b) ((q a) b))))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) b) (((λx.(λy.y)) a) b)))
        q := FALSE
   3  λa.(λb.((λy.y) (((λx.(λy.y)) a) b)))
        x := b   (thrown away)
   4  λa.(λb.(((λx.(λy.y)) a) b))
        y := (((λx.(λy.y)) a) b)
   5  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   6  λa.(λb.b)
        y := b


--- 2  AND   λp.(λq.(λa.(λb.((p ((q a) b)) b))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) b))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q a) b)) b)))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.x)) a) b)) b))
        q := TRUE
   3  λa.(λb.((λy.(((λx.(λy.x)) a) b)) b))
        x := (((λx.(λy.x)) a) b)
   4  λa.(λb.(((λx.(λy.x)) a) b))
        y := b   (thrown away)
   5  λa.(λb.((λy.a) b))
        x := a
   6  λa.(λb.a)
        y := b   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) b))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q a) b)) b)))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.y)) a) b)) b))
        q := FALSE
   3  λa.(λb.((λy.(((λx.(λy.y)) a) b)) b))
        x := (((λx.(λy.y)) a) b)
   4  λa.(λb.(((λx.(λy.y)) a) b))
        y := b   (thrown away)
   5  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   6  λa.(λb.b)
        y := b

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) b))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q a) b)) b)))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.x)) a) b)) b))
        q := TRUE
   3  λa.(λb.((λy.y) b))
        x := (((λx.(λy.x)) a) b)   (thrown away)
   4  λa.(λb.b)
        y := b

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) b))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q a) b)) b)))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.y)) a) b)) b))
        q := FALSE
   3  λa.(λb.((λy.y) b))
        x := (((λx.(λy.y)) a) b)   (thrown away)
   4  λa.(λb.b)
        y := b


--- 3  Q   λp.(λq.(λa.(λb.((q a) b))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((q a) b))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.((q a) b)))) (λx.(λy.x)))
        p := TRUE   (thrown away)
   2  λa.(λb.(((λx.(λy.x)) a) b))
        q := TRUE
   3  λa.(λb.((λy.a) b))
        x := a
   4  λa.(λb.a)
        y := b   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((q a) b))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.((q a) b)))) (λx.(λy.y)))
        p := TRUE   (thrown away)
   2  λa.(λb.(((λx.(λy.y)) a) b))
        q := FALSE
   3  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   4  λa.(λb.b)
        y := b

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((q a) b))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.((q a) b)))) (λx.(λy.x)))
        p := FALSE   (thrown away)
   2  λa.(λb.(((λx.(λy.x)) a) b))
        q := TRUE
   3  λa.(λb.((λy.a) b))
        x := a
   4  λa.(λb.a)
        y := b   (thrown away)

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((q a) b))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.((q a) b)))) (λx.(λy.y)))
        p := FALSE   (thrown away)
   2  λa.(λb.(((λx.(λy.y)) a) b))
        q := FALSE
   3  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   4  λa.(λb.b)
        y := b


--- 4  p AND NOT q   λp.(λq.(λa.(λb.((p ((q b) a)) b))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) b))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q b) a)) b)))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.x)) b) a)) b))
        q := TRUE
   3  λa.(λb.((λy.(((λx.(λy.x)) b) a)) b))
        x := (((λx.(λy.x)) b) a)
   4  λa.(λb.(((λx.(λy.x)) b) a))
        y := b   (thrown away)
   5  λa.(λb.((λy.b) a))
        x := b
   6  λa.(λb.b)
        y := a   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) b))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q b) a)) b)))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.y)) b) a)) b))
        q := FALSE
   3  λa.(λb.((λy.(((λx.(λy.y)) b) a)) b))
        x := (((λx.(λy.y)) b) a)
   4  λa.(λb.(((λx.(λy.y)) b) a))
        y := b   (thrown away)
   5  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   6  λa.(λb.a)
        y := a

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) b))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q b) a)) b)))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.x)) b) a)) b))
        q := TRUE
   3  λa.(λb.((λy.y) b))
        x := (((λx.(λy.x)) b) a)   (thrown away)
   4  λa.(λb.b)
        y := b

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) b))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q b) a)) b)))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.y)) b) a)) b))
        q := FALSE
   3  λa.(λb.((λy.y) b))
        x := (((λx.(λy.y)) b) a)   (thrown away)
   4  λa.(λb.b)
        y := b


--- 5  XOR   λp.(λq.(λa.(λb.((p ((q b) a)) ((q a) b)))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) ((q a) b)))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q b) a)) ((q a) b))))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.x)) b) a)) (((λx.(λy.x)) a) b)))
        q := TRUE
   3  λa.(λb.((λy.(((λx.(λy.x)) b) a)) (((λx.(λy.x)) a) b)))
        x := (((λx.(λy.x)) b) a)
   4  λa.(λb.(((λx.(λy.x)) b) a))
        y := (((λx.(λy.x)) a) b)   (thrown away)
   5  λa.(λb.((λy.b) a))
        x := b
   6  λa.(λb.b)
        y := a   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) ((q a) b)))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q b) a)) ((q a) b))))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.y)) b) a)) (((λx.(λy.y)) a) b)))
        q := FALSE
   3  λa.(λb.((λy.(((λx.(λy.y)) b) a)) (((λx.(λy.y)) a) b)))
        x := (((λx.(λy.y)) b) a)
   4  λa.(λb.(((λx.(λy.y)) b) a))
        y := (((λx.(λy.y)) a) b)   (thrown away)
   5  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   6  λa.(λb.a)
        y := a

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) ((q a) b)))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q b) a)) ((q a) b))))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.x)) b) a)) (((λx.(λy.x)) a) b)))
        q := TRUE
   3  λa.(λb.((λy.y) (((λx.(λy.x)) a) b)))
        x := (((λx.(λy.x)) b) a)   (thrown away)
   4  λa.(λb.(((λx.(λy.x)) a) b))
        y := (((λx.(λy.x)) a) b)
   5  λa.(λb.((λy.a) b))
        x := a
   6  λa.(λb.a)
        y := b   (thrown away)

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) ((q a) b)))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q b) a)) ((q a) b))))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.y)) b) a)) (((λx.(λy.y)) a) b)))
        q := FALSE
   3  λa.(λb.((λy.y) (((λx.(λy.y)) a) b)))
        x := (((λx.(λy.y)) b) a)   (thrown away)
   4  λa.(λb.(((λx.(λy.y)) a) b))
        y := (((λx.(λy.y)) a) b)
   5  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   6  λa.(λb.b)
        y := b


--- 6  P   λp.(λq.(λa.(λb.((p a) b))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) b))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) a) b)))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) a) b))
        q := TRUE   (thrown away)
   3  λa.(λb.((λy.a) b))
        x := a
   4  λa.(λb.a)
        y := b   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) b))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) a) b)))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) a) b))
        q := FALSE   (thrown away)
   3  λa.(λb.((λy.a) b))
        x := a
   4  λa.(λb.a)
        y := b   (thrown away)

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p a) b))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) a) b)))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) a) b))
        q := TRUE   (thrown away)
   3  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   4  λa.(λb.b)
        y := b

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p a) b))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) a) b)))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) a) b))
        q := FALSE   (thrown away)
   3  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   4  λa.(λb.b)
        y := b


--- 7  OR   λp.(λq.(λa.(λb.((p a) ((q a) b)))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) ((q a) b)))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) a) ((q a) b))))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) a) (((λx.(λy.x)) a) b)))
        q := TRUE
   3  λa.(λb.((λy.a) (((λx.(λy.x)) a) b)))
        x := a
   4  λa.(λb.a)
        y := (((λx.(λy.x)) a) b)   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) ((q a) b)))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) a) ((q a) b))))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) a) (((λx.(λy.y)) a) b)))
        q := FALSE
   3  λa.(λb.((λy.a) (((λx.(λy.y)) a) b)))
        x := a
   4  λa.(λb.a)
        y := (((λx.(λy.y)) a) b)   (thrown away)

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) ((q a) b)))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) a) ((q a) b))))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) a) (((λx.(λy.x)) a) b)))
        q := TRUE
   3  λa.(λb.((λy.y) (((λx.(λy.x)) a) b)))
        x := a   (thrown away)
   4  λa.(λb.(((λx.(λy.x)) a) b))
        y := (((λx.(λy.x)) a) b)
   5  λa.(λb.((λy.a) b))
        x := a
   6  λa.(λb.a)
        y := b   (thrown away)

  p = FALSE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p a) ((q a) b)))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) a) ((q a) b))))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) a) (((λx.(λy.y)) a) b)))
        q := FALSE
   3  λa.(λb.((λy.y) (((λx.(λy.y)) a) b)))
        x := a   (thrown away)
   4  λa.(λb.(((λx.(λy.y)) a) b))
        y := (((λx.(λy.y)) a) b)
   5  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   6  λa.(λb.b)
        y := b


--- 8  NOR   λp.(λq.(λa.(λb.((p b) ((q b) a)))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) ((q b) a)))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) b) ((q b) a))))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) b) (((λx.(λy.x)) b) a)))
        q := TRUE
   3  λa.(λb.((λy.b) (((λx.(λy.x)) b) a)))
        x := b
   4  λa.(λb.b)
        y := (((λx.(λy.x)) b) a)   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) ((q b) a)))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) b) ((q b) a))))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) b) (((λx.(λy.y)) b) a)))
        q := FALSE
   3  λa.(λb.((λy.b) (((λx.(λy.y)) b) a)))
        x := b
   4  λa.(λb.b)
        y := (((λx.(λy.y)) b) a)   (thrown away)

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) ((q b) a)))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) b) ((q b) a))))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) b) (((λx.(λy.x)) b) a)))
        q := TRUE
   3  λa.(λb.((λy.y) (((λx.(λy.x)) b) a)))
        x := b   (thrown away)
   4  λa.(λb.(((λx.(λy.x)) b) a))
        y := (((λx.(λy.x)) b) a)
   5  λa.(λb.((λy.b) a))
        x := b
   6  λa.(λb.b)
        y := a   (thrown away)

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p b) ((q b) a)))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) b) ((q b) a))))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) b) (((λx.(λy.y)) b) a)))
        q := FALSE
   3  λa.(λb.((λy.y) (((λx.(λy.y)) b) a)))
        x := b   (thrown away)
   4  λa.(λb.(((λx.(λy.y)) b) a))
        y := (((λx.(λy.y)) b) a)
   5  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   6  λa.(λb.a)
        y := a


--- 9  NOT P   λp.(λq.(λa.(λb.((p b) a))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) a))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) b) a)))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) b) a))
        q := TRUE   (thrown away)
   3  λa.(λb.((λy.b) a))
        x := b
   4  λa.(λb.b)
        y := a   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p b) a))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) b) a)))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) b) a))
        q := FALSE   (thrown away)
   3  λa.(λb.((λy.b) a))
        x := b
   4  λa.(λb.b)
        y := a   (thrown away)

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p b) a))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) b) a)))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) b) a))
        q := TRUE   (thrown away)
   3  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   4  λa.(λb.a)
        y := a

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p b) a))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) b) a)))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) b) a))
        q := FALSE   (thrown away)
   3  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   4  λa.(λb.a)
        y := a


--- 10  XNOR   λp.(λq.(λa.(λb.((p ((q a) b)) ((q b) a)))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) ((q b) a)))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q a) b)) ((q b) a))))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.x)) a) b)) (((λx.(λy.x)) b) a)))
        q := TRUE
   3  λa.(λb.((λy.(((λx.(λy.x)) a) b)) (((λx.(λy.x)) b) a)))
        x := (((λx.(λy.x)) a) b)
   4  λa.(λb.(((λx.(λy.x)) a) b))
        y := (((λx.(λy.x)) b) a)   (thrown away)
   5  λa.(λb.((λy.a) b))
        x := a
   6  λa.(λb.a)
        y := b   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) ((q b) a)))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q a) b)) ((q b) a))))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.y)) a) b)) (((λx.(λy.y)) b) a)))
        q := FALSE
   3  λa.(λb.((λy.(((λx.(λy.y)) a) b)) (((λx.(λy.y)) b) a)))
        x := (((λx.(λy.y)) a) b)
   4  λa.(λb.(((λx.(λy.y)) a) b))
        y := (((λx.(λy.y)) b) a)   (thrown away)
   5  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   6  λa.(λb.b)
        y := b

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) ((q b) a)))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q a) b)) ((q b) a))))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.x)) a) b)) (((λx.(λy.x)) b) a)))
        q := TRUE
   3  λa.(λb.((λy.y) (((λx.(λy.x)) b) a)))
        x := (((λx.(λy.x)) a) b)   (thrown away)
   4  λa.(λb.(((λx.(λy.x)) b) a))
        y := (((λx.(λy.x)) b) a)
   5  λa.(λb.((λy.b) a))
        x := b
   6  λa.(λb.b)
        y := a   (thrown away)

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) ((q b) a)))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q a) b)) ((q b) a))))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.y)) a) b)) (((λx.(λy.y)) b) a)))
        q := FALSE
   3  λa.(λb.((λy.y) (((λx.(λy.y)) b) a)))
        x := (((λx.(λy.y)) a) b)   (thrown away)
   4  λa.(λb.(((λx.(λy.y)) b) a))
        y := (((λx.(λy.y)) b) a)
   5  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   6  λa.(λb.a)
        y := a


--- 11  IMPLIES (p -> q)   λp.(λq.(λa.(λb.((p ((q a) b)) a))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) a))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q a) b)) a)))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.x)) a) b)) a))
        q := TRUE
   3  λa.(λb.((λy.(((λx.(λy.x)) a) b)) a))
        x := (((λx.(λy.x)) a) b)
   4  λa.(λb.(((λx.(λy.x)) a) b))
        y := a   (thrown away)
   5  λa.(λb.((λy.a) b))
        x := a
   6  λa.(λb.a)
        y := b   (thrown away)

  p = TRUE, q = FALSE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) a))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q a) b)) a)))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.y)) a) b)) a))
        q := FALSE
   3  λa.(λb.((λy.(((λx.(λy.y)) a) b)) a))
        x := (((λx.(λy.y)) a) b)
   4  λa.(λb.(((λx.(λy.y)) a) b))
        y := a   (thrown away)
   5  λa.(λb.((λy.y) b))
        x := a   (thrown away)
   6  λa.(λb.b)
        y := b

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) a))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q a) b)) a)))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.x)) a) b)) a))
        q := TRUE
   3  λa.(λb.((λy.y) a))
        x := (((λx.(λy.x)) a) b)   (thrown away)
   4  λa.(λb.a)
        y := a

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q a) b)) a))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q a) b)) a)))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.y)) a) b)) a))
        q := FALSE
   3  λa.(λb.((λy.y) a))
        x := (((λx.(λy.y)) a) b)   (thrown away)
   4  λa.(λb.a)
        y := a


--- 12  NOT Q   λp.(λq.(λa.(λb.((q b) a))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((q b) a))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.((q b) a)))) (λx.(λy.x)))
        p := TRUE   (thrown away)
   2  λa.(λb.(((λx.(λy.x)) b) a))
        q := TRUE
   3  λa.(λb.((λy.b) a))
        x := b
   4  λa.(λb.b)
        y := a   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((q b) a))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.((q b) a)))) (λx.(λy.y)))
        p := TRUE   (thrown away)
   2  λa.(λb.(((λx.(λy.y)) b) a))
        q := FALSE
   3  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   4  λa.(λb.a)
        y := a

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((q b) a))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.((q b) a)))) (λx.(λy.x)))
        p := FALSE   (thrown away)
   2  λa.(λb.(((λx.(λy.x)) b) a))
        q := TRUE
   3  λa.(λb.((λy.b) a))
        x := b
   4  λa.(λb.b)
        y := a   (thrown away)

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((q b) a))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.((q b) a)))) (λx.(λy.y)))
        p := FALSE   (thrown away)
   2  λa.(λb.(((λx.(λy.y)) b) a))
        q := FALSE
   3  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   4  λa.(λb.a)
        y := a


--- 13  NAND   λp.(λq.(λa.(λb.((p ((q b) a)) a))))

  p = TRUE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) a))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q b) a)) a)))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.x)) b) a)) a))
        q := TRUE
   3  λa.(λb.((λy.(((λx.(λy.x)) b) a)) a))
        x := (((λx.(λy.x)) b) a)
   4  λa.(λb.(((λx.(λy.x)) b) a))
        y := a   (thrown away)
   5  λa.(λb.((λy.b) a))
        x := b
   6  λa.(λb.b)
        y := a   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) a))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) ((q b) a)) a)))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) (((λx.(λy.y)) b) a)) a))
        q := FALSE
   3  λa.(λb.((λy.(((λx.(λy.y)) b) a)) a))
        x := (((λx.(λy.y)) b) a)
   4  λa.(λb.(((λx.(λy.y)) b) a))
        y := a   (thrown away)
   5  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   6  λa.(λb.a)
        y := a

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) a))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q b) a)) a)))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.x)) b) a)) a))
        q := TRUE
   3  λa.(λb.((λy.y) a))
        x := (((λx.(λy.x)) b) a)   (thrown away)
   4  λa.(λb.a)
        y := a

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p ((q b) a)) a))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) ((q b) a)) a)))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) (((λx.(λy.y)) b) a)) a))
        q := FALSE
   3  λa.(λb.((λy.y) a))
        x := (((λx.(λy.y)) b) a)   (thrown away)
   4  λa.(λb.a)
        y := a


--- 14  CONVERSE (q -> p)   λp.(λq.(λa.(λb.((p a) ((q b) a)))))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) ((q b) a)))))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) a) ((q b) a))))) (λx.(λy.x)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) a) (((λx.(λy.x)) b) a)))
        q := TRUE
   3  λa.(λb.((λy.a) (((λx.(λy.x)) b) a)))
        x := a
   4  λa.(λb.a)
        y := (((λx.(λy.x)) b) a)   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) ((q b) a)))))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.x)) a) ((q b) a))))) (λx.(λy.y)))
        p := TRUE
   2  λa.(λb.(((λx.(λy.x)) a) (((λx.(λy.y)) b) a)))
        q := FALSE
   3  λa.(λb.((λy.a) (((λx.(λy.y)) b) a)))
        x := a
   4  λa.(λb.a)
        y := (((λx.(λy.y)) b) a)   (thrown away)

  p = FALSE, q = TRUE  →  FALSE
   0  (((λp.(λq.(λa.(λb.((p a) ((q b) a)))))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) a) ((q b) a))))) (λx.(λy.x)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) a) (((λx.(λy.x)) b) a)))
        q := TRUE
   3  λa.(λb.((λy.y) (((λx.(λy.x)) b) a)))
        x := a   (thrown away)
   4  λa.(λb.(((λx.(λy.x)) b) a))
        y := (((λx.(λy.x)) b) a)
   5  λa.(λb.((λy.b) a))
        x := b
   6  λa.(λb.b)
        y := a   (thrown away)

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.((p a) ((q b) a)))))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.(((λx.(λy.y)) a) ((q b) a))))) (λx.(λy.y)))
        p := FALSE
   2  λa.(λb.(((λx.(λy.y)) a) (((λx.(λy.y)) b) a)))
        q := FALSE
   3  λa.(λb.((λy.y) (((λx.(λy.y)) b) a)))
        x := a   (thrown away)
   4  λa.(λb.(((λx.(λy.y)) b) a))
        y := (((λx.(λy.y)) b) a)
   5  λa.(λb.((λy.y) a))
        x := b   (thrown away)
   6  λa.(λb.a)
        y := a


--- 15  TRUE   λp.(λq.(λa.(λb.a)))

  p = TRUE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.a)))) (λx.(λy.x))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.a))) (λx.(λy.x)))
        p := TRUE   (thrown away)
   2  λa.(λb.a)
        q := TRUE   (thrown away)

  p = TRUE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.a)))) (λx.(λy.x))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.a))) (λx.(λy.y)))
        p := TRUE   (thrown away)
   2  λa.(λb.a)
        q := FALSE   (thrown away)

  p = FALSE, q = TRUE  →  TRUE
   0  (((λp.(λq.(λa.(λb.a)))) (λx.(λy.y))) (λx.(λy.x)))
   1  ((λq.(λa.(λb.a))) (λx.(λy.x)))
        p := FALSE   (thrown away)
   2  λa.(λb.a)
        q := TRUE   (thrown away)

  p = FALSE, q = FALSE  →  TRUE
   0  (((λp.(λq.(λa.(λb.a)))) (λx.(λy.y))) (λx.(λy.y)))
   1  ((λq.(λa.(λb.a))) (λx.(λy.y)))
        p := FALSE   (thrown away)
   2  λa.(λb.a)
        q := FALSE   (thrown away)

Appendix: data

The data behind every picture, as CSV. Truth-table columns start with an apostrophe so spreadsheets keep the leading zeros.

cells.csv: all 4,096 cells, with G, X, Y, the result, and which of the 506 programs it reduces to
programs.csv: the 506 programs, with behaviour, number of cells, whether it is the lambda16.txt term, short form and an example cell