Extending arbitrary Homomorphisms along a Chase Branch

For some results about alternative matches, we need the ability to extend a homomorphisms from the chase node to the chase result into an endomorphism on the chase result (ChaseBranch.hom_for_node_extendable_to_result). We can do this in a step by step fashion along the chase. Although the result is sufficiently different, the construction, in spirit, is similar to the one used in the universality result (chaseTreeResultIsUniversal).

theorem ChaseBranch.hom_for_node_extendable_to_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {cb : ChaseBranch obs kb} (det : kb.rules.isDeterministic) {node : ChaseNode obs kb.rules} (node_mem : node ∈ cb.toChaseDerivation) {h : GroundTermMapping sig} (hom : h.isHomomorphism node.facts cb.result) : ∃ (h' : GroundTermMapping sig), (∀ (t : GroundTerm sig), t ∈ node.facts.terms → h' t = h t) ∧ h'.isHomomorphism cb.result cb.result

Using extend_hom_to_next_step as a generator in PossiblyInfiniteList.generate we can create a possiblibly infinite list of homomorphisms that extend each other and all map to the result. We can combine them into a single function to have an endomorphism on the result. The idea is similar to the construction used in chaseTreeResultIsUniversal.