Welcome to Abella 2.0.5-dev.

Abella <Specification "breduce".Reading specification "breduce".

Abella <Close tm, p.

Abella <Define ctx2 : olist -> olist -> prop by ctx2 nil nil; nabla x p, ctx2 (bred x x :: G) (path x p :: D) := ctx2 G D; nabla x, ctx2 ((pi u\bred N u => bred x u) :: G) ((pi q\path N q => path x q) :: D) := ctx2 G D.

Abella <Define name : tm -> prop by nabla n, name n.

Abella <Define fresh : tm -> tm -> prop by nabla n, fresh n X.

Abella <Define pname : p -> prop by nabla p, pname p.

Abella <Theorem ctx2_mem_G : forall G D F, ctx2 G D -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N).

============================ forall G D F, ctx2 G D -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <induction on 1.

IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ============================ forall G D F, ctx2 G D @ -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <intros.

Variables: G D F IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H1 : ctx2 G D @ H2 : member F G ============================ (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <case H1.

Subgoal 1: Variables: F IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H2 : member F nil ============================ (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) Subgoal 2 is: (exists x, F n1 n2 = bred x x /\ name x) \/ (exists x N, F n1 n2 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <case H2.

Subgoal 2: Variables: F D1 G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H2 : member (F n1 n2) (bred n1 n1 :: G1) H3 : ctx2 G1 D1 * ============================ (exists x, F n1 n2 = bred x x /\ name x) \/ (exists x N, F n1 n2 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <case H2.

Subgoal 2.1: Variables: D1 G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * ============================ (exists x, bred n1 n1 = bred x x /\ name x) \/ (exists x N, bred n1 n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 2.2 is: (exists x, F n1 n2 = bred x x /\ name x) \/ (exists x N, F n1 n2 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <search.

Subgoal 2.2: Variables: F D1 G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1 n2) G1 ============================ (exists x, F n1 n2 = bred x x /\ name x) \/ (exists x N, F n1 n2 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <apply IH to H3 H4.

Subgoal 2.2: Variables: F D1 G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1 n2) G1 H5 : (exists x, F n1 n2 = bred x x /\ name x) \/ (exists x N, F n1 n2 = pi u\bred N u => bred x u /\ fresh x N) ============================ (exists x, F n1 n2 = bred x x /\ name x) \/ (exists x N, F n1 n2 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <case H5.

Subgoal 2.2.1: Variables: D1 G1 x IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (bred (x n1) (x n1)) G1 H6 : name (x n1) ============================ (exists x1, bred (x n1) (x n1) = bred x1 x1 /\ name x1) \/ (exists x1 N, bred (x n1) (x n1) = pi u\bred N u => bred x1 u /\ fresh x1 N) Subgoal 2.2.2 is: (exists x1, pi u\bred (N n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N1, pi u\bred (N n1) u => bred (x n1) u = pi u\bred N1 u => bred x1 u /\ fresh x1 N1) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <search.

Subgoal 2.2.2: Variables: D1 G1 x N IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (pi u\bred (N n1) u => bred (x n1) u) G1 H6 : fresh (x n1) (N n1) ============================ (exists x1, pi u\bred (N n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N1, pi u\bred (N n1) u => bred (x n1) u = pi u\bred N1 u => bred x1 u /\ fresh x1 N1) Subgoal 3 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <search.

Subgoal 3: Variables: F D1 N G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H2 : member (F n1) ((pi u\bred N u => bred n1 u) :: G1) H3 : ctx2 G1 D1 * ============================ (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <case H2.

Subgoal 3.1: Variables: D1 N G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * ============================ (exists x, pi u\bred N u => bred n1 u = bred x x /\ name x) \/ (exists x N1, pi u\bred N u => bred n1 u = pi u\bred N1 u => bred x u /\ fresh x N1) Subgoal 3.2 is: (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <search.

Subgoal 3.2: Variables: F D1 N G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1) G1 ============================ (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <apply IH to H3 H4.

Subgoal 3.2: Variables: F D1 N G1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1) G1 H5 : (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ============================ (exists x, F n1 = bred x x /\ name x) \/ (exists x N, F n1 = pi u\bred N u => bred x u /\ fresh x N) ctx2_mem_G <case H5.

Subgoal 3.2.1: Variables: D1 N G1 x IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (bred (x n1) (x n1)) G1 H6 : name (x n1) ============================ (exists x1, bred (x n1) (x n1) = bred x1 x1 /\ name x1) \/ (exists x1 N, bred (x n1) (x n1) = pi u\bred N u => bred x1 u /\ fresh x1 N) Subgoal 3.2.2 is: (exists x1, pi u\bred (N1 n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N, pi u\bred (N1 n1) u => bred (x n1) u = pi u\bred N u => bred x1 u /\ fresh x1 N) ctx2_mem_G <search.

Subgoal 3.2.2: Variables: D1 N G1 x N1 IH : forall G D F, ctx2 G D * -> member F G -> (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (pi u\bred (N1 n1) u => bred (x n1) u) G1 H6 : fresh (x n1) (N1 n1) ============================ (exists x1, pi u\bred (N1 n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N, pi u\bred (N1 n1) u => bred (x n1) u = pi u\bred N u => bred x1 u /\ fresh x1 N) ctx2_mem_G <search.Proof completed.

Abella <Theorem ctx2_mem_D : forall G D F, ctx2 G D -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N).

============================ forall G D F, ctx2 G D -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <induction on 1.

IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ============================ forall G D F, ctx2 G D @ -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <intros.

Variables: G D F IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H1 : ctx2 G D @ H2 : member F D ============================ (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <case H1.

Subgoal 1: Variables: F IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H2 : member F nil ============================ (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) Subgoal 2 is: (exists x p, F n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 n2 = pi q\path N q => path x q /\ fresh x N) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <case H2.

Subgoal 2: Variables: F D1 G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H2 : member (F n1 n2) (path n1 n2 :: D1) H3 : ctx2 G1 D1 * ============================ (exists x p, F n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 n2 = pi q\path N q => path x q /\ fresh x N) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <case H2.

Subgoal 2.1: Variables: D1 G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * ============================ (exists x p, path n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, path n1 n2 = pi q\path N q => path x q /\ fresh x N) Subgoal 2.2 is: (exists x p, F n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 n2 = pi q\path N q => path x q /\ fresh x N) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <search.

Subgoal 2.2: Variables: F D1 G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1 n2) D1 ============================ (exists x p, F n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 n2 = pi q\path N q => path x q /\ fresh x N) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <apply IH to H3 H4.

Subgoal 2.2: Variables: F D1 G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1 n2) D1 H5 : (exists x p, F n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 n2 = pi q\path N q => path x q /\ fresh x N) ============================ (exists x p, F n1 n2 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 n2 = pi q\path N q => path x q /\ fresh x N) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <case H5.

Subgoal 2.2.1: Variables: D1 G1 x p IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (path (x n1) (p n2)) D1 H6 : name (x n1) H7 : pname (p n2) ============================ (exists x1 p1, path (x n1) (p n2) = path x1 p1 /\ name x1 /\ pname p1) \/ (exists x1 N, path (x n1) (p n2) = pi q\path N q => path x1 q /\ fresh x1 N) Subgoal 2.2.2 is: (exists x1 p, pi q\path (N n1) q => path (x n1) q = path x1 p /\ name x1 /\ pname p) \/ (exists x1 N1, pi q\path (N n1) q => path (x n1) q = pi q\path N1 q => path x1 q /\ fresh x1 N1) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <search.

Subgoal 2.2.2: Variables: D1 G1 x N IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (pi q\path (N n1) q => path (x n1) q) D1 H6 : fresh (x n1) (N n1) ============================ (exists x1 p, pi q\path (N n1) q => path (x n1) q = path x1 p /\ name x1 /\ pname p) \/ (exists x1 N1, pi q\path (N n1) q => path (x n1) q = pi q\path N1 q => path x1 q /\ fresh x1 N1) Subgoal 3 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <search.

Subgoal 3: Variables: F D1 N G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H2 : member (F n1) ((pi q\path N q => path n1 q) :: D1) H3 : ctx2 G1 D1 * ============================ (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <case H2.

Subgoal 3.1: Variables: D1 N G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * ============================ (exists x p, pi q\path N q => path n1 q = path x p /\ name x /\ pname p) \/ (exists x N1, pi q\path N q => path n1 q = pi q\path N1 q => path x q /\ fresh x N1) Subgoal 3.2 is: (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <search.

Subgoal 3.2: Variables: F D1 N G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1) D1 ============================ (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <apply IH to H3 H4.

Subgoal 3.2: Variables: F D1 N G1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (F n1) D1 H5 : (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ============================ (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ctx2_mem_D <case H5.

Subgoal 3.2.1: Variables: D1 N G1 x p IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (path (x n1) p) D1 H6 : name (x n1) H7 : pname p ============================ (exists x1 p1, path (x n1) p = path x1 p1 /\ name x1 /\ pname p1) \/ (exists x1 N, path (x n1) p = pi q\path N q => path x1 q /\ fresh x1 N) Subgoal 3.2.2 is: (exists x1 p, pi q\path (N1 n1) q => path (x n1) q = path x1 p /\ name x1 /\ pname p) \/ (exists x1 N, pi q\path (N1 n1) q => path (x n1) q = pi q\path N q => path x1 q /\ fresh x1 N) ctx2_mem_D <search.

Subgoal 3.2.2: Variables: D1 N G1 x N1 IH : forall G D F, ctx2 G D * -> member F D -> (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) H3 : ctx2 G1 D1 * H4 : member (pi q\path (N1 n1) q => path (x n1) q) D1 H6 : fresh (x n1) (N1 n1) ============================ (exists x1 p, pi q\path (N1 n1) q => path (x n1) q = path x1 p /\ name x1 /\ pname p) \/ (exists x1 N, pi q\path (N1 n1) q => path (x n1) q = pi q\path N q => path x1 q /\ fresh x1 N) ctx2_mem_D <search.Proof completed.

Abella <Theorem ctx2_uniform : forall G D X, nabla n, ctx2 (G n) (D n) -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n).

============================ forall G D X, nabla n, ctx2 (G n) (D n) -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) ctx2_uniform <induction on 1.

IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) ============================ forall G D X, nabla n, ctx2 (G n) (D n) @ -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) ctx2_uniform <intros.

Variables: G D X IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H1 : ctx2 (G n1) (D n1) @ H2 : member (pi u\bred X u => bred n1 u) (G n1) ============================ member (pi q\path X q => path n1 q) (D n1) ctx2_uniform <case H1.

Subgoal 1: Variables: X IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H2 : member (pi u\bred X u => bred n1 u) nil ============================ member (pi q\path X q => path n1 q) nil Subgoal 2 is: member (pi q\path (X n2) q => path n1 q) (path n2 n3 :: D1 n1) Subgoal 3 is: member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <case H2.

Subgoal 2: Variables: X D1 G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H2 : member (pi u\bred (X n2) u => bred n1 u) (bred n2 n2 :: G1 n1) H3 : ctx2 (G1 n1) (D1 n1) * ============================ member (pi q\path (X n2) q => path n1 q) (path n2 n3 :: D1 n1) Subgoal 3 is: member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <case H2.

Subgoal 2: Variables: X D1 G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 (G1 n1) (D1 n1) * H4 : member (pi u\bred (X n2) u => bred n1 u) (G1 n1) ============================ member (pi q\path (X n2) q => path n1 q) (path n2 n3 :: D1 n1) Subgoal 3 is: member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <apply IH to H3 H4.

Subgoal 2: Variables: X D1 G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 (G1 n1) (D1 n1) * H4 : member (pi u\bred (X n2) u => bred n1 u) (G1 n1) H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) ============================ member (pi q\path (X n2) q => path n1 q) (path n2 n3 :: D1 n1) Subgoal 3 is: member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <search.

Subgoal 3: Variables: X D1 G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H2 : member (pi u\bred X u => bred n1 u) (bred n1 n1 :: G1) H3 : ctx2 G1 D1 * ============================ member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <case H2.

Subgoal 3: Variables: X D1 G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 G1 D1 * H4 : member (pi u\bred X u => bred n1 u) G1 ============================ member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <apply IH to H3 H4.

Subgoal 3: Variables: X D1 G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 G1 D1 * H4 : member (pi u\bred X u => bred n1 u) G1 H5 : member (pi q\path X q => path n1 q) D1 ============================ member (pi q\path X q => path n1 q) (path n1 n2 :: D1) Subgoal 4 is: member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <search.

Subgoal 4: Variables: X D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H2 : member (pi u\bred (X n2) u => bred n1 u) ((pi u\bred (N n1) u => bred n2 u) :: G1 n1) H3 : ctx2 (G1 n1) (D1 n1) * ============================ member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <case H2.

Subgoal 4: Variables: X D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 (G1 n1) (D1 n1) * H4 : member (pi u\bred (X n2) u => bred n1 u) (G1 n1) ============================ member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <apply IH to H3 H4.

Subgoal 4: Variables: X D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 (G1 n1) (D1 n1) * H4 : member (pi u\bred (X n2) u => bred n1 u) (G1 n1) H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) ============================ member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) Subgoal 5 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <search.

Subgoal 5: Variables: X D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H2 : member (pi u\bred X u => bred n1 u) ((pi u\bred N u => bred n1 u) :: G1) H3 : ctx2 G1 D1 * ============================ member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <case H2.

Subgoal 5.1: Variables: D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 G1 D1 * ============================ member (pi q\path N q => path n1 q) ((pi q\path N q => path n1 q) :: D1) Subgoal 5.2 is: member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <search.

Subgoal 5.2: Variables: X D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 G1 D1 * H4 : member (pi u\bred X u => bred n1 u) G1 ============================ member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <apply IH to H3 H4.

Subgoal 5.2: Variables: X D1 N G1 IH : forall G D X, nabla n, ctx2 (G n) (D n) * -> member (pi u\bred X u => bred n u) (G n) -> member (pi q\path X q => path n q) (D n) H3 : ctx2 G1 D1 * H4 : member (pi u\bred X u => bred n1 u) G1 H5 : member (pi q\path X q => path n1 q) D1 ============================ member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) ctx2_uniform <search.Proof completed.

Abella <Theorem member_prune_D : forall G D E, nabla n, ctx2 G D -> member (E n) D -> (exists F, E = x\F).

============================ forall G D E, nabla n, ctx2 G D -> member (E n) D -> (exists F, E = x\F) member_prune_D <induction on 1.

IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) ============================ forall G D E, nabla n, ctx2 G D @ -> member (E n) D -> (exists F, E = x\F) member_prune_D <intros.

Variables: G D E IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H1 : ctx2 G D @ H2 : member (E n1) D ============================ exists F, E = x\F member_prune_D <case H1.

Subgoal 1: Variables: E IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H2 : member (E n1) nil ============================ exists F, E = x\F Subgoal 2 is: exists F, E n2 n3 = x\F Subgoal 3 is: exists F, E n2 = x\F member_prune_D <case H2.

Subgoal 2: Variables: E D1 G1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H2 : member (E n2 n3 n1) (path n2 n3 :: D1) H3 : ctx2 G1 D1 * ============================ exists F, E n2 n3 = x\F Subgoal 3 is: exists F, E n2 = x\F member_prune_D <case H2.

Subgoal 2.1: Variables: D1 G1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * ============================ exists F, z3\path n2 n3 = x\F Subgoal 2.2 is: exists F, E n2 n3 = x\F Subgoal 3 is: exists F, E n2 = x\F member_prune_D <search.

Subgoal 2.2: Variables: E D1 G1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * H4 : member (E n2 n3 n1) D1 ============================ exists F, E n2 n3 = x\F Subgoal 3 is: exists F, E n2 = x\F member_prune_D <apply IH to H3 H4.

Subgoal 2.2: Variables: D1 G1 F IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * H4 : member (F n1 n3) D1 ============================ exists F1, z3\F z3 n3 = x\F1 Subgoal 3 is: exists F, E n2 = x\F member_prune_D <apply IH to H3 H4.

Subgoal 2.2: Variables: D1 G1 F1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * H4 : member (F1 n3) D1 ============================ exists F2, z3\F1 n3 = x\F2 Subgoal 3 is: exists F, E n2 = x\F member_prune_D <search.

Subgoal 3: Variables: E D1 N G1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H2 : member (E n2 n1) ((pi q\path N q => path n2 q) :: D1) H3 : ctx2 G1 D1 * ============================ exists F, E n2 = x\F member_prune_D <case H2.

Subgoal 3.1: Variables: D1 N G1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * ============================ exists F, z2\pi q\path N q => path n2 q = x\F Subgoal 3.2 is: exists F, E n2 = x\F member_prune_D <search.

Subgoal 3.2: Variables: E D1 N G1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * H4 : member (E n2 n1) D1 ============================ exists F, E n2 = x\F member_prune_D <apply IH to H3 H4.

Subgoal 3.2: Variables: D1 N G1 F IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * H4 : member (F n1) D1 ============================ exists F1, z2\F z2 = x\F1 member_prune_D <apply IH to H3 H4.

Subgoal 3.2: Variables: D1 N G1 F1 IH : forall G D E, nabla n, ctx2 G D * -> member (E n) D -> (exists F, E = x\F) H3 : ctx2 G1 D1 * H4 : member F1 D1 ============================ exists F2, z2\F1 = x\F2 member_prune_D <search.Proof completed.

Abella <Theorem member_D_determinate : forall G D X Y, nabla n, ctx2 (G n) (D n) -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y.

============================ forall G D X Y, nabla n, ctx2 (G n) (D n) -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y member_D_determinate <induction on 1.

IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y ============================ forall G D X Y, nabla n, ctx2 (G n) (D n) @ -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y member_D_determinate <intros.

Variables: G D X Y IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H1 : ctx2 (G n1) (D n1) @ H2 : member (pi q\path X q => path n1 q) (D n1) H3 : member (pi q\path Y q => path n1 q) (D n1) ============================ X = Y member_D_determinate <case H1.

Subgoal 1: Variables: X Y IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H2 : member (pi q\path X q => path n1 q) nil H3 : member (pi q\path Y q => path n1 q) nil ============================ X = Y Subgoal 2 is: X n2 = Y n2 Subgoal 3 is: X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H2.

Subgoal 2: Variables: X Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H2 : member (pi q\path (X n2) q => path n1 q) (path n2 n3 :: D1 n1) H3 : member (pi q\path (Y n2) q => path n1 q) (path n2 n3 :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * ============================ X n2 = Y n2 Subgoal 3 is: X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H2.

Subgoal 2: Variables: X Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H3 : member (pi q\path (Y n2) q => path n1 q) (path n2 n3 :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) ============================ X n2 = Y n2 Subgoal 3 is: X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H3.

Subgoal 2: Variables: X Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) H6 : member (pi q\path (Y n2) q => path n1 q) (D1 n1) ============================ X n2 = Y n2 Subgoal 3 is: X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <apply IH to H4 H5 H6.

Subgoal 2: Variables: Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (Y n2) q => path n1 q) (D1 n1) H6 : member (pi q\path (Y n2) q => path n1 q) (D1 n1) ============================ Y n2 = Y n2 Subgoal 3 is: X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <search.

Subgoal 3: Variables: X Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H2 : member (pi q\path X q => path n1 q) (path n1 n2 :: D1) H3 : member (pi q\path Y q => path n1 q) (path n1 n2 :: D1) H4 : ctx2 G1 D1 * ============================ X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H2.

Subgoal 3: Variables: X Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H3 : member (pi q\path Y q => path n1 q) (path n1 n2 :: D1) H4 : ctx2 G1 D1 * H5 : member (pi q\path X q => path n1 q) D1 ============================ X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H3.

Subgoal 3: Variables: X Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 G1 D1 * H5 : member (pi q\path X q => path n1 q) D1 H6 : member (pi q\path Y q => path n1 q) D1 ============================ X = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <apply IH to H4 H5 H6.

Subgoal 3: Variables: Y D1 G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 G1 D1 * H5 : member (pi q\path Y q => path n1 q) D1 H6 : member (pi q\path Y q => path n1 q) D1 ============================ Y = Y Subgoal 4 is: X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <search.

Subgoal 4: Variables: X Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H2 : member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) H3 : member (pi q\path (Y n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * ============================ X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H2.

Subgoal 4: Variables: X Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H3 : member (pi q\path (Y n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) ============================ X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <case H3.

Subgoal 4: Variables: X Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) H6 : member (pi q\path (Y n2) q => path n1 q) (D1 n1) ============================ X n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <apply IH to H4 H5 H6.

Subgoal 4: Variables: Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (Y n2) q => path n1 q) (D1 n1) H6 : member (pi q\path (Y n2) q => path n1 q) (D1 n1) ============================ Y n2 = Y n2 Subgoal 5 is: X = Y member_D_determinate <search.

Subgoal 5: Variables: X Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H2 : member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) H3 : member (pi q\path Y q => path n1 q) ((pi q\path N q => path n1 q) :: D1) H4 : ctx2 G1 D1 * ============================ X = Y member_D_determinate <case H2.

Subgoal 5.1: Variables: Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H3 : member (pi q\path Y q => path n1 q) ((pi q\path N q => path n1 q) :: D1) H4 : ctx2 G1 D1 * ============================ N = Y Subgoal 5.2 is: X = Y member_D_determinate <case H3.

Subgoal 5.1.1: Variables: D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 G1 D1 * ============================ N = N Subgoal 5.1.2 is: N = Y Subgoal 5.2 is: X = Y member_D_determinate <search.

Subgoal 5.1.2: Variables: Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H4 : ctx2 G1 D1 * H5 : member (pi q\path Y q => path n1 q) D1 ============================ N = Y Subgoal 5.2 is: X = Y member_D_determinate <apply member_prune_D to H4 H5.

Subgoal 5.2: Variables: X Y D1 N G1 IH : forall G D X Y, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (pi q\path Y q => path n q) (D n) -> X = Y H3 : member (pi q\path Y q => path n1 q) ((pi q\path N q => path n1 q) :: D1) H4 : ctx2 G1 D1 * H5 : member (pi q\path X q => path n1 q) D1 ============================ X = Y member_D_determinate <apply member_prune_D to H4 H5.Proof completed.

Abella <Theorem member_D_discrim : forall G D X P, nabla n, ctx2 (G n) (D n) -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false.

============================ forall G D X P, nabla n, ctx2 (G n) (D n) -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false member_D_discrim <induction on 1.

IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false ============================ forall G D X P, nabla n, ctx2 (G n) (D n) @ -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false member_D_discrim <intros.

Variables: G D X P IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H1 : ctx2 (G n1) (D n1) @ H2 : member (pi q\path X q => path n1 q) (D n1) H3 : member (path n1 P) (D n1) ============================ false member_D_discrim <case H1.

Subgoal 1: Variables: X P IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H2 : member (pi q\path X q => path n1 q) nil H3 : member (path n1 P) nil ============================ false Subgoal 2 is: false Subgoal 3 is: false Subgoal 4 is: false Subgoal 5 is: false member_D_discrim <case H2.

Subgoal 2: Variables: X P D1 G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H2 : member (pi q\path (X n2) q => path n1 q) (path n2 n3 :: D1 n1) H3 : member (path n1 (P n3)) (path n2 n3 :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * ============================ false Subgoal 3 is: false Subgoal 4 is: false Subgoal 5 is: false member_D_discrim <case H2.

Subgoal 2: Variables: X P D1 G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H3 : member (path n1 (P n3)) (path n2 n3 :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) ============================ false Subgoal 3 is: false Subgoal 4 is: false Subgoal 5 is: false member_D_discrim <case H3.

Subgoal 2: Variables: X P D1 G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) H6 : member (path n1 (P n3)) (D1 n1) ============================ false Subgoal 3 is: false Subgoal 4 is: false Subgoal 5 is: false member_D_discrim <apply IH to H4 H5 H6.

Subgoal 3: Variables: X P D1 G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H2 : member (pi q\path X q => path n1 q) (path n1 n2 :: D1) H3 : member (path n1 (P n2)) (path n1 n2 :: D1) H4 : ctx2 G1 D1 * ============================ false Subgoal 4 is: false Subgoal 5 is: false member_D_discrim <case H2.

Subgoal 3: Variables: X P D1 G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H3 : member (path n1 (P n2)) (path n1 n2 :: D1) H4 : ctx2 G1 D1 * H5 : member (pi q\path X q => path n1 q) D1 ============================ false Subgoal 4 is: false Subgoal 5 is: false member_D_discrim <apply member_prune_D to H4 H5.

Subgoal 4: Variables: X P D1 N G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H2 : member (pi q\path (X n2) q => path n1 q) ((pi q\path (N n1) q => path n2 q) :: D1 n1) H3 : member (path n1 P) ((pi q\path (N n1) q => path n2 q) :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * ============================ false Subgoal 5 is: false member_D_discrim <case H2.

Subgoal 4: Variables: X P D1 N G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H3 : member (path n1 P) ((pi q\path (N n1) q => path n2 q) :: D1 n1) H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) ============================ false Subgoal 5 is: false member_D_discrim <case H3.

Subgoal 4: Variables: X P D1 N G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H4 : ctx2 (G1 n1) (D1 n1) * H5 : member (pi q\path (X n2) q => path n1 q) (D1 n1) H6 : member (path n1 P) (D1 n1) ============================ false Subgoal 5 is: false member_D_discrim <apply IH to H4 H5 H6.

Subgoal 5: Variables: X P D1 N G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H2 : member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) H3 : member (path n1 P) ((pi q\path N q => path n1 q) :: D1) H4 : ctx2 G1 D1 * ============================ false member_D_discrim <case H3.

Subgoal 5: Variables: X P D1 N G1 IH : forall G D X P, nabla n, ctx2 (G n) (D n) * -> member (pi q\path X q => path n q) (D n) -> member (path n P) (D n) -> false H2 : member (pi q\path X q => path n1 q) ((pi q\path N q => path n1 q) :: D1) H4 : ctx2 G1 D1 * H5 : member (path n1 P) D1 ============================ false member_D_discrim <apply member_prune_D to H4 H5.Proof completed.

Abella <Theorem jump_D_invert : forall G D X P, nabla n, ctx2 (G n) (D n) -> member (pi q\path X q => path n q) (D n) -> {D n |- path n P} -> {D n |- path X P}.

============================ forall G D X P, nabla n, ctx2 (G n) (D n) -> member (pi q\path X q => path n q) (D n) -> {D n |- path n P} -> {D n |- path X P} jump_D_invert <intros.

Variables: G D X P H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H3 : {D n1 |- path n1 P} ============================ {D n1 |- path X P} jump_D_invert <case H3.

Variables: G D X P F H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H4 : {D n1, [F n1] |- path n1 P} H5 : member (F n1) (D n1) ============================ {D n1 |- path X P} jump_D_invert <apply ctx2_mem_D to H1 H5.

Variables: G D X P F H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H4 : {D n1, [F n1] |- path n1 P} H5 : member (F n1) (D n1) H6 : (exists x p, F n1 = path x p /\ name x /\ pname p) \/ (exists x N, F n1 = pi q\path N q => path x q /\ fresh x N) ============================ {D n1 |- path X P} jump_D_invert <case H6.

Subgoal 1: Variables: G D X P x p H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H4 : {D n1, [path (x n1) p] |- path n1 P} H5 : member (path (x n1) p) (D n1) H7 : name (x n1) H8 : pname p ============================ {D n1 |- path X P} Subgoal 2 is: {D n1 |- path X P} jump_D_invert <case H4.

Subgoal 1: Variables: G D X P H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H5 : member (path n1 P) (D n1) H7 : name n1 H8 : pname P ============================ {D n1 |- path X P} Subgoal 2 is: {D n1 |- path X P} jump_D_invert <apply member_D_discrim to H1 H2 H5.

Subgoal 2: Variables: G D X P x N H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H4 : {D n1, [pi q\path (N n1) q => path (x n1) q] |- path n1 P} H5 : member (pi q\path (N n1) q => path (x n1) q) (D n1) H7 : fresh (x n1) (N n1) ============================ {D n1 |- path X P} jump_D_invert <case H4.

Subgoal 2: Variables: G D X P N H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H5 : member (pi q\path (N n1) q => path n1 q) (D n1) H7 : fresh n1 (N n1) H8 : {D n1 |- path (N n1) P} ============================ {D n1 |- path X P} jump_D_invert <case H7.

Subgoal 2: Variables: G D X P X1 H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X q => path n1 q) (D n1) H5 : member (pi q\path X1 q => path n1 q) (D n1) H8 : {D n1 |- path X1 P} ============================ {D n1 |- path X P} jump_D_invert <apply member_D_determinate to H1 H2 H5.

Subgoal 2: Variables: G D P X1 H1 : ctx2 (G n1) (D n1) H2 : member (pi q\path X1 q => path n1 q) (D n1) H5 : member (pi q\path X1 q => path n1 q) (D n1) H8 : {D n1 |- path X1 P} ============================ {D n1 |- path X1 P} jump_D_invert <search.Proof completed.

Abella <Theorem bred_ltr : forall G D M N P, ctx2 G D -> {G |- bred M N} -> {D |- path M P} -> {D |- path N P}.

============================ forall G D M N P, ctx2 G D -> {G |- bred M N} -> {D |- path M P} -> {D |- path N P} bred_ltr <induction on 2.

IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} ============================ forall G D M N P, ctx2 G D -> {G |- bred M N}@ -> {D |- path M P} -> {D |- path N P} bred_ltr <intros.

