Nuprl Definition : split-gap

split-gap(f;L) ==
  rec-case(L) of
  [] => <Ax, Ax>
  a::L =>
   r.if L = Ax then <<a, Ax>, Ax> otherwise let u1,v1 = L

                             in if f u1=(f a) + 1  then let X1,X2 = r in <<a, X1>, X2>  else <<a, Ax>, u1, v1>

Definitions occuring in Statement : list_ind: list_ind, isaxiom: if z = Ax then a otherwise b, int_eq: if a=b then c else d, apply: f a, spread: spread def, pair: <a, b>, add: n + m, natural_number: $n, axiom: Ax
Definitions occuring in definition : list_ind: list_ind, isaxiom: if z = Ax then a otherwise b, int_eq: if a=b then c else d, add: n + m, apply: f a, natural_number: $n, spread: spread def, axiom: Ax, pair: <a, b>
FDL editor aliases : split-gap

Latex:
split-gap(f;L) == rec-case(L) of [] => <Ax, Ax> a::L => r.if L = Ax then <<a, Ax>, Ax> otherwise let u1,v1 = L in if f u1=(f a) + 1 then let X1,X2 = r in <<a, X1>, X2> else <<a, Ax>, u1, v1> Date html generated: 2016_05_15-PM-04_41_35 Last ObjectModification: 2015_09_23-AM-07_49_31 Theory : general Home Index