Require Import List.
Import ListNotations.
Definition stack (X : Type) := list (list X * list X).
Fixpoint sigma {X: Type} (a : X) (A : stack X) :=
match A with
nil => [a]
| (x, y) :: A => x ++ (sigma a A) ++ y
end.
Definition CFPP : stack nat * nat -> Prop :=
fun '(R, a) => exists (A : stack nat),
incl A R /\ A <> [] /\ sigma a A = rev (sigma a A).
Definition CFPI : stack nat * stack nat * nat -> Prop :=
fun '(R1, R2, a) => exists (A1 A2 : stack nat),
incl A1 R1 /\ incl A2 R2 /\ A1 <> [] /\ A2 <> [] /\ sigma a A1 = sigma a A2.
Import ListNotations.
Definition stack (X : Type) := list (list X * list X).
Fixpoint sigma {X: Type} (a : X) (A : stack X) :=
match A with
nil => [a]
| (x, y) :: A => x ++ (sigma a A) ++ y
end.
Definition CFPP : stack nat * nat -> Prop :=
fun '(R, a) => exists (A : stack nat),
incl A R /\ A <> [] /\ sigma a A = rev (sigma a A).
Definition CFPI : stack nat * stack nat * nat -> Prop :=
fun '(R1, R2, a) => exists (A1 A2 : stack nat),
incl A1 R1 /\ incl A2 R2 /\ A1 <> [] /\ A2 <> [] /\ sigma a A1 = sigma a A2.