import Init

def OA_statement : Prop := ((fun (run : List (Bool × Bool) → Nat → Option Nat → Sum Nat (Nat × Option Nat)) =>
(fun (active : List (Bool × Bool) → List (Bool × Bool)) =>
(fun (lastClear : List (Bool × Bool) → Option Nat) =>
(fun (firstStart : List (Bool × Bool) → Option Nat → Option Nat) =>
(fun (summarize : List (Bool × Bool) → Nat → Option Nat → Sum Nat (Nat × Option Nat)) =>
∀ actions position saved, run actions position saved = summarize actions position saved
) (fun actions position saved =>
(fun chunk =>
(fun clear =>
(fun start =>
(fun finalSaved =>
if chunk.length < actions.length then .inl (finalSaved.getD (position + chunk.length))
else .inr (position + chunk.length, finalSaved))
((if clear.isSome then none else saved).or (start.map (position + ·))))
(firstStart chunk clear)) (lastClear chunk)) (active actions))
) (fun chunk clear =>
(((chunk.zipIdx).drop (clear.map Nat.succ |>.getD 0)).find? (fun pair => !pair.1.1 && pair.1.2)).map Prod.snd)
) (fun chunk =>
((chunk.zipIdx.reverse).find? (fun pair => pair.1.1 && !pair.1.2)).map Prod.snd)
) (fun actions => actions.takeWhile (fun action => !action.1 || !action.2))
) (fun actions =>
List.rec (fun position saved => .inr (position, saved))
(fun action _ rest position saved =>
if action.1 then
  if action.2 then .inl (saved.getD position) else rest (position + 1) none
else
  if action.2 then rest (position + 1) (some (saved.getD position))
  else rest (position + 1) saved) actions))

theorem OA_target : OA_statement :=
  by
    dsimp only [OA_statement]
    intro actions position saved
    cases actions with
    | nil => cases saved <;> rfl
    | cons action rest =>
      rcases action with ⟨a, b⟩
      cases a <;> cases b
      · skip
      · skip
      · skip
      · cases saved <;> simp [List.takeWhile_cons]

#print axioms OA_target
#check OA_target