-- Lean 4 Formal Certificate for candidate_2
-- Generated by Relational Lisp Synthesis Engine
-- Date: 2026-07-31T16:43:01.862Z
-- AST Hash: a4b7e616bf28ed0f1317285c4103978086f7725cdc13f2924f785b10dd0c9f46

theorem append_correct : ∀ (x y z : List ℕ),
  append x y z ↔ z = x ++ y := by
  intro x y z
  constructor
  · intro h
    induction h with
    | nil => rfl
    | cons h ih =>
      simp [List.cons_append]
      exact ih
  · intro h
    rw [h]
    induction x with
    | nil => constructor
    | cons h t ih =>
      constructor
      · simp [List.cons_append]
        exact ih

-- Synthesis Trace
-- Candidate: candidate_2
-- Z3 Result: SAT
-- Validation: VALID

-- Z3 Model (if SAT)
-- Model: Z = [1,2,3]

-- Generated AST
-- {
--   "type": "if",
--   "test": [
--     "null",
--     "_x"
--   ],
--   "then": [
--     "eq",
--     "_y",
--     "_z"
--   ],
--   "else": [
--     "and",
--     [
--       "cons",
--       [
--         "car",
--         "_x"
--       ],
--       [
--         "cdr",
--         "_x"
--       ],
--       [
--         "car",
--         "_z"
--       ],
--       [
--         "cdr",
--         "_z"
--       ]
--     ],
--     [
--       "append",
--       [
--         "cdr",
--         "_x"
--       ],
--       "_y",
--       [
--         "cdr",
--         "_z"
--       ]
--     ]
--   ]
-- }

-- Verified signature below