chiark / gitweb /
topbloke-formulae.git
5 years agorename Tip Self Contents -> Tip Own Contents f0.2
Ian Jackson [Fri, 16 Mar 2012 23:47:45 +0000 (23:47 +0000)]
rename Tip Self Contents -> Tip Own Contents

5 years agorename Tip Self Inpatch -> Tip Self Contents
Ian Jackson [Fri, 16 Mar 2012 23:46:59 +0000 (23:46 +0000)]
rename Tip Self Inpatch -> Tip Self Contents

5 years agosmall fixes
Ian Jackson [Fri, 16 Mar 2012 23:45:16 +0000 (23:45 +0000)]
small fixes

5 years agonon-topbloke merges fix merge ends proof
Ian Jackson [Fri, 16 Mar 2012 23:39:37 +0000 (23:39 +0000)]
non-topbloke merges fix merge ends proof

5 years agobe more rigorous about conformance
Ian Jackson [Fri, 16 Mar 2012 23:14:18 +0000 (23:14 +0000)]
be more rigorous about conformance

5 years agoadd note about non-exclusivity of \haspatch and \nothaspatch
Ian Jackson [Fri, 16 Mar 2012 23:00:18 +0000 (23:00 +0000)]
add note about non-exclusivity of \haspatch and \nothaspatch

5 years agouse new extended Self Tip Inpatch
Ian Jackson [Fri, 16 Mar 2012 23:00:00 +0000 (23:00 +0000)]
use new extended Self Tip Inpatch

5 years agoextend Self Tip Inpatch
Ian Jackson [Fri, 16 Mar 2012 22:53:39 +0000 (22:53 +0000)]
extend Self Tip Inpatch

5 years agoremove a couple of spurious $\qed$
Ian Jackson [Fri, 16 Mar 2012 22:43:22 +0000 (22:43 +0000)]
remove a couple of spurious $\qed$

5 years agoremove spurious .
Ian Jackson [Fri, 16 Mar 2012 22:40:45 +0000 (22:40 +0000)]
remove spurious .

5 years agomerge fixes/clarifications - clarify and fix tip contents R \in \py
Ian Jackson [Fri, 16 Mar 2012 22:34:19 +0000 (22:34 +0000)]
merge fixes/clarifications - clarify and fix tip contents R \in \py

5 years agomerge fixes/clarifications - clarify tip contents R \not\in \py
Ian Jackson [Fri, 16 Mar 2012 22:28:31 +0000 (22:28 +0000)]
merge fixes/clarifications - clarify tip contents R \not\in \py

5 years agomerge fixes/clarifications - sort out complex case D = C
Ian Jackson [Fri, 16 Mar 2012 22:25:11 +0000 (22:25 +0000)]
merge fixes/clarifications - sort out complex case D = C

5 years agomerge fixes/clarifications - fix several P to \p
Ian Jackson [Fri, 16 Mar 2012 22:00:55 +0000 (22:00 +0000)]
merge fixes/clarifications - fix several P to \p

5 years agomerge fixes/clarifications - remove wrong "on R"
Ian Jackson [Fri, 16 Mar 2012 21:59:19 +0000 (21:59 +0000)]
merge fixes/clarifications - remove wrong "on R"

5 years agomerge fixes/clarifications - add missing \
Ian Jackson [Fri, 16 Mar 2012 21:59:10 +0000 (21:59 +0000)]
merge fixes/clarifications - add missing \

5 years agomerge fixes/clarifications - clarify Non-Topbloke merges - add a wlog
Ian Jackson [Fri, 16 Mar 2012 21:57:23 +0000 (21:57 +0000)]
merge fixes/clarifications - clarify Non-Topbloke merges - add a wlog

5 years agomerge fixes/clarifications - clarify Non-Topbloke merges
Ian Jackson [Fri, 16 Mar 2012 21:55:51 +0000 (21:55 +0000)]
merge fixes/clarifications - clarify Non-Topbloke merges

5 years agomerge fixes/clarifications - relax Foreign Merges
Ian Jackson [Fri, 16 Mar 2012 21:55:38 +0000 (21:55 +0000)]
merge fixes/clarifications - relax Foreign Merges

