Procedural Proof

The proof of the Independent Boundary Theorem in a previous post is incorrect because I failed to establish an isomorphism before applying the Antisection Theorem. To make the Independent Boundary Theorem proof more precise, I will present it as a method called extend in a class called Space. Other methods left undefined are the linear function that returns whether the given Space is linear, section and antisection that work like the Section Theorem and Antisection Theorem, and the take function. The take function converts regions from one Space to regions on the same side of shared boundaries in another Space. If both the containing Space and the given Space have the same boundaries, then take finds isomorphic regions; otherwise, take finds super-regions or sub-regions.
Space Space::extend(
  const Space &S0,
  const Space &S1,
  const int b0,
  const int b1) const {
  assert(linear());
  assert(S0.linear());
  assert(S1.linear());
  assert(boundaries()==S0.boundaries());
  assert(boundaries()==S1.boundaries());
  assert(dimension()==S0.dimension()+1);
  assert(dimension()==S1.dimension()+1);
  assert(take(S0.regions(),S0).size()==S0.regions().size());
  assert(take(S1.regions(),S1).size()==S1.regions().size());
  assert(!boundaries().contains(b0));
  assert(!boundaries().contains(b1));
  Space S2 = antisection(take(S0.regions(),S0),b0); // n2=n
  if (dimension()==1) {
    return S2.antisection(S2.take(S1.regions(),S1).choose(),b1);}
  Space S3 = subsection(S0,S1); // n3=n-1+n-1-n=n-2
  Space S4 = S1.antisection(S1.take(S3.regions(),S3),b0); // n4=n-1
  Space S5 = S2.antisection(S2.take(S4.regions(),S4),b1); // n5=n
  set<int> B0 = S5.boundaries().erase(b1);
  set<int> B1 = S5.boundaries().erase(b0);
  assert(S5.subspace(B0)==antisection(take(S0.regions(),S0),b0));
  assert(S5.subspace(B1)==antisection(take(S1.regions(),S1),b1));
  assert(S5.linear());
  return S5;}
Space Space::subsection(
  const Space &S0,
  const Space &S1) const {
  assert(linear());
  assert(S0.linear());
  assert(S1.linear()):
  assert(boundaries()==S0.boundaries());
  assert(boundaries()==S1.boundaries());
  int n = dimension();
  int n0 = S0.dimension();
  int n1 = S1.dimension();
  assert(n0+n1-n>=0);
  if (boundaries().size()==0) {
    return Space(n0+n1-n);}
  int b = boundaries().choose();
  set<int> B = boundaries().erase(b);
  set<int> R = attached(b);
  Space S2 = subspace(B); // n2=n
  Space S3 = S0.subspace(B); // n3=n0
  Space S4 = S1.subspace(B); // n4=n1
  Space S5 = S2.section(S2.take(R,*this)); // n5=n-1
  Space S6 = S2.subsection(S3,S4); // n6=n0+n1-n
  Space S7 = S2.subsection(S5,S6); // n7=n-1+n0+n1-n-n=n0+n1-n-1
  Space S8 = S6.antisection(S6.take(S7.regions(),S7),b); // n8=n0+n1-n
  assert(S8.dimension()==n0+n1-n);
  assert(take(S0.regions(),S0).contains(take(S8.regions(),S8)));
  assert(take(S1.regions(),S1).contains(take(S8.regions(),S8)));
  assert(S8.linear());
  return S8;}