Variables: G D M N P IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path M P} ============================ {D |- path N P} bred_ltr <case H2 (keep).

Subgoal 1: Variables: G D P U M1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H3 : {D |- path (abs M1) P} H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* ============================ {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H3.

Subgoal 1.1: Variables: G D U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, path n1 n2 |- path (M1 n1) (P1 n2)} ============================ {D |- path (abs U) (bnd P1)} Subgoal 1.2 is: {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply IH to _ H4 H5.

Subgoal 1.1: Variables: G D U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, path n1 n2 |- path (M1 n1) (P1 n2)} H6 : {D, path n1 n2 |- path (U n1) (P1 n2)} ============================ {D |- path (abs U) (bnd P1)} Subgoal 1.2 is: {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <search.

Subgoal 1.2: Variables: G D P U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [F] |- path (abs M1) P} H6 : member F D ============================ {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply ctx2_mem_D to H1 H6.

Subgoal 1.2: Variables: G D P U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [F] |- path (abs M1) P} H6 : member F D H7 : (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ============================ {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H7.

Subgoal 1.2.1: Variables: G D P U M1 x p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [path x p] |- path (abs M1) P} H6 : member (path x p) D H8 : name x H9 : pname p ============================ {D |- path (abs U) P} Subgoal 1.2.2 is: {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H8.

Subgoal 1.2.1: Variables: G D P U M1 p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n2) (D n2) H2 : {G n2 |- bred (abs (M1 n2)) (abs (U n2))}@ H4 : {G n2, bred n1 n1 |- bred (M1 n2 n1) (U n2 n1)}* H5 : {D n2, [path n2 p] |- path (abs (M1 n2)) P} H6 : member (path n2 p) (D n2) H9 : pname p ============================ {D n2 |- path (abs (U n2)) P} Subgoal 1.2.2 is: {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H5.

Subgoal 1.2.2: Variables: G D P U M1 x N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [pi q\path N1 q => path x q] |- path (abs M1) P} H6 : member (pi q\path N1 q => path x q) D H8 : fresh x N1 ============================ {D |- path (abs U) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H8.

Subgoal 1.2.2: Variables: G D P U M1 X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n2) (D n2) H2 : {G n2 |- bred (abs (M1 n2)) (abs (U n2))}@ H4 : {G n2, bred n1 n1 |- bred (M1 n2 n1) (U n2 n1)}* H5 : {D n2, [pi q\path X q => path n2 q] |- path (abs (M1 n2)) P} H6 : member (pi q\path X q => path n2 q) (D n2) ============================ {D n2 |- path (abs (U n2)) P} Subgoal 2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H5.

Subgoal 2: Variables: G D P V N1 U M1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H3 : {D |- path (app M1 N1) P} H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* ============================ {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H3.

Subgoal 2.1: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path M1 P1} ============================ {D |- path (app U V) (left P1)} Subgoal 2.2 is: {D |- path (app U V) (right P1)} Subgoal 2.3 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply IH to _ H4 H6.

Subgoal 2.1: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path M1 P1} H7 : {D |- path U P1} ============================ {D |- path (app U V) (left P1)} Subgoal 2.2 is: {D |- path (app U V) (right P1)} Subgoal 2.3 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <search.

