Version 0.3 Alpha bool2.  

Heretofore, every effort will be made to include a release at the end of
each year, before Winter Solstice.  This consistency means however,
that sometimes releases won't be complete, and this latest
release of BooleanAlgebrasIntro2, Version 0.3 Alpha, 2019,
defers one last step in the Recursion Theorem (subterm injectivity)
to next release.  There is still some sloppy old code from
Boolean algebras that needs to be cleaned, although much has been cleaned.

Version 0.3 finds us switching from Boolean agebras altogether, into,
first function algebras, then partial algebras.
The handful of definitions and theorems used from function algebras
are taken from Dietlinde Lau's "Function Algebras on Finite Sets."
Eventually, we are driven to our final course, 
translating Horst Reichel's "Initial Computability, Algebraic Specifications, 
and Partial Algebras," into Coq.  This huge task will hopefully
occupy my main efforts for the next forty or so years!

The reason for the switch is complicated and philosophical.  

The last version (0.2) culminated in Sikorski's Extension Criterion,
and this version includes many corollaries and variants of that,
like the monomorphism criterion, and finitary/countable versions.
We also dabble a bit with atomless Boolean algebras, and a few experiments
in original definitions.  
There are also many new utilities files, and the finite maps library
has been made more resistant to the law of excluded middle, and
cleaned up.  It's still far from fully clean, though.  

The big news metaphysically, though, is that this software project succeeds
so well in interacting with the Sun Spirit 
that it's no longer safe to use during the day!
During peak magnetic fluctuations from the sun,
the computer displays signs of digital possession, by glitchy typing,
and arbitrary repetitions of keyboard stokes in the shell.
It's intermittent, some days working some days not, but it always
works at night.
Whether or not I'm right in my conclusion is not really the point,
but rather the point is code, hidden digital interfaces,
and tracing broken symmetries.  
Hopefully the manner of possession will change as we progress since,
this metaphysical divide is the whole point of bool2.

The most practical use of bool2 is hardware certification,
but the whole fun and excitement comes from the digital spaces we are
also certifying, and the mysterious aspect!
Digital and financial alchemy, other possibilities, I know little about,
but have seen glimpses of.  

The plan from now on is to upgrade versions of Coq after each release.
This version 0.3 still uses Version 8.4pl4 of Coq. An effort will be made
to keep the version consistent with the current LTS Ubuntu release.

-- Daniel Wyckoff,
dwyckoff76@remove.the.excess.around.hotmail.com.kaka