Theorem: PropagateStruc.eval_decr (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval decr x = decrSeq (x ())
Tactic:
dsimp [decr, eval]
State after:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ()))) x =
    decrSeq (x ())

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ()))) x =
    decrSeq (x ())
Tactic:
rw [decr_eq_propagate]
State after:
no goals