Subgoal 2.2: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path N1 P1} ============================ {D |- path (app U V) (right P1)} Subgoal 2.3 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply IH to _ H5 H6.

Subgoal 2.2: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path N1 P1} H7 : {D |- path V P1} ============================ {D |- path (app U V) (right P1)} Subgoal 2.3 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <search.

Subgoal 2.3: Variables: G D P V N1 U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [F] |- path (app M1 N1) P} H7 : member F D ============================ {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply ctx2_mem_D to H1 H7.

Subgoal 2.3: Variables: G D P V N1 U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [F] |- path (app M1 N1) P} H7 : member F D H8 : (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ============================ {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H8.

Subgoal 2.3.1: Variables: G D P V N1 U M1 x p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [path x p] |- path (app M1 N1) P} H7 : member (path x p) D H9 : name x H10 : pname p ============================ {D |- path (app U V) P} Subgoal 2.3.2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H9.

Subgoal 2.3.1: Variables: G D P V N1 U M1 p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (app (M1 n1) (N1 n1)) (app (U n1) (V n1))}@ H4 : {G n1 |- bred (M1 n1) (U n1)}* H5 : {G n1 |- bred (N1 n1) (V n1)}* H6 : {D n1, [path n1 p] |- path (app (M1 n1) (N1 n1)) P} H7 : member (path n1 p) (D n1) H10 : pname p ============================ {D n1 |- path (app (U n1) (V n1)) P} Subgoal 2.3.2 is: {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H6.

Subgoal 2.3.2: Variables: G D P V N1 U M1 x N2 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [pi q\path N2 q => path x q] |- path (app M1 N1) P} H7 : member (pi q\path N2 q => path x q) D H9 : fresh x N2 ============================ {D |- path (app U V) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H9.

Subgoal 2.3.2: Variables: G D P V N1 U M1 X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (app (M1 n1) (N1 n1)) (app (U n1) (V n1))}@ H4 : {G n1 |- bred (M1 n1) (U n1)}* H5 : {G n1 |- bred (N1 n1) (V n1)}* H6 : {D n1, [pi q\path X q => path n1 q] |- path (app (M1 n1) (N1 n1)) P} H7 : member (pi q\path X q => path n1 q) (D n1) ============================ {D n1 |- path (app (U n1) (V n1)) P} Subgoal 3 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H6.

Subgoal 3: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H3 : {D |- path (beta R N1) P} H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* ============================ {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H3.

Subgoal 3.1: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path (R n1) P} ============================ {D |- path N P} Subgoal 3.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply IH to _ H4 H5.

Subgoal 3.1: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path (R n1) P} H6 : {D, pi q\path N1 q => path n1 q |- path N P} ============================ {D |- path N P} Subgoal 3.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <inst H6 with n1 = N1.

Subgoal 3.1: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path (R n1) P} H6 : {D, pi q\path N1 q => path n1 q |- path N P} H7 : {D, pi q\path N1 q => path N1 q |- path N P} ============================ {D |- path N P} Subgoal 3.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <assert {D |- pi q\path N1 q => path N1 q}.

Subgoal 3.1: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path (R n1) P} H6 : {D, pi q\path N1 q => path n1 q |- path N P} H7 : {D, pi q\path N1 q => path N1 q |- path N P} H8 : {D |- pi q\path N1 q => path N1 q} ============================ {D |- path N P} Subgoal 3.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <cut H7 with H8.

Subgoal 3.1: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path (R n1) P} H6 : {D, pi q\path N1 q => path n1 q |- path N P} H7 : {D, pi q\path N1 q => path N1 q |- path N P} H8 : {D |- pi q\path N1 q => path N1 q} H9 : {D |- path N P} ============================ {D |- path N P} Subgoal 3.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <search.

Subgoal 3.2: Variables: G D N P R N1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, [F] |- path (beta R N1) P} H6 : member F D ============================ {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <apply ctx2_mem_D to H1 H6.

Subgoal 3.2: Variables: G D N P R N1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, [F] |- path (beta R N1) P} H6 : member F D H7 : (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ============================ {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H7.

Subgoal 3.2.1: Variables: G D N P R N1 x p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, [path x p] |- path (beta R N1) P} H6 : member (path x p) D H8 : name x H9 : pname p ============================ {D |- path N P} Subgoal 3.2.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H8.

Subgoal 3.2.1: Variables: G D N P R N1 p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n2) (D n2) H2 : {G n2 |- bred (beta (R n2) (N1 n2)) (N n2)}@ H4 : {G n2, pi u\bred (N1 n2) u => bred n1 u |- bred (R n2 n1) (N n2)}* H5 : {D n2, [path n2 p] |- path (beta (R n2) (N1 n2)) P} H6 : member (path n2 p) (D n2) H9 : pname p ============================ {D n2 |- path (N n2) P} Subgoal 3.2.2 is: {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H5.

Subgoal 3.2.2: Variables: G D N P R N1 x N2 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, [pi q\path N2 q => path x q] |- path (beta R N1) P} H6 : member (pi q\path N2 q => path x q) D H8 : fresh x N2 ============================ {D |- path N P} Subgoal 4 is: {D |- path N P} bred_ltr <case H8.

Subgoal 3.2.2: Variables: G D N P R N1 X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n2) (D n2) H2 : {G n2 |- bred (beta (R n2) (N1 n2)) (N n2)}@ H4 : {G n2, pi u\bred (N1 n2) u => bred n1 u |- bred (R n2 n1) (N n2)}* H5 : {D n2, [pi q\path X q => path n2 q] |- path (beta (R n2) (N1 n2)) P} H6 : member (pi q\path X q => path n2 q) (D n2) ============================ {D n2 |- path (N n2) P} Subgoal 4 is: {D |- path N P} bred_ltr <case H5.

Subgoal 4: Variables: G D M N P F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path M P} H4 : {G, [F] |- bred M N}* H5 : member F G ============================ {D |- path N P} bred_ltr <apply ctx2_mem_G to H1 H5.

Subgoal 4: Variables: G D M N P F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path M P} H4 : {G, [F] |- bred M N}* H5 : member F G H6 : (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ============================ {D |- path N P} bred_ltr <case H6.

Subgoal 4.1: Variables: G D M N P x IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path M P} H4 : {G, [bred x x] |- bred M N}* H5 : member (bred x x) G H7 : name x ============================ {D |- path N P} Subgoal 4.2 is: {D |- path N P} bred_ltr <case H7.

Subgoal 4.1: Variables: G D M N P IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (M n1) (N n1)}@ H3 : {D n1 |- path (M n1) P} H4 : {G n1, [bred n1 n1] |- bred (M n1) (N n1)}* H5 : member (bred n1 n1) (G n1) ============================ {D n1 |- path (N n1) P} Subgoal 4.2 is: {D |- path N P} bred_ltr <case H4.

Subgoal 4.1: Variables: G D P IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 n1}@ H3 : {D n1 |- path n1 P} H5 : member (bred n1 n1) (G n1) ============================ {D n1 |- path n1 P} Subgoal 4.2 is: {D |- path N P} bred_ltr <search.

Subgoal 4.2: Variables: G D M N P x N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path M P} H4 : {G, [pi u\bred N1 u => bred x u] |- bred M N}* H5 : member (pi u\bred N1 u => bred x u) G H7 : fresh x N1 ============================ {D |- path N P} bred_ltr <case H7.

Subgoal 4.2: Variables: G D M N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (M n1) (N n1)}@ H3 : {D n1 |- path (M n1) P} H4 : {G n1, [pi u\bred X u => bred n1 u] |- bred (M n1) (N n1)}* H5 : member (pi u\bred X u => bred n1 u) (G n1) ============================ {D n1 |- path (N n1) P} bred_ltr <case H4.

Subgoal 4.2: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path n1 P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* ============================ {D n1 |- path (N n1) P} bred_ltr <assert {D n1 |- path X P}.

Subgoal 4.2.1: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path n1 P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* ============================ {D n1 |- path X P} Subgoal 4.2 is: {D n1 |- path (N n1) P} bred_ltr <apply ctx2_uniform to H1 H5.

