equal
deleted
inserted
replaced
86 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
86 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
87 proof (induct t) |
87 proof (induct t) |
88 case Lf thus ?case by (metis reflect.simps(1)) |
88 case Lf thus ?case by (metis reflect.simps(1)) |
89 next |
89 next |
90 case (Br a t1 t2) thus ?case |
90 case (Br a t1 t2) thus ?case |
91 by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) |
91 by (metis add_commute n_nodes.simps(2) reflect.simps(2)) |
92 qed |
92 qed |
93 |
93 |
94 declare [[ atp_problem_prefix = "BT__depth_reflect" ]] |
94 declare [[ atp_problem_prefix = "BT__depth_reflect" ]] |
95 |
95 |
96 lemma depth_reflect: "depth (reflect t) = depth t" |
96 lemma depth_reflect: "depth (reflect t) = depth t" |