Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withoutTemps (LeanSAT/Encode/EncCNF.lean)

State before:
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
⊢ interp (withoutTemps s vMap vMapLt vMapInj av) = fun τ => ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Tactic:
ext τ
State after:
case h.a
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
τ : PropAssignment ν
⊢ interp (withoutTemps s vMap vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ

State before:
case h.a
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
τ : PropAssignment ν
⊢ interp (withoutTemps s vMap vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Tactic:
cases h
State after:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ interp (withoutTemps s (s.vMap ∘ Sum.inl) vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ

State before:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ interp (withoutTemps s (s.vMap ∘ Sum.inl) vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Tactic:
simp [LawfulState.withoutTemps, State.withoutTemps, interp]
State after:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ (∃ σ, τ = PropAssignment.map (s.vMap ∘ Sum.inl) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ ∃ σ_1, σ = PropAssignment.map s.vMap σ_1 ∧ σ_1 ⊨ Cnf.toPropFun s.cnf

State before:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ (∃ σ, τ = PropAssignment.map (s.vMap ∘ Sum.inl) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ ∃ σ_1, σ = PropAssignment.map s.vMap σ_1 ∧ σ_1 ⊨ Cnf.toPropFun s.cnf
Tactic:
aesop
State after:
no goals