Subgoal 4.2.1: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path n1 P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* H9 : member (pi q\path X q => path n1 q) (D n1) ============================ {D n1 |- path X P} Subgoal 4.2 is: {D n1 |- path (N n1) P} bred_ltr <apply jump_D_invert to H1 H9 H3.

Subgoal 4.2.1: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path n1 P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* H9 : member (pi q\path X q => path n1 q) (D n1) H10 : {D n1 |- path X P} ============================ {D n1 |- path X P} Subgoal 4.2 is: {D n1 |- path (N n1) P} bred_ltr <search.

Subgoal 4.2: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path n1 P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* H9 : {D n1 |- path X P} ============================ {D n1 |- path (N n1) P} bred_ltr <apply IH to H1 H8 H9.

Subgoal 4.2: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path M P} -> {D |- path N P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path n1 P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* H9 : {D n1 |- path X P} H10 : {D n1 |- path (N n1) P} ============================ {D n1 |- path (N n1) P} bred_ltr <search.Proof completed.

Abella <Theorem bred_rtl : forall G D M N P, ctx2 G D -> {G |- bred M N} -> {D |- path N P} -> {D |- path M P}.

============================ forall G D M N P, ctx2 G D -> {G |- bred M N} -> {D |- path N P} -> {D |- path M P} bred_rtl <induction on 2.

IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} ============================ forall G D M N P, ctx2 G D -> {G |- bred M N}@ -> {D |- path N P} -> {D |- path M P} bred_rtl <intros.

Variables: G D M N P IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path N P} ============================ {D |- path M P} bred_rtl <case H2 (keep).

Subgoal 1: Variables: G D P U M1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H3 : {D |- path (abs U) P} H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* ============================ {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H3.

Subgoal 1.1: Variables: G D U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, path n1 n2 |- path (U n1) (P1 n2)} ============================ {D |- path (abs M1) (bnd P1)} Subgoal 1.2 is: {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <apply IH to _ H4 H5.

Subgoal 1.1: Variables: G D U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, path n1 n2 |- path (U n1) (P1 n2)} H6 : {D, path n1 n2 |- path (M1 n1) (P1 n2)} ============================ {D |- path (abs M1) (bnd P1)} Subgoal 1.2 is: {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <search.

Subgoal 1.2: Variables: G D P U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [F] |- path (abs U) P} H6 : member F D ============================ {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <apply ctx2_mem_D to H1 H6.

Subgoal 1.2: Variables: G D P U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [F] |- path (abs U) P} H6 : member F D H7 : (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ============================ {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H7.

Subgoal 1.2.1: Variables: G D P U M1 x p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [path x p] |- path (abs U) P} H6 : member (path x p) D H8 : name x H9 : pname p ============================ {D |- path (abs M1) P} Subgoal 1.2.2 is: {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H8.

Subgoal 1.2.1: Variables: G D P U M1 p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n2) (D n2) H2 : {G n2 |- bred (abs (M1 n2)) (abs (U n2))}@ H4 : {G n2, bred n1 n1 |- bred (M1 n2 n1) (U n2 n1)}* H5 : {D n2, [path n2 p] |- path (abs (U n2)) P} H6 : member (path n2 p) (D n2) H9 : pname p ============================ {D n2 |- path (abs (M1 n2)) P} Subgoal 1.2.2 is: {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H5.

Subgoal 1.2.2: Variables: G D P U M1 x N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (abs M1) (abs U)}@ H4 : {G, bred n1 n1 |- bred (M1 n1) (U n1)}* H5 : {D, [pi q\path N1 q => path x q] |- path (abs U) P} H6 : member (pi q\path N1 q => path x q) D H8 : fresh x N1 ============================ {D |- path (abs M1) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H8.

Subgoal 1.2.2: Variables: G D P U M1 X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n2) (D n2) H2 : {G n2 |- bred (abs (M1 n2)) (abs (U n2))}@ H4 : {G n2, bred n1 n1 |- bred (M1 n2 n1) (U n2 n1)}* H5 : {D n2, [pi q\path X q => path n2 q] |- path (abs (U n2)) P} H6 : member (pi q\path X q => path n2 q) (D n2) ============================ {D n2 |- path (abs (M1 n2)) P} Subgoal 2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H5.

Subgoal 2: Variables: G D P V N1 U M1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H3 : {D |- path (app U V) P} H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* ============================ {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H3.

Subgoal 2.1: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path U P1} ============================ {D |- path (app M1 N1) (left P1)} Subgoal 2.2 is: {D |- path (app M1 N1) (right P1)} Subgoal 2.3 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <apply IH to _ H4 H6.

Subgoal 2.1: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path U P1} H7 : {D |- path M1 P1} ============================ {D |- path (app M1 N1) (left P1)} Subgoal 2.2 is: {D |- path (app M1 N1) (right P1)} Subgoal 2.3 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <search.

Subgoal 2.2: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path V P1} ============================ {D |- path (app M1 N1) (right P1)} Subgoal 2.3 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <apply IH to _ H5 H6.

Subgoal 2.2: Variables: G D V N1 U M1 P1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D |- path V P1} H7 : {D |- path N1 P1} ============================ {D |- path (app M1 N1) (right P1)} Subgoal 2.3 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <search.

Subgoal 2.3: Variables: G D P V N1 U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [F] |- path (app U V) P} H7 : member F D ============================ {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <apply ctx2_mem_D to H1 H7.

Subgoal 2.3: Variables: G D P V N1 U M1 F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [F] |- path (app U V) P} H7 : member F D H8 : (exists x p, F = path x p /\ name x /\ pname p) \/ (exists x N, F = pi q\path N q => path x q /\ fresh x N) ============================ {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H8.

Subgoal 2.3.1: Variables: G D P V N1 U M1 x p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [path x p] |- path (app U V) P} H7 : member (path x p) D H9 : name x H10 : pname p ============================ {D |- path (app M1 N1) P} Subgoal 2.3.2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H9.

Subgoal 2.3.1: Variables: G D P V N1 U M1 p IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (app (M1 n1) (N1 n1)) (app (U n1) (V n1))}@ H4 : {G n1 |- bred (M1 n1) (U n1)}* H5 : {G n1 |- bred (N1 n1) (V n1)}* H6 : {D n1, [path n1 p] |- path (app (U n1) (V n1)) P} H7 : member (path n1 p) (D n1) H10 : pname p ============================ {D n1 |- path (app (M1 n1) (N1 n1)) P} Subgoal 2.3.2 is: {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H6.

Subgoal 2.3.2: Variables: G D P V N1 U M1 x N2 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (app M1 N1) (app U V)}@ H4 : {G |- bred M1 U}* H5 : {G |- bred N1 V}* H6 : {D, [pi q\path N2 q => path x q] |- path (app U V) P} H7 : member (pi q\path N2 q => path x q) D H9 : fresh x N2 ============================ {D |- path (app M1 N1) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H9.

Subgoal 2.3.2: Variables: G D P V N1 U M1 X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (app (M1 n1) (N1 n1)) (app (U n1) (V n1))}@ H4 : {G n1 |- bred (M1 n1) (U n1)}* H5 : {G n1 |- bred (N1 n1) (V n1)}* H6 : {D n1, [pi q\path X q => path n1 q] |- path (app (U n1) (V n1)) P} H7 : member (pi q\path X q => path n1 q) (D n1) ============================ {D n1 |- path (app (M1 n1) (N1 n1)) P} Subgoal 3 is: {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <case H6.

Subgoal 3: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H3 : {D |- path N P} H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* ============================ {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <assert {D, pi q\path N1 q => path n1 q |- path N P}.

Subgoal 3: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H3 : {D |- path N P} H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path N P} ============================ {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <apply IH to _ H4 H5.

Subgoal 3: Variables: G D N P R N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred (beta R N1) N}@ H3 : {D |- path N P} H4 : {G, pi u\bred N1 u => bred n1 u |- bred (R n1) N}* H5 : {D, pi q\path N1 q => path n1 q |- path N P} H6 : {D, pi q\path N1 q => path n1 q |- path (R n1) P} ============================ {D |- path (beta R N1) P} Subgoal 4 is: {D |- path M P} bred_rtl <search.

Subgoal 4: Variables: G D M N P F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path N P} H4 : {G, [F] |- bred M N}* H5 : member F G ============================ {D |- path M P} bred_rtl <apply ctx2_mem_G to H1 H5.

Subgoal 4: Variables: G D M N P F IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path N P} H4 : {G, [F] |- bred M N}* H5 : member F G H6 : (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ============================ {D |- path M P} bred_rtl <case H6.

Subgoal 4.1: Variables: G D M N P x IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path N P} H4 : {G, [bred x x] |- bred M N}* H5 : member (bred x x) G H7 : name x ============================ {D |- path M P} Subgoal 4.2 is: {D |- path M P} bred_rtl <case H7.

Subgoal 4.1: Variables: G D M N P IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (M n1) (N n1)}@ H3 : {D n1 |- path (N n1) P} H4 : {G n1, [bred n1 n1] |- bred (M n1) (N n1)}* H5 : member (bred n1 n1) (G n1) ============================ {D n1 |- path (M n1) P} Subgoal 4.2 is: {D |- path M P} bred_rtl <case H4.

Subgoal 4.1: Variables: G D P IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 n1}@ H3 : {D n1 |- path n1 P} H5 : member (bred n1 n1) (G n1) ============================ {D n1 |- path n1 P} Subgoal 4.2 is: {D |- path M P} bred_rtl <search.

Subgoal 4.2: Variables: G D M N P x N1 IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 G D H2 : {G |- bred M N}@ H3 : {D |- path N P} H4 : {G, [pi u\bred N1 u => bred x u] |- bred M N}* H5 : member (pi u\bred N1 u => bred x u) G H7 : fresh x N1 ============================ {D |- path M P} bred_rtl <case H7.

Subgoal 4.2: Variables: G D M N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred (M n1) (N n1)}@ H3 : {D n1 |- path (N n1) P} H4 : {G n1, [pi u\bred X u => bred n1 u] |- bred (M n1) (N n1)}* H5 : member (pi u\bred X u => bred n1 u) (G n1) ============================ {D n1 |- path (M n1) P} bred_rtl <case H4.

Subgoal 4.2: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path (N n1) P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* ============================ {D n1 |- path n1 P} bred_rtl <apply IH to H1 H8 H3.

Subgoal 4.2: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path (N n1) P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* H9 : {D n1 |- path X P} ============================ {D n1 |- path n1 P} bred_rtl <apply ctx2_uniform to H1 H5.

Subgoal 4.2: Variables: G D N P X IH : forall G D M N P, ctx2 G D -> {G |- bred M N}* -> {D |- path N P} -> {D |- path M P} H1 : ctx2 (G n1) (D n1) H2 : {G n1 |- bred n1 (N n1)}@ H3 : {D n1 |- path (N n1) P} H5 : member (pi u\bred X u => bred n1 u) (G n1) H8 : {G n1 |- bred X (N n1)}* H9 : {D n1 |- path X P} H10 : member (pi q\path X q => path n1 q) (D n1) ============================ {D n1 |- path n1 P} bred_rtl <search.Proof completed.

Abella <Define bfctx : olist -> olist -> prop by bfctx nil nil; nabla n p, bfctx (bfree n :: L) (path n p :: K) := bfctx L K.

Abella <Theorem member_prune_path : forall E L, nabla x, member (E x) L -> (exists F, E = y\F).

============================ forall E L, nabla x, member (E x) L -> (exists F, E = y\F) member_prune_path <induction on 1.

IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F) ============================ forall E L, nabla x, member (E x) L @ -> (exists F, E = y\F) member_prune_path <intros.

Variables: E L IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F) H1 : member (E n1) L @ ============================ exists F, E = y\F member_prune_path <case H1.

Subgoal 1: Variables: L3 L2 IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F) ============================ exists F, z1\L2 = y\F Subgoal 2 is: exists F, E = y\F member_prune_path <search.

Subgoal 2: Variables: E L3 L2 IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F) H2 : member (E n1) L3 * ============================ exists F, E = y\F member_prune_path <apply IH to H2.

Subgoal 2: Variables: L3 L2 F IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F) H2 : member F L3 * ============================ exists F1, z1\F = y\F1 member_prune_path <search.Proof completed.

Abella <Theorem bfctx_member1 : forall X L K, bfctx L K -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F).

============================ forall X L K, bfctx L K -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) bfctx_member1 <induction on 1.

IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) ============================ forall X L K, bfctx L K @ -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) bfctx_member1 <intros.

Variables: X L K IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) H1 : bfctx L K @ H2 : member X L ============================ exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F bfctx_member1 <case H1.

Subgoal 1: Variables: X IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) H2 : member X nil ============================ exists E F, X = bfree E /\ name E /\ member (path E F) nil /\ pname F Subgoal 2 is: exists E F, X n1 n2 = bfree E /\ name E /\ member (path E F) (path n1 n2 :: K1) /\ pname F bfctx_member1 <case H2.

Subgoal 2: Variables: X K1 L1 IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) H2 : member (X n1 n2) (bfree n1 :: L1) H3 : bfctx L1 K1 * ============================ exists E F, X n1 n2 = bfree E /\ name E /\ member (path E F) (path n1 n2 :: K1) /\ pname F bfctx_member1 <case H2.

Subgoal 2.1: Variables: K1 L1 IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) H3 : bfctx L1 K1 * ============================ exists E F, bfree n1 = bfree E /\ name E /\ member (path E F) (path n1 n2 :: K1) /\ pname F Subgoal 2.2 is: exists E F, X n1 n2 = bfree E /\ name E /\ member (path E F) (path n1 n2 :: K1) /\ pname F bfctx_member1 <search.

