mod Maux logic: 'cl'

incl Mtex

incl Mtexln

rem 
  \para \bf  Characteristic function.  \end 

fun/2 Eqf 'Tex_f2_n_char_eqf'
  Eqf(x,y) = 1 <- x = y
  Eqf(x,y) = 0 <- x != y

rem 
  \para \bf  Numeric programs.  \end 

fun/2 Min 'Tex_f2_n_min'
  Min(x,y) = x <- x <= y
  Min(x,y) = y <- x > y

fun/2 Max 'Tex_f2_n_max'
  Max(x,y) = x <- x >= y
  Max(x,y) = y <- x < y

rem 
  \para \bf  Catalan pairing function.  \end 

rem 
  \para \it  Pairing function.  \end 

fun/2 Pair 'Tex_f2_pp_pair'
  Pair(x,y) = x,y

rem 
  \para \it  Projection functions.  \end 

fun Proj1 'Tex_f1_pp_proj1'
  Proj1(x) = H(x)

fun Proj2 'Tex_f1_pp_proj2'
  Proj2(x) = T(x)

rem 
  \para \it  Unary iteration of the second projection.  \end 

fun/2 Iproj2 'Tex_f2_pp_iproj2'
  Iproj2(0,x) = x
  Iproj2(n+1,x) = Iproj2(n,Proj2(x))

rem 
  \para \bf  Tuples.  \end 

pred/2 Tuple 
  Tuple(n,x) <-> n = 0 & x = 0 \/ n = 1 \/ n >= 2 & Iproj2(n-2,x) != 0

fun/3 Proj 'Tex_f3_pp_proj'
  Proj(n,x,i) = Proj1 Iproj2(i-1,x) <- i != n
  Proj(n,x,i) = Iproj2(n-1,x) <- i = n