5 years agomerge fixes/clarifications - change , to \land
Ian Jackson [Fri, 16 Mar 2012 21:55:25 +0000 (21:55 +0000)]
merge fixes/clarifications - change , to \land

5 years agosplit into multiple source files
Ian Jackson [Fri, 16 Mar 2012 21:47:37 +0000 (21:47 +0000)]
split into multiple source files

5 years agoremove a spurious \newpage
Ian Jackson [Fri, 16 Mar 2012 21:36:15 +0000 (21:36 +0000)]
remove a spurious \newpage

5 years agomerge ends conditions change order of precondition to put M in middle, for clarity
Ian Jackson [Thu, 15 Mar 2012 19:20:27 +0000 (19:20 +0000)]
merge ends conditions change order of precondition to put M in middle, for clarity

5 years agowording improvement
Ian Jackson [Thu, 15 Mar 2012 19:19:17 +0000 (19:19 +0000)]
wording improvement

5 years agomention that merge can be used for dependency reinsertion
Ian Jackson [Thu, 15 Mar 2012 19:19:07 +0000 (19:19 +0000)]
mention that merge can be used for dependency reinsertion

5 years agoRevert "rename anticommit section"
Ian Jackson [Thu, 15 Mar 2012 19:14:25 +0000 (19:14 +0000)]
Revert "rename anticommit section"

This reverts commit 8649610cb4d7ce51cda5040bf9f17c05636b016f.

5 years agoRevert all "wip dependency insertion"
Ian Jackson [Thu, 15 Mar 2012 19:14:03 +0000 (19:14 +0000)]
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.

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 23:22:20 +0000 (23:22 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 23:18:50 +0000 (23:18 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 23:12:18 +0000 (23:12 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 22:10:04 +0000 (22:10 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 18:37:49 +0000 (18:37 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 18:35:06 +0000 (18:35 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 18:30:42 +0000 (18:30 +0000)]
wip dependency insertion

5 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 18:27:25 +0000 (18:27 +0000)]
wip dependency insertion

5 years agorename anticommit section
Ian Jackson [Wed, 14 Mar 2012 18:20:13 +0000 (18:20 +0000)]
rename anticommit section

5 years agomore clarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 18:04:51 +0000 (18:04 +0000)]
more clarifications and fixes from reread

5 years agomore clarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 17:59:57 +0000 (17:59 +0000)]
more clarifications and fixes from reread

5 years agomore clarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 17:59:28 +0000 (17:59 +0000)]
more clarifications and fixes from reread

5 years agoclarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 17:02:50 +0000 (17:02 +0000)]
clarifications and fixes from reread

5 years agoimprove wording
Ian Jackson [Mon, 12 Mar 2012 16:11:41 +0000 (16:11 +0000)]
improve wording

5 years agoimprove wording
Ian Jackson [Mon, 12 Mar 2012 16:09:29 +0000 (16:09 +0000)]
improve wording

5 years agocreate base: remove ingredients condition
Ian Jackson [Mon, 12 Mar 2012 16:06:18 +0000 (16:06 +0000)]
create base: remove ingredients condition

5 years agocreate base: strengthen create acyclic condition
Ian Jackson [Mon, 12 Mar 2012 16:03:36 +0000 (16:03 +0000)]
create base: strengthen create acyclic condition

5 years agoformatting: a couple of extra [ ]
Ian Jackson [Mon, 12 Mar 2012 15:53:40 +0000 (15:53 +0000)]
formatting: a couple of extra [ ]

5 years agoformatting: section headings on lh pages too
Ian Jackson [Mon, 12 Mar 2012 15:50:59 +0000 (15:50 +0000)]
formatting: section headings on lh pages too

5 years agoin simple commit rename parent from A to L
Ian Jackson [Mon, 12 Mar 2012 15:36:53 +0000 (15:36 +0000)]
in simple commit rename parent from A to L

5 years agoadd purported proof of calculation of ends
Ian Jackson [Mon, 12 Mar 2012 15:35:30 +0000 (15:35 +0000)]
add purported proof of calculation of ends

5 years agofix calculation of ends formula
Ian Jackson [Mon, 12 Mar 2012 15:34:45 +0000 (15:34 +0000)]
fix calculation of ends formula

5 years agoassert that exact ancestors is trivial
Ian Jackson [Mon, 12 Mar 2012 15:17:46 +0000 (15:17 +0000)]
assert that exact ancestors is trivial