Subgoal 2.2: Variables: X K1 L1 IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) H3 : bfctx L1 K1 * H4 : member (X n1 n2) L1 ============================ exists E F, X n1 n2 = bfree E /\ name E /\ member (path E F) (path n1 n2 :: K1) /\ pname F bfctx_member1 <apply IH to H3 H4.

Subgoal 2.2: Variables: K1 L1 E F IH : forall X L K, bfctx L K * -> member X L -> (exists E F, X = bfree E /\ name E /\ member (path E F) K /\ pname F) H3 : bfctx L1 K1 * H4 : member (bfree (E n1)) L1 H5 : name (E n1) H6 : member (path (E n1) (F n2)) K1 H7 : pname (F n2) ============================ exists E1 F, bfree (E n1) = bfree E1 /\ name E1 /\ member (path E1 F) (path n1 n2 :: K1) /\ pname F bfctx_member1 <search.Proof completed.

Abella <Theorem bfctx_member2 : forall X L K, bfctx L K -> member X K -> (exists E F, X = path E F /\ name E /\ pname F).

============================ forall X L K, bfctx L K -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) bfctx_member2 <induction on 1.

IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) ============================ forall X L K, bfctx L K @ -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) bfctx_member2 <intros.

Variables: X L K IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) H1 : bfctx L K @ H2 : member X K ============================ exists E F, X = path E F /\ name E /\ pname F bfctx_member2 <case H1.

Subgoal 1: Variables: X IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) H2 : member X nil ============================ exists E F, X = path E F /\ name E /\ pname F Subgoal 2 is: exists E F, X n1 n2 = path E F /\ name E /\ pname F bfctx_member2 <case H2.

Subgoal 2: Variables: X K1 L1 IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) H2 : member (X n1 n2) (path n1 n2 :: K1) H3 : bfctx L1 K1 * ============================ exists E F, X n1 n2 = path E F /\ name E /\ pname F bfctx_member2 <case H2.

Subgoal 2.1: Variables: K1 L1 IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) H3 : bfctx L1 K1 * ============================ exists E F, path n1 n2 = path E F /\ name E /\ pname F Subgoal 2.2 is: exists E F, X n1 n2 = path E F /\ name E /\ pname F bfctx_member2 <search.

Subgoal 2.2: Variables: X K1 L1 IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) H3 : bfctx L1 K1 * H4 : member (X n1 n2) K1 ============================ exists E F, X n1 n2 = path E F /\ name E /\ pname F bfctx_member2 <apply IH to H3 H4.

Subgoal 2.2: Variables: K1 L1 E F IH : forall X L K, bfctx L K * -> member X K -> (exists E F, X = path E F /\ name E /\ pname F) H3 : bfctx L1 K1 * H4 : member (path (E n1) (F n2)) K1 H5 : name (E n1) H6 : pname (F n2) ============================ exists E1 F1, path (E n1) (F n2) = path E1 F1 /\ name E1 /\ pname F1 bfctx_member2 <search.Proof completed.

Abella <Theorem member_path_unique : forall L K X Y F, bfctx L K -> member (path X F) K -> member (path Y F) K -> X = Y.

============================ forall L K X Y F, bfctx L K -> member (path X F) K -> member (path Y F) K -> X = Y member_path_unique <induction on 2.

IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y ============================ forall L K X Y F, bfctx L K -> member (path X F) K @ -> member (path Y F) K -> X = Y member_path_unique <intros.

Variables: L K X Y F IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L K H2 : member (path X F) K @ H3 : member (path Y F) K ============================ X = Y member_path_unique <case H2.

Subgoal 1: Variables: L X Y F L1 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L (path X F :: L1) H3 : member (path Y F) (path X F :: L1) ============================ X = Y Subgoal 2 is: X = Y member_path_unique <case H3.

Subgoal 1.1: Variables: L X F L1 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L (path X F :: L1) ============================ X = X Subgoal 1.2 is: X = Y Subgoal 2 is: X = Y member_path_unique <search.

Subgoal 1.2: Variables: L X Y F L1 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L (path X F :: L1) H4 : member (path Y F) L1 ============================ X = Y Subgoal 2 is: X = Y member_path_unique <case H1.

Subgoal 1.2: Variables: Y K1 L2 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H4 : member (path (Y n1) n2) K1 H5 : bfctx L2 K1 ============================ n1 = Y n1 Subgoal 2 is: X = Y member_path_unique <apply member_prune_path to H4.

Subgoal 2: Variables: L X Y F L1 B IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L (B :: L1) H3 : member (path Y F) (B :: L1) H4 : member (path X F) L1 * ============================ X = Y member_path_unique <case H3.

Subgoal 2.1: Variables: L X Y F L1 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L (path Y F :: L1) H4 : member (path X F) L1 * ============================ X = Y Subgoal 2.2 is: X = Y member_path_unique <case H1.

Subgoal 2.1: Variables: X K1 L2 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H4 : member (path (X n1) n2) K1 * H5 : bfctx L2 K1 ============================ X n1 = n1 Subgoal 2.2 is: X = Y member_path_unique <apply member_prune_path to H4.

Subgoal 2.2: Variables: L X Y F L1 B IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H1 : bfctx L (B :: L1) H4 : member (path X F) L1 * H5 : member (path Y F) L1 ============================ X = Y member_path_unique <case H1.

Subgoal 2.2: Variables: X Y F K1 L2 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H4 : member (path (X n1) (F n2)) K1 * H5 : member (path (Y n1) (F n2)) K1 H6 : bfctx L2 K1 ============================ X n1 = Y n1 member_path_unique <apply IH to H6 H4 H5.

Subgoal 2.2: Variables: Y F K1 L2 IH : forall L K X Y F, bfctx L K -> member (path X F) K * -> member (path Y F) K -> X = Y H4 : member (path (Y n1) (F n2)) K1 * H5 : member (path (Y n1) (F n2)) K1 H6 : bfctx L2 K1 ============================ Y n1 = Y n1 member_path_unique <search.Proof completed.

Abella <Theorem path_exists : forall L K M, bfctx L K -> {L |- bfree M} -> (exists P, {K |- path M P}).

============================ forall L K M, bfctx L K -> {L |- bfree M} -> (exists P, {K |- path M P}) path_exists <induction on 2.

IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) ============================ forall L K M, bfctx L K -> {L |- bfree M}@ -> (exists P, {K |- path M P}) path_exists <intros.

Variables: L K M IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H2 : {L |- bfree M}@ ============================ exists P, {K |- path M P} path_exists <case H2.

Subgoal 1: Variables: L K M1 IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L, bfree n1 |- bfree (M1 n1)}* ============================ exists P, {K |- path (abs M1) P} Subgoal 2 is: exists P, {K |- path (app M1 N) P} Subgoal 3 is: exists P, {K |- path M P} path_exists <assert bfctx (bfree n1 :: L) (path n1 n2 :: K).

Subgoal 1: Variables: L K M1 IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L, bfree n1 |- bfree (M1 n1)}* H4 : bfctx (bfree n1 :: L) (path n1 n2 :: K) ============================ exists P, {K |- path (abs M1) P} Subgoal 2 is: exists P, {K |- path (app M1 N) P} Subgoal 3 is: exists P, {K |- path M P} path_exists <apply IH to H4 H3.

Subgoal 1: Variables: L K M1 P IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L, bfree n1 |- bfree (M1 n1)}* H4 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H5 : {K, path n1 n2 |- path (M1 n1) (P n2)} ============================ exists P, {K |- path (abs M1) P} Subgoal 2 is: exists P, {K |- path (app M1 N) P} Subgoal 3 is: exists P, {K |- path M P} path_exists <exists bnd P.

Subgoal 1: Variables: L K M1 P IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L, bfree n1 |- bfree (M1 n1)}* H4 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H5 : {K, path n1 n2 |- path (M1 n1) (P n2)} ============================ {K |- path (abs M1) (bnd P)} Subgoal 2 is: exists P, {K |- path (app M1 N) P} Subgoal 3 is: exists P, {K |- path M P} path_exists <search.

Subgoal 2: Variables: L K N M1 IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L |- bfree M1}* H4 : {L |- bfree N}* ============================ exists P, {K |- path (app M1 N) P} Subgoal 3 is: exists P, {K |- path M P} path_exists <apply IH to H1 H3.

Subgoal 2: Variables: L K N M1 P IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L |- bfree M1}* H4 : {L |- bfree N}* H5 : {K |- path M1 P} ============================ exists P, {K |- path (app M1 N) P} Subgoal 3 is: exists P, {K |- path M P} path_exists <search.

Subgoal 3: Variables: L K M F IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L, [F] |- bfree M}* H4 : member F L ============================ exists P, {K |- path M P} path_exists <apply bfctx_member1 to H1 H4.

Subgoal 3: Variables: L K M E F1 IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H3 : {L, [bfree E] |- bfree M}* H4 : member (bfree E) L H5 : name E H6 : member (path E F1) K H7 : pname F1 ============================ exists P, {K |- path M P} path_exists <case H3.

Subgoal 3: Variables: L K M F1 IH : forall L K M, bfctx L K -> {L |- bfree M}* -> (exists P, {K |- path M P}) H1 : bfctx L K H4 : member (bfree M) L H5 : name M H6 : member (path M F1) K H7 : pname F1 ============================ exists P, {K |- path M P} path_exists <search.Proof completed.

Abella <Theorem bfree_beta_absurd : forall L K R N, bfctx L K -> {L |- bfree (beta R N)} -> false.

============================ forall L K R N, bfctx L K -> {L |- bfree (beta R N)} -> false bfree_beta_absurd <intros.

Variables: L K R N H1 : bfctx L K H2 : {L |- bfree (beta R N)} ============================ false bfree_beta_absurd <case H2.

Variables: L K R N F H1 : bfctx L K H3 : {L, [F] |- bfree (beta R N)} H4 : member F L ============================ false bfree_beta_absurd <apply bfctx_member1 to H1 H4.

Variables: L K R N E F1 H1 : bfctx L K H3 : {L, [bfree E] |- bfree (beta R N)} H4 : member (bfree E) L H5 : name E H6 : member (path E F1) K H7 : pname F1 ============================ false bfree_beta_absurd <case H5.

Variables: L K R N F1 H1 : bfctx (L n1) (K n1) H3 : {L n1, [bfree n1] |- bfree (beta (R n1) (N n1))} H4 : member (bfree n1) (L n1) H6 : member (path n1 F1) (K n1) H7 : pname F1 ============================ false bfree_beta_absurd <case H3.Proof completed.

Abella <Theorem path_app : forall L K M N Y, bfctx L K -> {L |- bfree (app M N)} -> {L |- bfree Y} -> (forall P, {K |- path (app M N) P} -> {K |- path Y P}) -> (exists YM YN, Y = app YM YN).

============================ forall L K M N Y, bfctx L K -> {L |- bfree (app M N)} -> {L |- bfree Y} -> (forall P, {K |- path (app M N) P} -> {K |- path Y P}) -> (exists YM YN, Y = app YM YN) path_app <intros.

Variables: L K M N Y H1 : bfctx L K H2 : {L |- bfree (app M N)} H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} ============================ exists YM YN, Y = app YM YN path_app <case H2.

Subgoal 1: Variables: L K M N Y H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L |- bfree M} H6 : {L |- bfree N} ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <apply path_exists to H1 H5.

Subgoal 1: Variables: L K M N Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <assert {K |- path (app M N) (left P)}.

Subgoal 1: Variables: L K M N Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} H8 : {K |- path (app M N) (left P)} ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <apply H4 to H8.

Subgoal 1: Variables: L K M N Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} H8 : {K |- path (app M N) (left P)} H9 : {K |- path Y (left P)} ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <case H9.

Subgoal 1.1: Variables: L K M N P M1 N1 H1 : bfctx L K H3 : {L |- bfree (app M1 N1)} H4 : forall P, {K |- path (app M N) P} -> {K |- path (app M1 N1) P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} H8 : {K |- path (app M N) (left P)} H10 : {K |- path M1 P} ============================ exists YM YN, app M1 N1 = app YM YN Subgoal 1.2 is: exists YM YN, beta R N1 = app YM YN Subgoal 1.3 is: exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <search.

Subgoal 1.2: Variables: L K M N P R N1 H1 : bfctx L K H3 : {L |- bfree (beta R N1)} H4 : forall P, {K |- path (app M N) P} -> {K |- path (beta R N1) P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} H8 : {K |- path (app M N) (left P)} H10 : {K, pi q\path N1 q => path n1 q |- path (R n1) (left P)} ============================ exists YM YN, beta R N1 = app YM YN Subgoal 1.3 is: exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <apply bfree_beta_absurd to H1 H3.

Subgoal 1.3: Variables: L K M N Y P F H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} H8 : {K |- path (app M N) (left P)} H10 : {K, [F] |- path Y (left P)} H11 : member F K ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <apply bfctx_member2 to H1 H11.

Subgoal 1.3: Variables: L K M N Y P E F1 H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L |- bfree M} H6 : {L |- bfree N} H7 : {K |- path M P} H8 : {K |- path (app M N) (left P)} H10 : {K, [path E F1] |- path Y (left P)} H11 : member (path E F1) K H12 : name E H13 : pname F1 ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <case H13.

Subgoal 1.3: Variables: L K M N Y P E H1 : bfctx (L n1) (K n1) H3 : {L n1 |- bfree Y} H4 : forall P, {K n1 |- path (app M N) P} -> {K n1 |- path Y P} H5 : {L n1 |- bfree M} H6 : {L n1 |- bfree N} H7 : {K n1 |- path M (P n1)} H8 : {K n1 |- path (app M N) (left (P n1))} H10 : {K n1, [path E n1] |- path Y (left (P n1))} H11 : member (path E n1) (K n1) H12 : name E ============================ exists YM YN, Y = app YM YN Subgoal 2 is: exists YM YN, Y = app YM YN path_app <case H10.

