Primitive Recursiveness of Saturation Step

This file proves that the saturation step function satStep is primitive recursive, which is needed for the computability proof of context-free membership.

Triple list membership is Primrec

matchOneSym helper is Primrec

matchRHS is Primrec

satStep is Primrec

theorem satStep_primrec_full {T : Type} [DecidableEq T] [Primcodable T] : Primrec fun (p : (ℕ × List (ℕ × List (ℕ ⊕ T)) × List T) × List (ℕ × ℕ × ℕ)) => satStep p.1.1 p.1.2.1 p.1.2.2 p.2

satStep is Primrec as a function of bundled parameters.

Iteration of satStep is Primrec

checkMembershipEncoded is Computable

theorem checkMembershipEncoded_computable' {T : Type} [DecidableEq T] [Primcodable T] [Fintype T] : Computable checkMembershipEncoded