I   Couples

II   Fractions

1. 
   
   
   
   

   addN  ^ 1   1

   → β λ m. λ f . λ x . ( 1   f   (m   f  x))  ^ 1

   → β λ f . λ x . ( 1  ^ f   ( 1   f  x))

   → β λ f . λ x . (λ x . (f   x)  ^ ( 1   f  x))

   → β λ f . λ x . (f   ( 1  ^ f  x))

   → β λ f . λ x . (f   (λ x . (f   x)  ^ x))

   → β λ f . λ x . (f   (f   x)) = 2

   
   

   addN  ^ 2   3

   → β λ m. λ f . λ x . ( 2   f   (m   f  x))  ^ 3

   → β λ f . λ x . ( 2  ^ f   ( 3   f  x))

   → β λ f . λ x . (λ x . (f2   x)  ^ ( 3   f  x))

   → β λ f . λ x . (f2   ( 3  ^ f  x))

   → β λ f . λ x . (f2   (λ x . (f3   x)  ^ x))

   → β λ f . λ x . (f2   (f3   x)) = 5

   
   

   addN  ^ 3   2

   → β λ m. λ f . λ x . ( 3   f   (m   f  x))  ^ 2

   → β λ f . λ x . ( 3  ^ f   ( 2   f  x))

   → β λ f . λ x . (λ x . (f3   x)  ^ ( 2   f  x))

   → β λ f . λ x . (f3   ( 2  ^ f  x))

   → β λ f . λ x . (f3   (λ x . (f2   x)  ^ x))

   → β λ f . λ x . (f3   (f2   x)) = 5

   
   

   multN  ^ 1   2

   → β λ m. λ f . (m   ( 1   f))  ^ 2

   → β λ f . ( 2  ^ ( 1   f))

   → β λ f . λ x . (( 1   f)   (( 1  ^ f)   x))

   → β λ f . λ x . (( 1   f)   (λ x . (f   x)  ^ x))

   → β λ f . λ x . (( 1  ^ f)   (f   x))

   → β λ f . λ x . (λ x . (f   x)  ^ (f   x))

   → β λ f . λ x . (f   (f   x)) = 2

   
   

   multN  ^ 3   2

   → β λ m. λ f . (m   ( 3   f))  ^ 2

   → β λ f . ( 2  ^ ( 3   f))

   → β λ f . λ x . (( 3   f)   (( 3  ^ f)   x))

   → β λ f . λ x . (( 3   f)   (λ x . (f3   x)  ^ x))

   → β λ f . λ x . (( 3  ^ f)   (f3   x))

   → β λ f . λ x . (λ x . (f3   x)  ^ (f3   x))

   → β λ f . λ x . (f3   (f3   x)) = 6

   
   

2. addN  ^ n   0

   → β λ m. λ f . λ x . ( n   f   (m   f  x))  ^ 0

   → β λ f . λ x . ( n   f   ( 0  ^ f  x))

   → β λ f . λ x . ( n   f   (λ x . x  ^ x))

   → β λ f . λ x . ( n   f   x)

   → η λ f . ( n   f )

   → η n

   
   

   multN  ^ n   1

   → β λ m. λ f . (m   ( n   f))  ^ 1

   → β λ f . ( 1  ^ ( n   f))

   → β λ f . λ x . ( n   f   x)

   → η λ f . ( n   f)

   → η n

   
   
3. tuple2   a   b
   
   
   
   
4. addQ = λ q . λ r .

   (tuple2	(addN (multN   (index1   q)   (index2   r))   (multN   (index1   r)   (index2   q)))
   	(multN   (index2   q)   (index2   r)))

   
   multQ = λ q . λ r .

   (tuple2	(multN   (index1   q)   (index1   r))
   	(multN   (index2   q)   (index2   r)))

   
   

This document was translated from L^AT_EX by H^EV^EA.