Subgoal 2: Variables: L K M N Y F H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L, [F] |- bfree (app M N)} H6 : member F L ============================ exists YM YN, Y = app YM YN path_app <apply bfctx_member1 to H1 H6.

Subgoal 2: Variables: L K M N Y E F1 H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H5 : {L, [bfree E] |- bfree (app M N)} H6 : member (bfree E) L H7 : name E H8 : member (path E F1) K H9 : pname F1 ============================ exists YM YN, Y = app YM YN path_app <case H5.

Subgoal 2: Variables: L K M N Y F1 H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (app M N) P} -> {K |- path Y P} H6 : member (bfree (app M N)) L H7 : name (app M N) H8 : member (path (app M N) F1) K H9 : pname F1 ============================ exists YM YN, Y = app YM YN path_app <case H7.Proof completed.

Abella <Theorem path_abs : forall L K R Y, bfctx L K -> {L |- bfree (abs R)} -> {L |- bfree Y} -> (forall P, {K |- path (abs R) P} -> {K |- path Y P}) -> (exists YR, Y = abs YR).

============================ forall L K R Y, bfctx L K -> {L |- bfree (abs R)} -> {L |- bfree Y} -> (forall P, {K |- path (abs R) P} -> {K |- path Y P}) -> (exists YR, Y = abs YR) path_abs <intros.

Variables: L K R Y H1 : bfctx L K H2 : {L |- bfree (abs R)} H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} ============================ exists YR, Y = abs YR path_abs <case H2.

Subgoal 1: Variables: L K R Y H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <assert bfctx (bfree n1 :: L) (path n1 n2 :: K).

Subgoal 1: Variables: L K R Y H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <apply path_exists to H6 H5.

Subgoal 1: Variables: L K R Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <assert {K |- path (abs R) (bnd P)}.

Subgoal 1: Variables: L K R Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <apply H4 to H8.

Subgoal 1: Variables: L K R Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} H9 : {K |- path Y (bnd P)} ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <case H9.

Subgoal 1.1: Variables: L K R P M H1 : bfctx L K H3 : {L |- bfree (abs M)} H4 : forall P, {K |- path (abs R) P} -> {K |- path (abs M) P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} H10 : {K, path n1 n2 |- path (M n1) (P n2)} ============================ exists YR, abs M = abs YR Subgoal 1.2 is: exists YR, beta R1 N = abs YR Subgoal 1.3 is: exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <search.

Subgoal 1.2: Variables: L K R P R1 N H1 : bfctx L K H3 : {L |- bfree (beta R1 N)} H4 : forall P, {K |- path (abs R) P} -> {K |- path (beta R1 N) P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} H10 : {K, pi q\path N q => path n1 q |- path (R1 n1) (bnd P)} ============================ exists YR, beta R1 N = abs YR Subgoal 1.3 is: exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <apply bfree_beta_absurd to H1 H3.

Subgoal 1.3: Variables: L K R Y P F H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} H10 : {K, [F] |- path Y (bnd P)} H11 : member F K ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <apply bfctx_member2 to H1 H11.

Subgoal 1.3: Variables: L K R Y P E F1 H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} H10 : {K, [path E F1] |- path Y (bnd P)} H11 : member (path E F1) K H12 : name E H13 : pname F1 ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <case H10.

Subgoal 1.3: Variables: L K R Y P H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, bfree n1 |- bfree (R n1)} H6 : bfctx (bfree n1 :: L) (path n1 n2 :: K) H7 : {K, path n1 n2 |- path (R n1) (P n2)} H8 : {K |- path (abs R) (bnd P)} H11 : member (path Y (bnd P)) K H12 : name Y H13 : pname (bnd P) ============================ exists YR, Y = abs YR Subgoal 2 is: exists YR, Y = abs YR path_abs <case H13.

Subgoal 2: Variables: L K R Y F H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, [F] |- bfree (abs R)} H6 : member F L ============================ exists YR, Y = abs YR path_abs <apply bfctx_member1 to H1 H6.

Subgoal 2: Variables: L K R Y E F1 H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H5 : {L, [bfree E] |- bfree (abs R)} H6 : member (bfree E) L H7 : name E H8 : member (path E F1) K H9 : pname F1 ============================ exists YR, Y = abs YR path_abs <case H5.

Subgoal 2: Variables: L K R Y F1 H1 : bfctx L K H3 : {L |- bfree Y} H4 : forall P, {K |- path (abs R) P} -> {K |- path Y P} H6 : member (bfree (abs R)) L H7 : name (abs R) H8 : member (path (abs R) F1) K H9 : pname F1 ============================ exists YR, Y = abs YR path_abs <case H7.Proof completed.

Abella <Theorem bfree_sames : forall L K M N, bfctx L K -> {L |- bfree M} -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N.

============================ forall L K M N, bfctx L K -> {L |- bfree M} -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N bfree_sames <induction on 2.

IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N ============================ forall L K M N, bfctx L K -> {L |- bfree M}@ -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N bfree_sames <intros.

Variables: L K M N IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree M}@ H3 : {L |- bfree N} H4 : forall p, {K |- path M p} -> {K |- path N p} ============================ M = N bfree_sames <case H2 (keep).

Subgoal 1: Variables: L K N M1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H3 : {L |- bfree N} H4 : forall p, {K |- path (abs M1) p} -> {K |- path N p} H5 : {L, bfree n1 |- bfree (M1 n1)}* ============================ abs M1 = N Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <apply path_abs to H1 H2 H3 H4.

Subgoal 1: Variables: L K M1 YR IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H3 : {L |- bfree (abs YR)} H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* ============================ abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <case H3.

Subgoal 1.1: Variables: L K M1 YR IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} ============================ abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <assert forall p, {K, path n1 n2 |- path (M1 n1) p} -> {K, path n1 n2 |- path (YR n1) p}.

Subgoal 1.1.1: Variables: L K M1 YR IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} ============================ forall p, {K, path n1 n2 |- path (M1 n1) p} -> {K, path n1 n2 |- path (YR n1) p} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <intros.

Subgoal 1.1.1: Variables: L K M1 YR p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : {K, path n1 n2 |- path (M1 n1) (p n2)} ============================ {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <assert {K |- path (abs M1) (bnd p)}.

Subgoal 1.1.1: Variables: L K M1 YR p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : {K, path n1 n2 |- path (M1 n1) (p n2)} H8 : {K |- path (abs M1) (bnd p)} ============================ {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <apply H4 to H8.

Subgoal 1.1.1: Variables: L K M1 YR p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : {K, path n1 n2 |- path (M1 n1) (p n2)} H8 : {K |- path (abs M1) (bnd p)} H9 : {K |- path (abs YR) (bnd p)} ============================ {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <case H9.

Subgoal 1.1.1.1: Variables: L K M1 YR p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : {K, path n1 n2 |- path (M1 n1) (p n2)} H8 : {K |- path (abs M1) (bnd p)} H10 : {K, path n1 n2 |- path (YR n1) (p n2)} ============================ {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1.1.2 is: {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <search.

Subgoal 1.1.1.2: Variables: L K M1 YR p F IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : {K, path n1 n2 |- path (M1 n1) (p n2)} H8 : {K |- path (abs M1) (bnd p)} H10 : {K, [F] |- path (abs YR) (bnd p)} H11 : member F K ============================ {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <apply bfctx_member2 to H1 H11.

Subgoal 1.1.1.2: Variables: L K M1 YR p E F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : {K, path n1 n2 |- path (M1 n1) (p n2)} H8 : {K |- path (abs M1) (bnd p)} H10 : {K, [path E F1] |- path (abs YR) (bnd p)} H11 : member (path E F1) K H12 : name E H13 : pname F1 ============================ {K, path n1 n2 |- path (YR n1) (p n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <case H13.

Subgoal 1.1.1.2: Variables: L K M1 YR p E IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n3) (K n3) H2 : {L n3 |- bfree (abs M1)}@ H4 : forall p, {K n3 |- path (abs M1) p} -> {K n3 |- path (abs YR) p} H5 : {L n3, bfree n1 |- bfree (M1 n1)}* H6 : {L n3, bfree n1 |- bfree (YR n1)} H7 : {K n3, path n1 n2 |- path (M1 n1) (p n3 n2)} H8 : {K n3 |- path (abs M1) (bnd (p n3))} H10 : {K n3, [path E n3] |- path (abs YR) (bnd (p n3))} H11 : member (path E n3) (K n3) H12 : name E ============================ {K n3, path n1 n2 |- path (YR n1) (p n3 n2)} Subgoal 1.1 is: abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <case H10.

Subgoal 1.1: Variables: L K M1 YR IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : forall p, {K, path n1 n2 |- path (M1 n1) p} -> {K, path n1 n2 |- path (YR n1) p} ============================ abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <assert bfctx (bfree n1 :: L) (path n1 n2 :: K).

Subgoal 1.1: Variables: L K M1 YR IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : forall p, {K, path n1 n2 |- path (M1 n1) p} -> {K, path n1 n2 |- path (YR n1) p} H8 : bfctx (bfree n1 :: L) (path n1 n2 :: K) ============================ abs M1 = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <apply IH to H8 H5 H6 H7.

Subgoal 1.1: Variables: L K YR IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs (z1\YR z1))}@ H4 : forall p, {K |- path (abs (z1\YR z1)) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (YR n1)}* H6 : {L, bfree n1 |- bfree (YR n1)} H7 : forall p, {K, path n1 n2 |- path (YR n1) p} -> {K, path n1 n2 |- path (YR n1) p} H8 : bfctx (bfree n1 :: L) (path n1 n2 :: K) ============================ abs (z1\YR z1) = abs YR Subgoal 1.2 is: abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <search.

Subgoal 1.2: Variables: L K M1 YR F IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, [F] |- bfree (abs YR)} H7 : member F L ============================ abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <apply bfctx_member1 to H1 H7.

Subgoal 1.2: Variables: L K M1 YR E F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (abs M1)}@ H4 : forall p, {K |- path (abs M1) p} -> {K |- path (abs YR) p} H5 : {L, bfree n1 |- bfree (M1 n1)}* H6 : {L, [bfree E] |- bfree (abs YR)} H7 : member (bfree E) L H8 : name E H9 : member (path E F1) K H10 : pname F1 ============================ abs M1 = abs YR Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <case H8.

Subgoal 1.2: Variables: L K M1 YR F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n2) (K n2) H2 : {L n2 |- bfree (abs (M1 n2))}@ H4 : forall p, {K n2 |- path (abs (M1 n2)) p} -> {K n2 |- path (abs (YR n2)) p} H5 : {L n2, bfree n1 |- bfree (M1 n2 n1)}* H6 : {L n2, [bfree n2] |- bfree (abs (YR n2))} H7 : member (bfree n2) (L n2) H9 : member (path n2 F1) (K n2) H10 : pname F1 ============================ abs (M1 n2) = abs (YR n2) Subgoal 2 is: app M1 N1 = N Subgoal 3 is: M = N bfree_sames <case H6.

Subgoal 2: Variables: L K N N1 M1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H3 : {L |- bfree N} H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path N p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* ============================ app M1 N1 = N Subgoal 3 is: M = N bfree_sames <apply path_app to H1 H2 H3 H4.

Subgoal 2: Variables: L K N1 M1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H3 : {L |- bfree (app YM YN)} H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* ============================ app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H3.

Subgoal 2.1: Variables: L K N1 M1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} ============================ app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <assert forall p, {K |- path M1 p} -> {K |- path YM p}.

Subgoal 2.1.1: Variables: L K N1 M1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} ============================ forall p, {K |- path M1 p} -> {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <intros.

Subgoal 2.1.1: Variables: L K N1 M1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : {K |- path M1 p} ============================ {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <assert {K |- path (app M1 N1) (left p)}.

Subgoal 2.1.1: Variables: L K N1 M1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : {K |- path M1 p} H10 : {K |- path (app M1 N1) (left p)} ============================ {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply H4 to H10.

Subgoal 2.1.1: Variables: L K N1 M1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : {K |- path M1 p} H10 : {K |- path (app M1 N1) (left p)} H11 : {K |- path (app YM YN) (left p)} ============================ {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H11.

Subgoal 2.1.1.1: Variables: L K N1 M1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : {K |- path M1 p} H10 : {K |- path (app M1 N1) (left p)} H12 : {K |- path YM p} ============================ {K |- path YM p} Subgoal 2.1.1.2 is: {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <search.

Subgoal 2.1.1.2: Variables: L K N1 M1 YM YN p F IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : {K |- path M1 p} H10 : {K |- path (app M1 N1) (left p)} H12 : {K, [F] |- path (app YM YN) (left p)} H13 : member F K ============================ {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply bfctx_member2 to H1 H13.

Subgoal 2.1.1.2: Variables: L K N1 M1 YM YN p E F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : {K |- path M1 p} H10 : {K |- path (app M1 N1) (left p)} H12 : {K, [path E F1] |- path (app YM YN) (left p)} H13 : member (path E F1) K H14 : name E H15 : pname F1 ============================ {K |- path YM p} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H15.

Subgoal 2.1.1.2: Variables: L K N1 M1 YM YN p E IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree (app M1 N1)}@ H4 : forall p, {K n1 |- path (app M1 N1) p} -> {K n1 |- path (app YM YN) p} H5 : {L n1 |- bfree M1}* H6 : {L n1 |- bfree N1}* H7 : {L n1 |- bfree YM} H8 : {L n1 |- bfree YN} H9 : {K n1 |- path M1 (p n1)} H10 : {K n1 |- path (app M1 N1) (left (p n1))} H12 : {K n1, [path E n1] |- path (app YM YN) (left (p n1))} H13 : member (path E n1) (K n1) H14 : name E ============================ {K n1 |- path YM (p n1)} Subgoal 2.1 is: app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H12.

Subgoal 2.1: Variables: L K N1 M1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path M1 p} -> {K |- path YM p} ============================ app M1 N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply IH to H1 H5 H7 H9.

Subgoal 2.1: Variables: L K N1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} ============================ app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <assert forall p, {K |- path N1 p} -> {K |- path YN p}.

Subgoal 2.1.2: Variables: L K N1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} ============================ forall p, {K |- path N1 p} -> {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <intros.

Subgoal 2.1.2: Variables: L K N1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : {K |- path N1 p} ============================ {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <assert {K |- path (app M1 N1) (right p)}.

Subgoal 2.1.2: Variables: L K N1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : {K |- path N1 p} H11 : {K |- path (app YM N1) (right p)} ============================ {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply H4 to H11.

Subgoal 2.1.2: Variables: L K N1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : {K |- path N1 p} H11 : {K |- path (app YM N1) (right p)} H12 : {K |- path (app YM YN) (right p)} ============================ {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H12.

Subgoal 2.1.2.1: Variables: L K N1 YM YN p IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : {K |- path N1 p} H11 : {K |- path (app YM N1) (right p)} H13 : {K |- path YN p} ============================ {K |- path YN p} Subgoal 2.1.2.2 is: {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <search.

Subgoal 2.1.2.2: Variables: L K N1 YM YN p F IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : {K |- path N1 p} H11 : {K |- path (app YM N1) (right p)} H13 : {K, [F] |- path (app YM YN) (right p)} H14 : member F K ============================ {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply bfctx_member2 to H1 H14.

Subgoal 2.1.2.2: Variables: L K N1 YM YN p E F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : {K |- path N1 p} H11 : {K |- path (app YM N1) (right p)} H13 : {K, [path E F1] |- path (app YM YN) (right p)} H14 : member (path E F1) K H15 : name E H16 : pname F1 ============================ {K |- path YN p} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H16.

Subgoal 2.1.2.2: Variables: L K N1 YM YN p E IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree (app YM N1)}@ H4 : forall p, {K n1 |- path (app YM N1) p} -> {K n1 |- path (app YM YN) p} H5 : {L n1 |- bfree YM}* H6 : {L n1 |- bfree N1}* H7 : {L n1 |- bfree YM} H8 : {L n1 |- bfree YN} H9 : forall p, {K n1 |- path YM p} -> {K n1 |- path YM p} H10 : {K n1 |- path N1 (p n1)} H11 : {K n1 |- path (app YM N1) (right (p n1))} H13 : {K n1, [path E n1] |- path (app YM YN) (right (p n1))} H14 : member (path E n1) (K n1) H15 : name E ============================ {K n1 |- path YN (p n1)} Subgoal 2.1 is: app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H13.

Subgoal 2.1: Variables: L K N1 YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM N1)}@ H4 : forall p, {K |- path (app YM N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree N1}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : forall p, {K |- path N1 p} -> {K |- path YN p} ============================ app YM N1 = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply IH to H1 H6 H8 H10.

Subgoal 2.1: Variables: L K YM YN IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app YM YN)}@ H4 : forall p, {K |- path (app YM YN) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree YM}* H6 : {L |- bfree YN}* H7 : {L |- bfree YM} H8 : {L |- bfree YN} H9 : forall p, {K |- path YM p} -> {K |- path YM p} H10 : forall p, {K |- path YN p} -> {K |- path YN p} ============================ app YM YN = app YM YN Subgoal 2.2 is: app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <search.

Subgoal 2.2: Variables: L K N1 M1 YM YN F IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L, [F] |- bfree (app YM YN)} H8 : member F L ============================ app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <apply bfctx_member1 to H1 H8.

Subgoal 2.2: Variables: L K N1 M1 YM YN E F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree (app M1 N1)}@ H4 : forall p, {K |- path (app M1 N1) p} -> {K |- path (app YM YN) p} H5 : {L |- bfree M1}* H6 : {L |- bfree N1}* H7 : {L, [bfree E] |- bfree (app YM YN)} H8 : member (bfree E) L H9 : name E H10 : member (path E F1) K H11 : pname F1 ============================ app M1 N1 = app YM YN Subgoal 3 is: M = N bfree_sames <case H9.

Subgoal 2.2: Variables: L K N1 M1 YM YN F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree (app (M1 n1) (N1 n1))}@ H4 : forall p, {K n1 |- path (app (M1 n1) (N1 n1)) p} -> {K n1 |- path (app (YM n1) (YN n1)) p} H5 : {L n1 |- bfree (M1 n1)}* H6 : {L n1 |- bfree (N1 n1)}* H7 : {L n1, [bfree n1] |- bfree (app (YM n1) (YN n1))} H8 : member (bfree n1) (L n1) H10 : member (path n1 F1) (K n1) H11 : pname F1 ============================ app (M1 n1) (N1 n1) = app (YM n1) (YN n1) Subgoal 3 is: M = N bfree_sames <case H7.

Subgoal 3: Variables: L K M N F IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree M}@ H3 : {L |- bfree N} H4 : forall p, {K |- path M p} -> {K |- path N p} H5 : {L, [F] |- bfree M}* H6 : member F L ============================ M = N bfree_sames <apply bfctx_member1 to H1 H6.