5 years agoproof of alternative merge formulation
Ian Jackson [Mon, 12 Mar 2012 15:15:51 +0000 (15:15 +0000)]
proof of alternative merge formulation

5 years agoremove trailing ws
Ian Jackson [Mon, 12 Mar 2012 15:15:37 +0000 (15:15 +0000)]
remove trailing ws

5 years agocreate tip
Ian Jackson [Mon, 12 Mar 2012 14:52:51 +0000 (14:52 +0000)]
create tip

5 years agosimple commit foreign inclusion use simple foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 14:51:27 +0000 (14:51 +0000)]
simple commit foreign inclusion use simple foreign inclusion

5 years agointroduce and use Totally Foreign Contents
Ian Jackson [Mon, 12 Mar 2012 14:48:50 +0000 (14:48 +0000)]
introduce and use Totally Foreign Contents

5 years agowip create tip
Ian Jackson [Mon, 12 Mar 2012 14:38:24 +0000 (14:38 +0000)]
wip create tip

5 years agoadd missing []
Ian Jackson [Mon, 12 Mar 2012 14:37:47 +0000 (14:37 +0000)]
add missing []

5 years agoimprove proof of create base inclusion
Ian Jackson [Mon, 12 Mar 2012 14:37:37 +0000 (14:37 +0000)]
improve proof of create base inclusion

5 years agocreate tip wip
Ian Jackson [Mon, 12 Mar 2012 14:29:08 +0000 (14:29 +0000)]
create tip wip

5 years agointroduce macros \pq \pqy \pqn
Ian Jackson [Mon, 12 Mar 2012 14:28:13 +0000 (14:28 +0000)]
introduce macros \pq \pqy \pqn

5 years agocreate base rename cond to create acyclic
Ian Jackson [Mon, 12 Mar 2012 14:18:49 +0000 (14:18 +0000)]
create base rename cond to create acyclic

5 years agocreate base fix base acyclic and condition
Ian Jackson [Mon, 12 Mar 2012 14:17:50 +0000 (14:17 +0000)]
create base fix base acyclic and condition

5 years agowip create tip
Ian Jackson [Mon, 12 Mar 2012 14:13:49 +0000 (14:13 +0000)]
wip create tip

5 years agotodo list item
Ian Jackson [Mon, 12 Mar 2012 14:13:20 +0000 (14:13 +0000)]
todo list item

5 years agouse Q not B as patch name in create base
Ian Jackson [Mon, 12 Mar 2012 14:12:52 +0000 (14:12 +0000)]
use Q not B as patch name in create base

5 years agorename Ingredients Prohibit Replay to Prevent
Ian Jackson [Mon, 12 Mar 2012 13:57:55 +0000 (13:57 +0000)]
rename Ingredients Prohibit Replay to Prevent

5 years agoreplace various no replay with Ingredients Prohibit Replay
Ian Jackson [Mon, 12 Mar 2012 13:57:35 +0000 (13:57 +0000)]
replace various no replay with Ingredients Prohibit Replay

5 years agorename merge Ordering of L... to Ordering of Ingredients
Ian Jackson [Mon, 12 Mar 2012 13:56:55 +0000 (13:56 +0000)]
rename merge Ordering of L... to Ordering of Ingredients

5 years agocreate base foreign contents
Ian Jackson [Mon, 12 Mar 2012 13:40:27 +0000 (13:40 +0000)]
create base foreign contents

5 years agochange Not Applicable [] to Not Applicable
Ian Jackson [Mon, 12 Mar 2012 13:40:19 +0000 (13:40 +0000)]
change Not Applicable [] to Not Applicable

5 years agocreate base foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 13:39:14 +0000 (13:39 +0000)]
create base foreign inclusion

5 years agowip create base
Ian Jackson [Mon, 12 Mar 2012 08:55:53 +0000 (08:55 +0000)]
wip create base

5 years agocreate base coherence fix title
Ian Jackson [Sun, 11 Mar 2012 17:56:49 +0000 (17:56 +0000)]
create base coherence fix title

5 years agocreate base fix def
Ian Jackson [Sun, 11 Mar 2012 17:56:28 +0000 (17:56 +0000)]
create base fix def

