Alphabet

rand:[nat] ⟶ nat
s:[nat] ⟶ nat
bool:[nat] ⟶ boolean
false:boolean
true:boolean
filter:[nat → boolean × list] ⟶ list
nil:list
0:nat
cons:[nat × list] ⟶ list
consif:[boolean × nat × list] ⟶ list

Variables

X:nat
F:nat → boolean
H:nat
T:list

Rules

rand(X)⇒X
rand(s(X))⇒rand(X)
bool(0)⇒false
bool(s(0))⇒true
filter(F, nil)⇒nil
filter(F, cons(H, T))⇒consif(F · H, H, filter(F, T))
consif(true, H, T)⇒cons(H, T)
consif(false, H, T)⇒T