]> (define tree-invert (lambda (t) (if (null? t) '() (list (car t) _ (tree-invert (cadr t)))))) (evalo '(tree-invert '(1 (2 () ()) (3 () ()))) '() '(1 (3 () ()) (2 () ()))) evalo (cadr t) env val_left (list (car t) (tree-invert (cadr t)) (tree-invert (cadr t))) (set-logic QF_LIA) (declare-fun left_subtree_val () Int) (declare-fun right_subtree_val () Int) ; Refinement invariant: inversion must SWAP subtrees, not duplicate ; left_val must equal right_input (3), not left_input (2) (assert (= left_subtree_val 2)) (assert (= right_subtree_val 3)) (assert (= left_subtree_val right_subtree_val)) ; ^ VIOLATION: duplicated left branch, swap invariant breached (check-sat) unsat Subtree symmetry invariant breached: duplicated left branch instead of swapping right branch. Hole _ was bound to (tree-invert (cadr t)) but must be bound to (tree-invert (caddr t)) to satisfy the swap constraint. evalo (caddr t) env val_right (define tree-invert (lambda (t) (if (null? t) '() (list (car t) (tree-invert (caddr t)) (tree-invert (cadr t)))))) (set-logic QF_LIA) (declare-fun left_in () Int) (declare-fun right_in () Int) (declare-fun left_out () Int) (declare-fun right_out () Int) ; Input tree: (1 (2 () ()) (3 () ())) (assert (= left_in 2)) (assert (= right_in 3)) ; Inversion swap invariant: left_out == right_in, right_out == left_in (assert (= left_out right_in)) (assert (= right_out left_in)) (check-sat) (get-model) sat (model (define-fun left_in () Int 2) (define-fun right_in () Int 3) (define-fun left_out () Int 3) (define-fun right_out () Int 2) ) -- Lean 4 proof: tree_invert_correct -- depth preserved AND structure is mirror image theorem tree_invert_correct (t : Tree) : Tree.depth (tree_invert t) = Tree.depth t && Tree.mirror (tree_invert t) = t := by induction t with | leaf => rfl | node val l r ihl ihr => simp [tree_invert] exact <| by omega, by rw [ihl, ihr] |>

2 SAT PROVEN

(define tree-invert (lambda (t) (if (null? t) '() (list (car t) (tree-invert (caddr t)) (tree-invert (cadr t))))))