Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GeneratedGraphDefinitions

Supporting results for pointwise provable equality.

Definitions and closure laws for the generated graph congruence.

source
def PointwiseComposition.FailureOfComposition.GeneratedCongruence.Rel (T : FFL.FirstOrder.ArithmeticTheory) (F G : ProofSearch.FunctionalGraph) :
Prop

The least composition congruence on PA-functional Sigma-one graphs containing external pointwise provability in T.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_base (T : FFL.FirstOrder.ArithmeticTheory) {F G : ProofSearch.FunctionalGraph} (h : ProofSearch.Pointwise T ↑F ↑G) :
    Rel T F G
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_refl (T : FFL.FirstOrder.ArithmeticTheory) (F : ProofSearch.FunctionalGraph) :
    Rel T F F
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_symm (T : FFL.FirstOrder.ArithmeticTheory) {F G : ProofSearch.FunctionalGraph} (h : Rel T F G) :
    Rel T G F
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_trans (T : FFL.FirstOrder.ArithmeticTheory) {F G H : ProofSearch.FunctionalGraph} (hFG : Rel T F G) (hGH : Rel T G H) :
    Rel T F H
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_comp (T : FFL.FirstOrder.ArithmeticTheory) {F F' G G' : ProofSearch.FunctionalGraph} (hF : Rel T F F') (hG : Rel T G G') :
    Rel T (ProofSearch.functionalComp F G) (ProofSearch.functionalComp F' G')
    source
    theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.rel_of_uniform (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] {F G : ProofSearch.FunctionalGraph} (h : ProofSearch.Uniform 𝐏𝐀 ↑F ↑G) :
    Rel T F G
    source
    def PointwiseComposition.FailureOfComposition.GeneratedCongruence.graphSetoid (T : FFL.FirstOrder.ArithmeticTheory) :
    Setoid ProofSearch.FunctionalGraph

    The graph Setoid construction in FailureOfComposition.GeneratedCongruence.

    Equations
    Instances For