merge fixes/clarifications - clarify tip contents R \not\in \py

merge fixes/clarifications - sort out complex case D = C

merge fixes/clarifications - fix several P to \p

merge fixes/clarifications - remove wrong "on R"

merge fixes/clarifications - add missing \

merge fixes/clarifications - clarify Non-Topbloke merges - add a wlog

merge fixes/clarifications - clarify Non-Topbloke merges

merge fixes/clarifications - relax Foreign Merges

merge fixes/clarifications - change , to \land

split into multiple source files

remove a spurious \newpage

merge ends conditions change order of precondition to put M in middle, for clarity

wording improvement

mention that merge can be used for dependency reinsertion

Revert "rename anticommit section"

This reverts commit 8649610cb4d7ce51cda5040bf9f17c05636b016f.

Revert all "wip dependency insertion"

This is actually a subcase of Merge.

Revert "wip dependency insertion"

This reverts commit 12818e0da31738adbaecf129c1e697633d371cf8.

Revert "wip dependency insertion"

This reverts commit c39f3f1f5a5df2a4d628f335f7aaad44c0f68913.

Revert "wip dependency insertion"

This reverts commit e41fe6dd695b0354aa46929828f0d4ffd604f643.

Revert "wip dependency insertion"

This reverts commit 2e2c0cd70b9a6819e2289a7b07addb6e19f5012c.

Revert "wip dependency insertion"

This reverts commit d357159ce17651ed7deba459e32400636973b827.

Revert "wip dependency insertion"

This reverts commit c759fdf5965e18b0fc6f713b22526ec9464ed7f7.

Revert "wip dependency insertion"

This reverts commit de686ee8ee88dade41eb58f604a89f901b3a13a1.

Revert "wip dependency insertion"

This reverts commit fc96ba0c73d771839a025fc5cb771554cf178eaa.

wip dependency insertion

wip dependency insertion

wip dependency insertion

wip dependency insertion

wip dependency insertion

wip dependency insertion

wip dependency insertion

wip dependency insertion

rename anticommit section

more clarifications and fixes from reread

more clarifications and fixes from reread

more clarifications and fixes from reread

clarifications and fixes from reread

improve wording

improve wording

create base: remove ingredients condition

create base: strengthen create acyclic condition

formatting: a couple of extra [ ]

formatting: section headings on lh pages too

in simple commit rename parent from A to L

add purported proof of calculation of ends

fix calculation of ends formula

assert that exact ancestors is trivial

proof of alternative merge formulation

remove trailing ws

create tip

simple commit foreign inclusion use simple foreign inclusion

introduce and use Totally Foreign Contents

wip create tip

add missing []

improve proof of create base inclusion

create tip wip

introduce macros \pq \pqy \pqn

create base rename cond to create acyclic

create base fix base acyclic and condition

wip create tip

todo list item

use Q not B as patch name in create base

rename Ingredients Prohibit Replay to Prevent

replace various no replay with Ingredients Prohibit Replay

rename merge Ordering of L... to Ordering of Ingredients

create base foreign contents

change Not Applicable [] to Not Applicable

create base foreign inclusion

wip create base

create base coherence fix title

create base fix def

prove and use totally foreign contents

fix some headings

formalise foreign merges

Foreign Contents section in a couple of places

new foreign contents restriction

fix a section => subsection

fix create tip tbd

wip create base

merge conditions into conditions

anticommit clarify note re ingredient order

anticommit conditions into conditions

wip creates

formatting move/add some qeds

simple commit unique base clarification

annotation calculation

fix up some lemmas re ends

a todo item

anticommit foreign inclusion

a todo item

wip anticommit foreign inclusion

merge reference to no replay fix ref to be more regular

anticommit make note re merge base vs merge rhs ordering

anticommit - split out ordering

merge coherence use two implies in statement since equiv cannot represent haspatch and nothaspatch

anticommit coherence

anticommit rename From Base to Into Base

anticommit base acyclic

strengthen anticommit condition to From Base

merge foreign inclusion

move alternative formulation of merge results into lemmas

Prove that plain git merges on non-tb branches are ok

Mention that simple commit justification applies to tb export too

clarify text re non-tb flattened re-inclusion

merge wip

merge tip contents done

merge tip contentss: clarify arbitrariness of D

capitalise a few names