import Init

namespace Hunch.PatchReplay
def replay : ((State Op : Type) → (Op → State → Option State) → List Op → State → Option State) :=
  fun _ _ step ops s => ops.foldl (fun prior op => prior.bind (step op)) (some s)

theorem concat : (∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (replay State Op step xs s)) :=
  by
    intro State Op step xs ys s
    exact List.foldl_append

end Hunch.PatchReplay

def OA_statement : Prop := (∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), Hunch.PatchReplay.replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (Hunch.PatchReplay.replay State Op step xs s))

theorem OA_target : OA_statement :=
  by
    exact Hunch.PatchReplay.concat

#print axioms OA_target
#check OA_target