2 setecho.

DEFINE
    C0  ==  pop;
    Csucc  ==  [dup [i] dip] dip i.

DEFINE
    Peano  ==  0 [succ].

Peano C0.
Peano [C0] Csucc.
Peano [[C0] Csucc] Csucc.
Peano [[[C0] Csucc] Csucc] Csucc.

DEFINE
    C1  ==  [C0] Csucc;
    C2  ==  [C1] Csucc;
    C3 ==  [C2] Csucc.

Peano C0.
Peano C1.
Peano C2.
Peano C3.

DEFINE
    Doublings  ==  1 [2 *];
    Lists  ==  [] [[i] swoncat].

Doublings C0.
Doublings C1.
Doublings C2.
Doublings C3.

Lists C0.
Lists C1.
Lists C2.
Lists C3.

DEFINE
    Cadd  ==  [ [[Csucc] cons] ] dip i i;
    Cmul  ==  [ [[C0]] dip  [Cadd] cons [cons] cons ] dip i i;
    Cpow  ==  [ [[C1 ]] dip  [Cmul] cons [cons] cons ] dip i i.

Peano [C2] [C3] Cadd.
Peano [C2] [C3] Cmul.
Peano [C2] [C3] Cpow.

Doublings [C2] [C3] Cadd.
Doublings [C2] [C3] Cmul.
Doublings [C2] [C3] Cpow.

Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd .
Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd
            3   succ    2   +      3   *     succ    2   +      = .

Peano [[[[C2] [C3] Cmul] [C2] Cpow] [[C2] [[C1] Csucc] Cmul] Cadd] [C2] Cadd.

DEFINE
    Q0  ==  [pop];
    Qsucc  ==  [ [dup [i] dip] dip i ]  cons.

Peano Q0 i.
Peano Q0 Qsucc i.
Peano Q0 Qsucc Qsucc i.

DEFINE
    Q1  ==  Q0 Qsucc;
    Q2  ==  Q1 Qsucc;
    Q3 ==  Q2 Qsucc.

Peano Q0 i.
Peano Q1 i.
Peano Q2 i.
Peano Q3 i.

Q0.
Q1.
Q2.
Q3.

DEFINE
    Qadd  ==
      [ [[Qsucc i] cons] swap i i ]  cons cons;
    Qmul  ==
      [ [[[Q0 i]] dip [Qadd i] cons [cons] cons] dip i i ] cons cons;
    Qpow  ==
      [ [[[Q1 i]] dip [Qmul i] cons [cons] cons] dip i i ] cons cons.


Peano Q2 Q3 Qadd i .
Peano Q2 Q3 Qmul i .
Peano Q2 Q3 Qpow i .

Q2 Q3 Qadd .
Q2 Q3 Qmul .
Q2 Q3 Qpow .

Peano      Q3 Qsucc  Q2 Qadd  Q3 Qmul Qsucc Q2 Qadd i.
Peano      Q3 Qsucc  Q2 Qadd  Q3 Qmul Qsucc Q2 Qadd i
            3  succ   2  +     3  *    succ  2  +      = .


DEFINE 
    Ctrue  ==  pop i;
    Cfalse  ==  popd i.

DEFINE
    Boole == ["Yes, yes"] ["No, no"];
    Comparison  ==  2 3 [<] [>].

Boole Ctrue.
Boole Cfalse.
Comparison Ctrue.
Comparison Cfalse.

DEFINE
(*
    Cnot  ==  [ [Cfalse] [Ctrue] ] dip i.
*)
    Cnot  ==  swapd i.

Boole [Ctrue] Cnot.
Boole [Cfalse] Cnot.
Comparison [[Ctrue] Cnot] Cnot.
Comparison [[Cfalse] Cnot] Cnot.

DEFINE
    Cor  ==  [[Ctrue]] dipd i;
    Cand  ==  [[Cfalse]] dip i.

Boole [Ctrue ] [Ctrue ] Cor.
Boole [Ctrue ] [Cfalse] Cor.
Boole [Cfalse] [Ctrue ] Cor.
Boole [Cfalse] [Cfalse] Cor.
Boole [Ctrue ] [Ctrue ] Cand.
Boole [Ctrue ] [Cfalse] Cand.
Boole [Cfalse] [Ctrue ] Cand.
Boole [Cfalse] [Cfalse] Cand.

DEFINE
    Ceq0  == [ [Ctrue] [pop [Cfalse]] ] dip i i.

Boole [C0] Ceq0 .
Boole [C1] Ceq0 .
Boole [C2] Ceq0 .
Boole [[C0] Ceq0] [[[C2] Csucc] Ceq0] Cor.
Boole [[C0] Ceq0] [[[C2] Csucc] Ceq0] Cand.

DEFINE
    Cifte  ==  rolldown i.

Peano  [[C0] Ceq0]  [C2]  [C3]  Cifte.
Peano  [[C1] Ceq0]  [C2]  [C3]  Cifte.
Peano  [[[C0] Ceq0] Cnot]  [C2]  [C3]  Cifte.
Peano  [[[C1] Ceq0] Cnot]  [C2]  [C3]  Cifte.

	Peano [Ctrue ] [[Ctrue ] [C0] [C1] Cifte] [[Ctrue ] [C2] [C3] Cifte] Cifte.
Peano [Ctrue ] [[Cfalse] [C0] [C1] Cifte] [[Cfalse] [C2] [C3] Cifte] Cifte.
Peano [Cfalse] [[Ctrue ] [C0] [C1] Cifte] [[Ctrue ] [C2] [C3] Cifte] Cifte.
Peano [Cfalse] [[Cfalse] [C0] [C1] Cifte] [[Cfalse] [C2] [C3] Cifte] Cifte.

DEFINE
    Ccons  ==  [i];
    Ccar  ==  [Ctrue] swap i;
    Ccdr  ==  [Cfalse] swap i.

Peano  [C0] [C1] Ccons Ccar.
Peano  [C0] [C1] Ccons Ccdr.

Peano [[C0] [C1] Ccons Ccar] [[C2] [C3] Ccons Ccar] Ccons Ccar.
Peano [[C0] [C1] Ccons Ccdr] [[C2] [C3] Ccons Ccdr] Ccons Ccar.
Peano [[C0] [C1] Ccons Ccar] [[C2] [C3] Ccons Ccar] Ccons Ccdr.
Peano [[C0] [C1] Ccons Ccdr] [[C2] [C3] Ccons Ccdr] Ccons Ccdr.
# The definition of Brent Kerby's more elegant Church numerals

# The original definitions, commented away, are given for comparison.
# The new definitions over-ride the old ones.

DEFINE

#  Csucc ==  [dup [i] dip] dip i;
   Csucc ==  [dup dip] dip i;

#  Cadd ==  [ [[Csucc] cons] ] dip i i;
   Cadd ==  [sip] dip i;               # but sip needs to be defined:
                                         sip ==  dupd dip;

#  Cmul ==  [ [[C0]] dip  [Cadd] cons [cons] cons ] dip i i;
   Cmul ==  [cons] dip i;

#  Cpow ==  [ [[C1]] dip  [Cmul] cons [cons] cons ] dip i i;
   Cpow ==  [[cons] cons] dip i i.


# Now the old tests using the new definitions:

Peano [C2] [C3] Cadd.
Peano [C2] [C3] Cmul.
Peano [C2] [C3] Cpow.

Doublings [C2] [C3] Cadd.
Doublings [C2] [C3] Cmul.
Doublings [C2] [C3] Cpow.

Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd .
Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd
            3   succ    2   +      3   *     succ    2   +      = .