import AntiDynamics.Strings
import AntiDynamics.Propositional

/-!
# Theorem 1 stated with the literal string definition of Transparency
-/

namespace AntiDyn
namespace Propositional

variable {W ι : Type} (v : W → ι → Bool) (i0 : ι)

/-- **Theorem 1 (i)**, with Transparency defined literally on strings (initial strings `α d̲d'`
of the serialized sentence and arbitrary well-formed completions `β`, paper (26)):
`Transp(C, F)` iff `C[F] ≠ #`. -/
theorem theorem1_i_strings (C : WSet W) (F : PFm ι) :
    (sys v i0).StrTransp C F ↔ (sys v i0).Def F C :=
  ((sys v i0).strTransp_iff_transp C F).trans (theorem1_i v i0 C F)

end Propositional
end AntiDyn