5 years agoprove and use totally foreign contents
Ian Jackson [Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)]
prove and use totally foreign contents

5 years agofix some headings
Ian Jackson [Sun, 11 Mar 2012 17:36:15 +0000 (17:36 +0000)]
fix some headings

5 years agoformalise foreign merges
Ian Jackson [Sun, 11 Mar 2012 17:35:27 +0000 (17:35 +0000)]
formalise foreign merges

5 years agoForeign Contents section in a couple of places
Ian Jackson [Sun, 11 Mar 2012 17:35:13 +0000 (17:35 +0000)]
Foreign Contents section in a couple of places

5 years agonew foreign contents restriction
Ian Jackson [Sun, 11 Mar 2012 17:34:15 +0000 (17:34 +0000)]
new foreign contents restriction

5 years agofix a section => subsection
Ian Jackson [Sun, 11 Mar 2012 16:31:18 +0000 (16:31 +0000)]
fix a section => subsection

5 years agofix create tip tbd
Ian Jackson [Sun, 11 Mar 2012 16:31:09 +0000 (16:31 +0000)]
fix create tip tbd

5 years agowip create base
Ian Jackson [Sun, 11 Mar 2012 16:30:59 +0000 (16:30 +0000)]
wip create base

5 years agomerge conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:36 +0000 (16:09 +0000)]
merge conditions into conditions

5 years agoanticommit clarify note re ingredient order
Ian Jackson [Sun, 11 Mar 2012 16:09:27 +0000 (16:09 +0000)]
anticommit clarify note re ingredient order

5 years agoanticommit conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:14 +0000 (16:09 +0000)]
anticommit conditions into conditions

5 years agowip creates
Ian Jackson [Sun, 11 Mar 2012 15:57:25 +0000 (15:57 +0000)]
wip creates

5 years agoformatting move/add some qeds
Ian Jackson [Sun, 11 Mar 2012 15:56:43 +0000 (15:56 +0000)]
formatting move/add some qeds

5 years agosimple commit unique base clarification
Ian Jackson [Sun, 11 Mar 2012 15:52:47 +0000 (15:52 +0000)]
simple commit unique base clarification

5 years agoannotation calculation
Ian Jackson [Sun, 11 Mar 2012 15:51:52 +0000 (15:51 +0000)]
annotation calculation

5 years agofix up some lemmas re ends
Ian Jackson [Sun, 11 Mar 2012 14:21:01 +0000 (14:21 +0000)]
fix up some lemmas re ends

5 years agoa todo item
Ian Jackson [Sun, 11 Mar 2012 14:07:39 +0000 (14:07 +0000)]
a todo item

5 years agoanticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 14:05:33 +0000 (14:05 +0000)]
anticommit foreign inclusion

5 years agoa todo item
Ian Jackson [Sun, 11 Mar 2012 13:10:57 +0000 (13:10 +0000)]
a todo item

5 years agowip anticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 12:44:56 +0000 (12:44 +0000)]
wip anticommit foreign inclusion

5 years agomerge reference to no replay fix ref to be more regular
Ian Jackson [Sun, 11 Mar 2012 12:35:23 +0000 (12:35 +0000)]
merge reference to no replay fix ref to be more regular

5 years agoanticommit make note re merge base vs merge rhs ordering
Ian Jackson [Sun, 11 Mar 2012 12:34:59 +0000 (12:34 +0000)]
anticommit make note re merge base vs merge rhs ordering

5 years agoanticommit - split out ordering
Ian Jackson [Sun, 11 Mar 2012 12:31:53 +0000 (12:31 +0000)]
anticommit - split out ordering

5 years agomerge coherence use two implies in statement since equiv cannot represent haspatch...
Ian Jackson [Sun, 11 Mar 2012 12:24:03 +0000 (12:24 +0000)]
merge coherence use two implies in statement since equiv cannot represent haspatch and nothaspatch

5 years agoanticommit coherence
Ian Jackson [Sun, 11 Mar 2012 12:23:37 +0000 (12:23 +0000)]
anticommit coherence

5 years agoanticommit rename From Base to Into Base
Ian Jackson [Sun, 11 Mar 2012 12:08:10 +0000 (12:08 +0000)]
anticommit rename From Base to Into Base