Subgoal 3: Variables: L K M N E F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree M}@ H3 : {L |- bfree N} H4 : forall p, {K |- path M p} -> {K |- path N p} H5 : {L, [bfree E] |- bfree M}* H6 : member (bfree E) L H7 : name E H8 : member (path E F1) K H9 : pname F1 ============================ M = N bfree_sames <case H5.

Subgoal 3: Variables: L K M N F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree M}@ H3 : {L |- bfree N} H4 : forall p, {K |- path M p} -> {K |- path N p} H6 : member (bfree M) L H7 : name M H8 : member (path M F1) K H9 : pname F1 ============================ M = N bfree_sames <assert {K |- path M F1}.

Subgoal 3: Variables: L K M N F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree M}@ H3 : {L |- bfree N} H4 : forall p, {K |- path M p} -> {K |- path N p} H6 : member (bfree M) L H7 : name M H8 : member (path M F1) K H9 : pname F1 H10 : {K |- path M F1} ============================ M = N bfree_sames <apply H4 to H10.

Subgoal 3: Variables: L K M N F1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx L K H2 : {L |- bfree M}@ H3 : {L |- bfree N} H4 : forall p, {K |- path M p} -> {K |- path N p} H6 : member (bfree M) L H7 : name M H8 : member (path M F1) K H9 : pname F1 H10 : {K |- path M F1} H11 : {K |- path N F1} ============================ M = N bfree_sames <case H9.

Subgoal 3: Variables: L K M N IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree M}@ H3 : {L n1 |- bfree N} H4 : forall p, {K n1 |- path M p} -> {K n1 |- path N p} H6 : member (bfree M) (L n1) H7 : name M H8 : member (path M n1) (K n1) H10 : {K n1 |- path M n1} H11 : {K n1 |- path N n1} ============================ M = N bfree_sames <case H11.

Subgoal 3.1: Variables: L K M R N1 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree M}@ H3 : {L n1 |- bfree (beta R N1)} H4 : forall p, {K n1 |- path M p} -> {K n1 |- path (beta R N1) p} H6 : member (bfree M) (L n1) H7 : name M H8 : member (path M n1) (K n1) H10 : {K n1 |- path M n1} H12 : {K n1, pi q\path N1 q => path n2 q |- path (R n2) n1} ============================ M = beta R N1 Subgoal 3.2 is: M = N bfree_sames <apply bfree_beta_absurd to H1 H3.

Subgoal 3.2: Variables: L K M N F2 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree M}@ H3 : {L n1 |- bfree N} H4 : forall p, {K n1 |- path M p} -> {K n1 |- path N p} H6 : member (bfree M) (L n1) H7 : name M H8 : member (path M n1) (K n1) H10 : {K n1 |- path M n1} H12 : {K n1, [F2 n1] |- path N n1} H13 : member (F2 n1) (K n1) ============================ M = N bfree_sames <apply bfctx_member2 to H1 H13.

Subgoal 3.2: Variables: L K M N E1 F3 IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree M}@ H3 : {L n1 |- bfree N} H4 : forall p, {K n1 |- path M p} -> {K n1 |- path N p} H6 : member (bfree M) (L n1) H7 : name M H8 : member (path M n1) (K n1) H10 : {K n1 |- path M n1} H12 : {K n1, [path E1 (F3 n1)] |- path N n1} H13 : member (path E1 (F3 n1)) (K n1) H14 : name E1 H15 : pname (F3 n1) ============================ M = N bfree_sames <case H12.

Subgoal 3.2: Variables: L K M N IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree M}@ H3 : {L n1 |- bfree N} H4 : forall p, {K n1 |- path M p} -> {K n1 |- path N p} H6 : member (bfree M) (L n1) H7 : name M H8 : member (path M n1) (K n1) H10 : {K n1 |- path M n1} H13 : member (path N n1) (K n1) H14 : name N H15 : pname n1 ============================ M = N bfree_sames <apply member_path_unique to H1 H8 H13.

Subgoal 3.2: Variables: L K N IH : forall L K M N, bfctx L K -> {L |- bfree M}* -> {L |- bfree N} -> (forall p, {K |- path M p} -> {K |- path N p}) -> M = N H1 : bfctx (L n1) (K n1) H2 : {L n1 |- bfree N}@ H3 : {L n1 |- bfree N} H4 : forall p, {K n1 |- path N p} -> {K n1 |- path N p} H6 : member (bfree N) (L n1) H7 : name N H8 : member (path N n1) (K n1) H10 : {K n1 |- path N n1} H13 : member (path N n1) (K n1) H14 : name N H15 : pname n1 ============================ N = N bfree_sames <search.Proof completed.

Abella <Define brctx : olist -> olist -> prop by brctx nil nil; nabla x, brctx (bred x x :: L) (bfree x :: K) := brctx L K; nabla x, brctx ((pi u\bred N u => bred x u) :: L) K := brctx L K.

Abella <Theorem brctx_mem_1 : forall L K E, brctx L K -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N).

============================ forall L K E, brctx L K -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <induction on 1.

IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) ============================ forall L K E, brctx L K @ -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <intros.

