Theorem: AIG.denote_mkGate (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ ⟦aig.mkGate input, assign⟧ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
conv =>
  lhs
  unfold denote denote.go
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
split
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
. next heq =>
  rw [mkGate, Array.get_push_size] at heq
  contradiction
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
. next heq =>
  rw [mkGate, Array.get_push_size] at heq
  contradiction
State after:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
. next heq =>
  rw [mkGate, Array.get_push_size] at heq
  injection heq with heq1 heq2 heq3 heq4
  dsimp
  congr 2
  . unfold denote
    simp only [heq1]
    apply denote.go_eq_of_aig_eq
    apply LawfulOperator.IsPrefix_aig
  . simp [heq3]
  . unfold denote
    simp only [heq2]
    apply denote.go_eq_of_aig_eq
    apply LawfulOperator.IsPrefix_aig
  . simp [heq4]
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
next heq =>
rw [mkGate, Array.get_push_size] at heq
contradiction
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
rw [mkGate, Array.get_push_size] at heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
contradiction
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
next heq =>
rw [mkGate, Array.get_push_size] at heq
contradiction
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
rw [mkGate, Array.get_push_size] at heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
contradiction
State after:
no goals

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
next heq =>
rw [mkGate, Array.get_push_size] at heq
injection heq with heq1 heq2 heq3 heq4
dsimp
congr 2
. unfold denote
  simp only [heq1]
  apply denote.go_eq_of_aig_eq
  apply LawfulOperator.IsPrefix_aig
. simp [heq3]
. unfold denote
  simp only [heq2]
  apply denote.go_eq_of_aig_eq
  apply LawfulOperator.IsPrefix_aig
. simp [heq4]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
rw [mkGate, Array.get_push_size] at heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
injection heq with heq1 heq2 heq3 heq4
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ (xor (denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯) linv✝ &&
      xor (denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯) rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ (xor (denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯) linv✝ &&
      xor (denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯) rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
congr 2
State after:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧

case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv

State before:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧

case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv
Tactic:
. unfold denote
  simp only [heq1]
  apply denote.go_eq_of_aig_eq
  apply LawfulOperator.IsPrefix_aig
State after:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv

State before:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv
Tactic:
. simp [heq3]
State after:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv

State before:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv
Tactic:
. unfold denote
  simp only [heq2]
  apply denote.go_eq_of_aig_eq
  apply LawfulOperator.IsPrefix_aig
State after:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv

State before:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv
Tactic:
. simp [heq4]
State after:
no goals

State before:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧
Tactic:
unfold denote
State after:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ =
    denote.go { aig := aig, ref := input.lhs.ref }.ref.gate { aig := aig, ref := input.lhs.ref }.aig.decls assign ⋯ ⋯

State before:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ =
    denote.go { aig := aig, ref := input.lhs.ref }.ref.gate { aig := aig, ref := input.lhs.ref }.aig.decls assign ⋯ ⋯
Tactic:
simp only [heq1]
State after:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = denote.go lidx✝ aig.decls assign ⋯ ⋯

State before:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = denote.go lidx✝ aig.decls assign ⋯ ⋯
Tactic:
apply denote.go_eq_of_aig_eq
State after:
case e_x.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ IsPrefix aig.decls (aig.mkGate input).aig.decls

State before:
case e_x.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ IsPrefix aig.decls (aig.mkGate input).aig.decls
Tactic:
apply LawfulOperator.IsPrefix_aig
State after:
no goals

State before:
case e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv
Tactic:
simp [heq3]
State after:
no goals

State before:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧
Tactic:
unfold denote
State after:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ =
    denote.go { aig := aig, ref := input.rhs.ref }.ref.gate { aig := aig, ref := input.rhs.ref }.aig.decls assign ⋯ ⋯

State before:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ =
    denote.go { aig := aig, ref := input.rhs.ref }.ref.gate { aig := aig, ref := input.rhs.ref }.aig.decls assign ⋯ ⋯
Tactic:
simp only [heq2]
State after:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = denote.go ridx✝ aig.decls assign ⋯ ⋯

State before:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = denote.go ridx✝ aig.decls assign ⋯ ⋯
Tactic:
apply denote.go_eq_of_aig_eq
State after:
case e_y.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ IsPrefix aig.decls (aig.mkGate input).aig.decls

State before:
case e_y.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ IsPrefix aig.decls (aig.mkGate input).aig.decls
Tactic:
apply LawfulOperator.IsPrefix_aig
State after:
no goals

State before:
case e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv
Tactic:
simp [heq4]
State after:
no goals