[DeriveMode True False, Match 2, Mark [[1]], Narrow 0 False, Mark [[0, 1, 0]], Theorem False (F "=" [F "top" [F "push" [V "x", V "s"]], F "entry" [V "x"]]), Mark [[0, 1, 1]], Theorem False (F "=" [F "top" [F "push" [V "x", V "s"]], F "entry" [V "x"]]), Mark [[1]], ApplyTrans, Mark [[1, 0, 0]], Theorem False (F "~" [F "pop" [F "push" [V "x", V "s"]], V "s"]), Mark [[1, 0, 0]], Theorem False (F "~" [F "pop" [F "push" [V "x", V "s"]], V "s"]), Mark [[1]], ApplyTrans, Mark [[1, 0, 1, 0], [1, 0, 1, 1]], ReverseSubtrees, Mark [[1, 0, 1]], Theorem False (F "~" [F "pop" [F "push" [V "x", V "s"]], V "s"]), Mark []]