Alphabet

and:[c × c] ⟶ c
cons:[a × b] ⟶ b
false:c
forall:[a → c × b] ⟶ c
forsome:[a → c × b] ⟶ c
nil:b
or:[c × c] ⟶ c
true:c

Variables

F:a → c
Z:a → c
U:a
V:b
I:a → c
J:a → c
X1:a
Y1:b

Rules

and(true, true)⇒true
and(true, false)⇒false
and(false, true)⇒false
and(false, false)⇒false
or(true, true)⇒true
or(true, false)⇒true
or(false, true)⇒true
or(false, false)⇒false
forall(F, nil)⇒true
forall(Z, cons(U, V))⇒and(Z · U, forall(Z, V))
forsome(I, nil)⇒false
forsome(J, cons(X1, Y1))⇒or(J · X1, forsome(J, Y1))