Variables: L K E IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx L K @ H2 : member E L ============================ (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <case H1 (keep).

Subgoal 1: Variables: E IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx nil nil @ H2 : member E nil ============================ (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) Subgoal 2 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <case H2.

Subgoal 2: Variables: E K1 L1 IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx (bred n1 n1 :: L1) (bfree n1 :: K1) @ H2 : member (E n1) (bred n1 n1 :: L1) H3 : brctx L1 K1 * ============================ (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <case H2.

Subgoal 2.1: Variables: K1 L1 IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx (bred n1 n1 :: L1) (bfree n1 :: K1) @ H3 : brctx L1 K1 * ============================ (exists x, bred n1 n1 = bred x x /\ name x) \/ (exists x N, bred n1 n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 2.2 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <search.

Subgoal 2.2: Variables: E K1 L1 IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx (bred n1 n1 :: L1) (bfree n1 :: K1) @ H3 : brctx L1 K1 * H4 : member (E n1) L1 ============================ (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <apply IH to H3 H4.

Subgoal 2.2: Variables: E K1 L1 IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx (bred n1 n1 :: L1) (bfree n1 :: K1) @ H3 : brctx L1 K1 * H4 : member (E n1) L1 H5 : (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) ============================ (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <case H5.

Subgoal 2.2.1: Variables: K1 L1 x IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx (bred n1 n1 :: L1) (bfree n1 :: K1) @ H3 : brctx L1 K1 * H4 : member (bred (x n1) (x n1)) L1 H6 : name (x n1) ============================ (exists x1, bred (x n1) (x n1) = bred x1 x1 /\ name x1) \/ (exists x1 N, bred (x n1) (x n1) = pi u\bred N u => bred x1 u /\ fresh x1 N) Subgoal 2.2.2 is: (exists x1, pi u\bred (N n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N1, pi u\bred (N n1) u => bred (x n1) u = pi u\bred N1 u => bred x1 u /\ fresh x1 N1) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <search.

Subgoal 2.2.2: Variables: K1 L1 x N IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx (bred n1 n1 :: L1) (bfree n1 :: K1) @ H3 : brctx L1 K1 * H4 : member (pi u\bred (N n1) u => bred (x n1) u) L1 H6 : fresh (x n1) (N n1) ============================ (exists x1, pi u\bred (N n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N1, pi u\bred (N n1) u => bred (x n1) u = pi u\bred N1 u => bred x1 u /\ fresh x1 N1) Subgoal 3 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <search.

Subgoal 3: Variables: E K1 L1 N IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx ((pi u\bred N u => bred n1 u) :: L1) K1 @ H2 : member (E n1) ((pi u\bred N u => bred n1 u) :: L1) H3 : brctx L1 K1 * ============================ (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <case H2.

Subgoal 3.1: Variables: K1 L1 N IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx ((pi u\bred N u => bred n1 u) :: L1) K1 @ H3 : brctx L1 K1 * ============================ (exists x, pi u\bred N u => bred n1 u = bred x x /\ name x) \/ (exists x N1, pi u\bred N u => bred n1 u = pi u\bred N1 u => bred x u /\ fresh x N1) Subgoal 3.2 is: (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <search.

Subgoal 3.2: Variables: E K1 L1 N IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx ((pi u\bred N u => bred n1 u) :: L1) K1 @ H3 : brctx L1 K1 * H4 : member (E n1) L1 ============================ (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <apply IH to H3 H4.

Subgoal 3.2: Variables: E K1 L1 N IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx ((pi u\bred N u => bred n1 u) :: L1) K1 @ H3 : brctx L1 K1 * H4 : member (E n1) L1 H5 : (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) ============================ (exists x, E n1 = bred x x /\ name x) \/ (exists x N, E n1 = pi u\bred N u => bred x u /\ fresh x N) brctx_mem_1 <case H5.

Subgoal 3.2.1: Variables: K1 L1 N x IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx ((pi u\bred N u => bred n1 u) :: L1) K1 @ H3 : brctx L1 K1 * H4 : member (bred (x n1) (x n1)) L1 H6 : name (x n1) ============================ (exists x1, bred (x n1) (x n1) = bred x1 x1 /\ name x1) \/ (exists x1 N, bred (x n1) (x n1) = pi u\bred N u => bred x1 u /\ fresh x1 N) Subgoal 3.2.2 is: (exists x1, pi u\bred (N1 n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N, pi u\bred (N1 n1) u => bred (x n1) u = pi u\bred N u => bred x1 u /\ fresh x1 N) brctx_mem_1 <search.

Subgoal 3.2.2: Variables: K1 L1 N x N1 IH : forall L K E, brctx L K * -> member E L -> (exists x, E = bred x x /\ name x) \/ (exists x N, E = pi u\bred N u => bred x u /\ fresh x N) H1 : brctx ((pi u\bred N u => bred n1 u) :: L1) K1 @ H3 : brctx L1 K1 * H4 : member (pi u\bred (N1 n1) u => bred (x n1) u) L1 H6 : fresh (x n1) (N1 n1) ============================ (exists x1, pi u\bred (N1 n1) u => bred (x n1) u = bred x1 x1 /\ name x1) \/ (exists x1 N, pi u\bred (N1 n1) u => bred (x n1) u = pi u\bred N u => bred x1 u /\ fresh x1 N) brctx_mem_1 <search.Proof completed.

Abella <Theorem brctx_sync : forall L K, nabla x, brctx (L x) (K x) -> member (bred x x) (L x) -> member (bfree x) (K x).

============================ forall L K, nabla x, brctx (L x) (K x) -> member (bred x x) (L x) -> member (bfree x) (K x) brctx_sync <induction on 1.

IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) ============================ forall L K, nabla x, brctx (L x) (K x) @ -> member (bred x x) (L x) -> member (bfree x) (K x) brctx_sync <intros.

Variables: L K IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H1 : brctx (L n1) (K n1) @ H2 : member (bred n1 n1) (L n1) ============================ member (bfree n1) (K n1) brctx_sync <case H1.

Subgoal 1: IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H2 : member (bred n1 n1) nil ============================ member (bfree n1) nil Subgoal 2 is: member (bfree n1) (bfree n2 :: K1 n1) Subgoal 3 is: member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <case H2.

Subgoal 2: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H2 : member (bred n1 n1) (bred n2 n2 :: L1 n1) H3 : brctx (L1 n1) (K1 n1) * ============================ member (bfree n1) (bfree n2 :: K1 n1) Subgoal 3 is: member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <case H2.

Subgoal 2: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx (L1 n1) (K1 n1) * H4 : member (bred n1 n1) (L1 n1) ============================ member (bfree n1) (bfree n2 :: K1 n1) Subgoal 3 is: member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <apply IH to H3 H4.

Subgoal 2: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx (L1 n1) (K1 n1) * H4 : member (bred n1 n1) (L1 n1) H5 : member (bfree n1) (K1 n1) ============================ member (bfree n1) (bfree n2 :: K1 n1) Subgoal 3 is: member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <search.

Subgoal 3: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H2 : member (bred n1 n1) (bred n1 n1 :: L1) H3 : brctx L1 K1 * ============================ member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <case H2.

Subgoal 3.1: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx L1 K1 * ============================ member (bfree n1) (bfree n1 :: K1) Subgoal 3.2 is: member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <search.

Subgoal 3.2: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx L1 K1 * H4 : member (bred n1 n1) L1 ============================ member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <apply IH to H3 H4.

Subgoal 3.2: Variables: K1 L1 IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx L1 K1 * H4 : member (bred n1 n1) L1 H5 : member (bfree n1) K1 ============================ member (bfree n1) (bfree n1 :: K1) Subgoal 4 is: member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <search.

Subgoal 4: Variables: K2 L1 N IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H2 : member (bred n1 n1) ((pi u\bred (N n1) u => bred n2 u) :: L1 n1) H3 : brctx (L1 n1) (K2 n1) * ============================ member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <case H2.

Subgoal 4: Variables: K2 L1 N IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx (L1 n1) (K2 n1) * H4 : member (bred n1 n1) (L1 n1) ============================ member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <apply IH to H3 H4.

Subgoal 4: Variables: K2 L1 N IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx (L1 n1) (K2 n1) * H4 : member (bred n1 n1) (L1 n1) H5 : member (bfree n1) (K2 n1) ============================ member (bfree n1) (K2 n1) Subgoal 5 is: member (bfree n1) K1 brctx_sync <search.

Subgoal 5: Variables: K1 L1 N IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H2 : member (bred n1 n1) ((pi u\bred N u => bred n1 u) :: L1) H3 : brctx L1 K1 * ============================ member (bfree n1) K1 brctx_sync <case H2.

Subgoal 5: Variables: K1 L1 N IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx L1 K1 * H4 : member (bred n1 n1) L1 ============================ member (bfree n1) K1 brctx_sync <apply IH to H3 H4.

Subgoal 5: Variables: K1 L1 N IH : forall L K, nabla x, brctx (L x) (K x) * -> member (bred x x) (L x) -> member (bfree x) (K x) H3 : brctx L1 K1 * H4 : member (bred n1 n1) L1 H5 : member (bfree n1) K1 ============================ member (bfree n1) K1 brctx_sync <search.Proof completed.

Abella <Theorem bred_makes_bfree : forall L K M U, brctx L K -> {L |- bred M U} -> {K |- bfree U}.

============================ forall L K M U, brctx L K -> {L |- bred M U} -> {K |- bfree U} bred_makes_bfree <induction on 2.

IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} ============================ forall L K M U, brctx L K -> {L |- bred M U}@ -> {K |- bfree U} bred_makes_bfree <intros.

Variables: L K M U IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred M U}@ ============================ {K |- bfree U} bred_makes_bfree <case H2 (keep).

Subgoal 1: Variables: L K U1 M1 IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (abs M1) (abs U1)}@ H3 : {L, bred n1 n1 |- bred (M1 n1) (U1 n1)}* ============================ {K |- bfree (abs U1)} Subgoal 2 is: {K |- bfree (app U1 V)} Subgoal 3 is: {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <apply IH to _ H3.

Subgoal 1: Variables: L K U1 M1 IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (abs M1) (abs U1)}@ H3 : {L, bred n1 n1 |- bred (M1 n1) (U1 n1)}* H4 : {K, bfree n1 |- bfree (U1 n1)} ============================ {K |- bfree (abs U1)} Subgoal 2 is: {K |- bfree (app U1 V)} Subgoal 3 is: {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <search.

Subgoal 2: Variables: L K V N U1 M1 IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (app M1 N) (app U1 V)}@ H3 : {L |- bred M1 U1}* H4 : {L |- bred N V}* ============================ {K |- bfree (app U1 V)} Subgoal 3 is: {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <apply IH to _ H3.

Subgoal 2: Variables: L K V N U1 M1 IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (app M1 N) (app U1 V)}@ H3 : {L |- bred M1 U1}* H4 : {L |- bred N V}* H5 : {K |- bfree U1} ============================ {K |- bfree (app U1 V)} Subgoal 3 is: {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <apply IH to _ H4.

Subgoal 2: Variables: L K V N U1 M1 IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (app M1 N) (app U1 V)}@ H3 : {L |- bred M1 U1}* H4 : {L |- bred N V}* H5 : {K |- bfree U1} H6 : {K |- bfree V} ============================ {K |- bfree (app U1 V)} Subgoal 3 is: {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <search.

Subgoal 3: Variables: L K U R N IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (beta R N) U}@ H3 : {L, pi u\bred N u => bred n1 u |- bred (R n1) U}* ============================ {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <apply IH to _ H3.

Subgoal 3: Variables: L K U R N IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred (beta R N) U}@ H3 : {L, pi u\bred N u => bred n1 u |- bred (R n1) U}* H4 : {K |- bfree U} ============================ {K |- bfree U} Subgoal 4 is: {K |- bfree U} bred_makes_bfree <search.

Subgoal 4: Variables: L K M U F IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred M U}@ H3 : {L, [F] |- bred M U}* H4 : member F L ============================ {K |- bfree U} bred_makes_bfree <apply brctx_mem_1 to H1 H4.

Subgoal 4: Variables: L K M U F IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred M U}@ H3 : {L, [F] |- bred M U}* H4 : member F L H5 : (exists x, F = bred x x /\ name x) \/ (exists x N, F = pi u\bred N u => bred x u /\ fresh x N) ============================ {K |- bfree U} bred_makes_bfree <case H5.

Subgoal 4.1: Variables: L K M U x IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred M U}@ H3 : {L, [bred x x] |- bred M U}* H4 : member (bred x x) L H6 : name x ============================ {K |- bfree U} Subgoal 4.2 is: {K |- bfree U} bred_makes_bfree <case H3.

Subgoal 4.1: Variables: L K U IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred U U}@ H4 : member (bred U U) L H6 : name U ============================ {K |- bfree U} Subgoal 4.2 is: {K |- bfree U} bred_makes_bfree <case H6.

Subgoal 4.1: Variables: L K IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx (L n1) (K n1) H2 : {L n1 |- bred n1 n1}@ H4 : member (bred n1 n1) (L n1) ============================ {K n1 |- bfree n1} Subgoal 4.2 is: {K |- bfree U} bred_makes_bfree <apply brctx_sync to H1 H4.

Subgoal 4.1: Variables: L K IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx (L n1) (K n1) H2 : {L n1 |- bred n1 n1}@ H4 : member (bred n1 n1) (L n1) H7 : member (bfree n1) (K n1) ============================ {K n1 |- bfree n1} Subgoal 4.2 is: {K |- bfree U} bred_makes_bfree <search.

Subgoal 4.2: Variables: L K M U x N IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred M U}@ H3 : {L, [pi u\bred N u => bred x u] |- bred M U}* H4 : member (pi u\bred N u => bred x u) L H6 : fresh x N ============================ {K |- bfree U} bred_makes_bfree <case H3.

Subgoal 4.2: Variables: L K M U N IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx L K H2 : {L |- bred M U}@ H4 : member (pi u\bred N u => bred M u) L H6 : fresh M N H7 : {L |- bred N U}* ============================ {K |- bfree U} bred_makes_bfree <case H6.

Subgoal 4.2: Variables: L K U X IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx (L n1) (K n1) H2 : {L n1 |- bred n1 (U n1)}@ H4 : member (pi u\bred X u => bred n1 u) (L n1) H7 : {L n1 |- bred X (U n1)}* ============================ {K n1 |- bfree (U n1)} bred_makes_bfree <apply IH to H1 H7.

Subgoal 4.2: Variables: L K U X IH : forall L K M U, brctx L K -> {L |- bred M U}* -> {K |- bfree U} H1 : brctx (L n1) (K n1) H2 : {L n1 |- bred n1 (U n1)}@ H4 : member (pi u\bred X u => bred n1 u) (L n1) H7 : {L n1 |- bred X (U n1)}* H8 : {K n1 |- bfree (U n1)} ============================ {K n1 |- bfree (U n1)} bred_makes_bfree <search.Proof completed.

Abella <Theorem same_paths_bred_same : forall M N U V, (forall P, {path M P} -> {path N P}) -> {bred M U} -> {bred N V} -> U = V.

============================ forall M N U V, (forall P, {path M P} -> {path N P}) -> {bred M U} -> {bred N V} -> U = V same_paths_bred_same <intros.

Variables: M N U V H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} ============================ U = V same_paths_bred_same <apply bred_makes_bfree to _ H2.

Variables: M N U V H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} ============================ U = V same_paths_bred_same <apply bred_makes_bfree to _ H3.

Variables: M N U V H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} H5 : {bfree V} ============================ U = V same_paths_bred_same <backchain bfree_sames.

Variables: M N U V H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} H5 : {bfree V} ============================ forall p, {path U p} -> {path V p} same_paths_bred_same <intros.

Variables: M N U V p H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} H5 : {bfree V} H6 : {path U p} ============================ {path V p} same_paths_bred_same <apply bred_rtl to _ H2 H6.

Variables: M N U V p H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} H5 : {bfree V} H6 : {path U p} H7 : {path M p} ============================ {path V p} same_paths_bred_same <apply H1 to H7.

Variables: M N U V p H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} H5 : {bfree V} H6 : {path U p} H7 : {path M p} H8 : {path N p} ============================ {path V p} same_paths_bred_same <apply bred_ltr to _ H3 H8.

Variables: M N U V p H1 : forall P, {path M P} -> {path N P} H2 : {bred M U} H3 : {bred N V} H4 : {bfree U} H5 : {bfree V} H6 : {path U p} H7 : {path M p} H8 : {path N p} H9 : {path V p} ============================ {path V p} same_paths_bred_same <search.Proof completed.

Abella <