import CubicPathwidth.T4.Assembly
import CubicPathwidth.T4.Process
import CubicPathwidth.T4.SeqH
import CubicPathwidth.T4.TorsoDyn
import CubicPathwidth.T4.Lift
import CubicPathwidth.T4.Basic
import CubicPathwidth.T4.DeletionX
import CubicPathwidth.T4.Cor5S

/-!
# Theorem 4 (all graphs) and Corollary 5 (edges): the approved targets

`target4 : Target4`, `target5 : Target5`.
-/

namespace CubicPathwidth
namespace T4

/-- The bootstrap lemma with base degree 5. -/
theorem bootstrap : BootstrapClaim :=
  bootstrap_of_children ⟨torsoDynamics, liftClaim, kindTwo⟩ basicClaim deletion_x

/-- **Theorem 4**, the approved target `Target4`. -/
theorem target4 : Target4 := target4_of_children seqClaim_h bootstrap

/-- **Corollary 5**, the approved target `Target5`. -/
theorem target5 : Target5 := target5_of_children seqClaim_h bootstrap cor5_s

end T4
end CubicPathwidth

#check (CubicPathwidth.T4.target4 : CubicPathwidth.T4.Target4)
#check (CubicPathwidth.T4.target5 : CubicPathwidth.T4.Target5)
#print axioms CubicPathwidth.T4.target4
#print axioms CubicPathwidth.T4.target5