fact: Fixpoint netlist_find_sublist {j k} (xs : netlist B j k) {i l} (ys : netlist B i l) : option ((netlist B i j + { i = j}) * (netlist B k l + { k = l})) := match xs, ys with | @tfin _ _ j k x, @tfin _ _ i l y => match eq_dec i j, eq_dec k l with | left H1, left H2 => match eq_dec x (rew <- [fun y => B _ y] H2 in rew [fun x => B x _] H1 in y) with | left _ => Some (inright H1, inright H2) | _ => None end | _, _ => None end | @tfin _ _ j k x, @tadd _ _ i o _ y ys => match eq_dec i j, eq_dec k o with | left H1, left H2 => match eq_dec x (rew <- [fun y => B _ y] H2 in rew [fun x => B x _] H1 in y) with | left _ => Some (inright H1, inleft (rew <- [fun x => netlist B x _] H2 in ys)) | _ => None end | _, _ => match netlist_find_sublist (tfin x) ys with | None => None | Some (inright H, zs) => Some (inleft (rew [fun y => netlist B _ y] H in tfin y), zs) | Some (inleft ys, zs) => Some (inleft (y :::: ys), zs) end end | _, tfin _ => None | @tadd _ _ j m k x xs, @tadd _ _ i o l y ys => match eq_dec i j, eq_dec m o with | left H1, left H2 => match eq_dec x (rew [fun x => B x _] H1 in rew <- [fun x => B _ x] H2 in y) with | left _ => match netlist_find_sublist xs ys with | Some (inright H, cs) => Some (inright H1, cs) | _ => match netlist_find_sublist (x :::: xs) ys with | None => None | Some (inright H, zs) => Some (inleft (rew [fun y => netlist B _ y] H in tfin y), zs) | Some (inleft ys, zs) => Some (inleft (y :::: ys), zs) end end | _ => match netlist_find_sublist (x :::: xs) ys with | None => None | Some (inright H, zs) => Some (inleft (rew [fun y => netlist B _ y] H in tfin y), zs) | Some (inleft ys, zs) => Some (inleft (y :::: ys), zs) end end | _, _ => match netlist_find_sublist (x :::: xs) ys with | None => None | Some (inright H, zs) => Some (inleft (rew [fun y => netlist B _ y] H in tfin y), zs) | Some (inleft ys, zs) => Some (inleft (y :::: ys), zs) end end end.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib