{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"665056b74ac2b6e5e2959f32a560c25196fc89e85394cf2032c3a868bb4e2884","problem":{"id":16,"title":"Exact causal-parent projection for a tombstone-preserving list CRDT","description":"Can the exact structural state of an event's causal parents be reconstructed by filtering the final state of a successful list-CRDT replay and restoring the parent-context tombstone flags?\n\nThe challenge is the supporting semantic lemma below, not a runtime claim. The parent history may omit concurrent events earlier in the serialization, so it need not be a serialization prefix. Preserving visible text alone is insufficient: deleted but known items can remain insertion anchors.\n\nModel and tuple notation\n• Id = Nat × Nat, interpreted as actor and sequence number.\n• Ins = Id × Id × Nat × Option Id × Option Id: ordering identity, immutable label, payload, left origin, right origin.\n• Item = Ins × Bool, with true meaning deleted. State = List Item, including tombstones.\n• Op = Sum Ins Id: insertion or deletion of an identity.\n• Edit = Sum (Nat × Id × Nat) Nat: insert at a visible position with a supplied label/payload, or delete at a visible position.\n• Event = Id × List Id × Edit × Op: event identity, explicit causal past, user edit, recorded generated operation. History = List Event.\n\nThe statement contains the entire executable model using typed lambda applications, because the venue disallows custom definitions and local := bindings in statements. Names inside those applications are indexOf, leftAfter, rightBefore, idBefore, scan, insert, apply, visible, generate, replayOps, replay, ids, parentContext, validExtension, validHistory and reconstruct. Products associate to the right. None of these names is a theorem assumed as an axiom.\n\nInsertion scans the structural interval between the two origins, including deleted items, using actor/sequence ordering to break equal-origin ties. Delete marks the existing item and retains it. Edit generation chooses a visible left neighbor, then the immediate structural right neighbor, which may be deleted. Replay folds the recorded operations from empty state and propagates errors. Errors 0–5 denote missing origin, duplicate identity, invalid interval, missing delete target, position out of bounds and exhausted scan fuel.\n\nValid history means every event has a fresh identity, refers only to earlier event identities, has a transitively closed past, includes previous events from the same actor with lower sequence numbers, and records precisely the operation generated from successfully replaying its own parent context. These assumptions do not assert the desired projection equation. Complete full-history replay success is a separate explicit premise.\n\nFor each actual event, P is the history filtered by membership in that event's past. Reconstruct selects from the final structural state precisely those items whose insertion identities appear in P, preserving all immutable fields and their final relative order. It then restores each selected item's deleted flag using existence of a deletion of that identity in P. The requested conclusion is replay(P) = ok(reconstruct(P, finalState)). This Boolean deletion model does not model the native implementation's multiplicity counters.\n\nAttempt and remaining obstacle\nThe empty-parent case has a direct Lean proof; a partial attempt is supplied separately. In our local project, we also have a proved serialization-prefix reconstruction theorem for the reference model. Neither settles non-prefix parents. A possible route is to stably move P to the front of the serialization, prove operation commutation/convergence and preservation of successful replay, and then apply prefix reconstruction. Establishing validity of the reordered history by assuming the desired projection would be circular. That missing step remains open here.\n\nResearch motivation and limits\nWe are exploring exact causal preparation for histories consisting of a linear source and concurrent remote edits. A useful eventual algorithm would answer identity-sensitive queries without walking every source version, with preprocessing, causal-context access, maintained order, tombstones, output and storage all charged. This challenge supplies only a semantic prerequisite. It proves no efficiency gain, memory bound, native refinement or new convergence result. It is plausibly an instance of established list-CRDT convergence reasoning. We welcome a proof or a counterexample under the exact stated model.\n\nPrepared by James Addison (jungle) with Codex, with a separate adversarial AI evaluator checking the local statement and tests. AI review is not an independent human statement review on this site. The platform's own Lean checker determines its displayed status.\n\nPort validation: the self-contained statement has been locally typechecked and source-reviewed, with finite Lean kernel controls. A universal port-equivalence theorem to the separately defined local project model is not claimed. The exact expression published here is the challenge.","statement":"(fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>\n(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>\n(fun (scan : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Nat→Nat→Nat→Nat→Bool→Nat→Except Nat Nat) =>\n(fun (insert : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (apply : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (visible : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (generate : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Nat×Nat)→(Sum (Nat×(Nat×Nat)×Nat) Nat)→Except Nat (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))) =>\n(fun (replayOps : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (replay : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (ids : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→List (Nat×Nat)) =>\n(fun (validExtension : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→Prop) =>\n(fun (validHistory : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Prop) =>\n(fun (reconstruct : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (parentContext : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→(List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) =>\n∀ (history : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) (finalState : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))),\nvalidHistory history→replay history = .ok finalState→∀ (event : ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))), event ∈ history→replay (parentContext history event) =\n.ok (reconstruct ((parentContext history event).map (fun e => e.2.2.2)) finalState)\n) (fun history event =>\nhistory.filter (fun previous => event.2.1.any (fun id => id == previous.1)))\n) (fun ops finalState =>\n(fun (born dead : List (Nat×Nat)) =>\n(finalState.filter (fun item => born.any (fun id => id == item.1.1))).map\n(fun item => (item.1, dead.any (fun id => id == item.1.1))))\n(ops.filterMap (fun op => match op with | .inl ins => some ins.1 | .inr _ => none))\n(ops.filterMap (fun op => match op with | .inl _ => none | .inr target => some target)))\n) (fun history =>\nList.rec (fun _ : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))) => True)\n(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])\n) (fun pre event =>\nevent.1 ∉ ids pre ∧\n(∀ id ∈ event.2.1, id ∈ ids pre) ∧\n(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧\n(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧\n∃ sourceState,\nreplay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧\ngenerate sourceState event.1 event.2.2.1 = .ok event.2.2.2)\n) (fun history => history.map (fun event => event.1))\n) (fun history =>\nreplayOps (history.map (fun event => event.2.2.2)) [])\n) (fun ops start =>\nops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))\n) (fun state fresh edit =>\nmatch edit with\n| .inl (pos, label, payload) => do\nif (visible state).length < pos then throw 4\n(fun (left : Option (Nat×Nat)) => do\nlet start ← leftAfter state left\nreturn .inl (fresh, label, payload, left, (state[start]?).map (fun x => x.1.1))) (if pos = 0 then none else ((visible state)[pos - 1]?).map (fun x => x.1.1))\n| .inr pos => match (visible state)[pos]? with\n| none => .error 4\n| some item => .ok (.inr item.1.1))\n) (fun state => state.filter (fun item => !item.2))\n) (fun state op =>\nmatch op with\n| .inl ins => insert state ins\n| .inr target =>\nif (indexOf target state).isSome then\n.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)\nelse .error 3)\n) (fun state ins => do\nif (indexOf ins.1 state).isSome then throw 1\nlet left ← leftAfter state ins.2.2.2.1\nlet right ← rightBefore state ins.2.2.2.2\nif right < left then throw 2\nlet dest ← scan state ins left right state.length left false left\nreturn state.take dest ++ [(ins, false)] ++ state.drop dest)\n) (fun state ins left right fuel =>\nNat.rec\n(fun i scanning back =>\nif right ≤ i then .ok (if scanning then back else i) else .error 5)\n(fun _ recur i scanning back => do\nif right ≤ i then return if scanning then back else i\nlet other ← match state[i]? with\n| none => .error 4\n| some item => .ok item\nif other.1.2.2.2.1 = ins.2.2.2.1 then\nif other.1.2.2.2.2 = ins.2.2.2.2 then\nif idBefore ins.1 other.1.1 then return if scanning then back else i\nelse recur (i + 1) false back\nelse\nlet otherRight ← rightBefore state other.1.2.2.2.2\nif otherRight < right then recur (i + 1) true (if scanning then back else i)\nelse recur (i + 1) false back\nelse\nlet otherLeft ← leftAfter state other.1.2.2.2.1\nif otherLeft < left then return if scanning then back else i\nelse recur (i + 1) scanning back)\nfuel)\n) (fun a b =>\na.1 < b.1 || (a.1 == b.1 && a.2 < b.2))\n) (fun state origin =>\nmatch origin with\n| none => .ok state.length\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok i)\n) (fun state origin =>\nmatch origin with\n| none => .ok 0\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok (i + 1))\n) (fun id state =>\nList.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state)","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := ((fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>\n(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>\n(fun (scan : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Nat→Nat→Nat→Nat→Bool→Nat→Except Nat Nat) =>\n(fun (insert : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (apply : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (visible : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (generate : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Nat×Nat)→(Sum (Nat×(Nat×Nat)×Nat) Nat)→Except Nat (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))) =>\n(fun (replayOps : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (replay : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (ids : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→List (Nat×Nat)) =>\n(fun (validExtension : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→Prop) =>\n(fun (validHistory : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Prop) =>\n(fun (reconstruct : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (parentContext : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→(List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) =>\n∀ (history : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) (finalState : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))),\nvalidHistory history→replay history = .ok finalState→∀ (event : ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))), event ∈ history→replay (parentContext history event) =\n.ok (reconstruct ((parentContext history event).map (fun e => e.2.2.2)) finalState)\n) (fun history event =>\nhistory.filter (fun previous => event.2.1.any (fun id => id == previous.1)))\n) (fun ops finalState =>\n(fun (born dead : List (Nat×Nat)) =>\n(finalState.filter (fun item => born.any (fun id => id == item.1.1))).map\n(fun item => (item.1, dead.any (fun id => id == item.1.1))))\n(ops.filterMap (fun op => match op with | .inl ins => some ins.1 | .inr _ => none))\n(ops.filterMap (fun op => match op with | .inl _ => none | .inr target => some target)))\n) (fun history =>\nList.rec (fun _ : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))) => True)\n(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])\n) (fun pre event =>\nevent.1 ∉ ids pre ∧\n(∀ id ∈ event.2.1, id ∈ ids pre) ∧\n(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧\n(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧\n∃ sourceState,\nreplay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧\ngenerate sourceState event.1 event.2.2.1 = .ok event.2.2.2)\n) (fun history => history.map (fun event => event.1))\n) (fun history =>\nreplayOps (history.map (fun event => event.2.2.2)) [])\n) (fun ops start =>\nops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))\n) (fun state fresh edit =>\nmatch edit with\n| .inl (pos, label, payload) => do\nif (visible state).length < pos then throw 4\n(fun (left : Option (Nat×Nat)) => do\nlet start ← leftAfter state left\nreturn .inl (fresh, label, payload, left, (state[start]?).map (fun x => x.1.1))) (if pos = 0 then none else ((visible state)[pos - 1]?).map (fun x => x.1.1))\n| .inr pos => match (visible state)[pos]? with\n| none => .error 4\n| some item => .ok (.inr item.1.1))\n) (fun state => state.filter (fun item => !item.2))\n) (fun state op =>\nmatch op with\n| .inl ins => insert state ins\n| .inr target =>\nif (indexOf target state).isSome then\n.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)\nelse .error 3)\n) (fun state ins => do\nif (indexOf ins.1 state).isSome then throw 1\nlet left ← leftAfter state ins.2.2.2.1\nlet right ← rightBefore state ins.2.2.2.2\nif right < left then throw 2\nlet dest ← scan state ins left right state.length left false left\nreturn state.take dest ++ [(ins, false)] ++ state.drop dest)\n) (fun state ins left right fuel =>\nNat.rec\n(fun i scanning back =>\nif right ≤ i then .ok (if scanning then back else i) else .error 5)\n(fun _ recur i scanning back => do\nif right ≤ i then return if scanning then back else i\nlet other ← match state[i]? with\n| none => .error 4\n| some item => .ok item\nif other.1.2.2.2.1 = ins.2.2.2.1 then\nif other.1.2.2.2.2 = ins.2.2.2.2 then\nif idBefore ins.1 other.1.1 then return if scanning then back else i\nelse recur (i + 1) false back\nelse\nlet otherRight ← rightBefore state other.1.2.2.2.2\nif otherRight < right then recur (i + 1) true (if scanning then back else i)\nelse recur (i + 1) false back\nelse\nlet otherLeft ← leftAfter state other.1.2.2.2.1\nif otherLeft < left then return if scanning then back else i\nelse recur (i + 1) scanning back)\nfuel)\n) (fun a b =>\na.1 < b.1 || (a.1 == b.1 && a.2 < b.2))\n) (fun state origin =>\nmatch origin with\n| none => .ok state.length\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok i)\n) (fun state origin =>\nmatch origin with\n| none => .ok 0\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok (i + 1))\n) (fun id state =>\nList.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state))\n\n#check OA_statement\n","proof":null}