Theorem: AIG.denote.go_eq_of_aig_eq (LeanSAT/AIG/LawfulOperator.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
⊢ go start decls2 assign hbounds2 hdag2 = go start decls1 assign hbounds1 hdag1
Tactic:
unfold denote.go
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
⊢ (match elem : decls2[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls2 assign ⋯ hdag2;
      let rval := go rhs decls2 assign ⋯ hdag2;
      xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
⊢ (match elem : decls2[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls2 assign ⋯ hdag2;
      let rval := go rhs decls2 assign ⋯ hdag2;
      xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
have hidx1 := hprefix.idx_eq start hbounds1
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
⊢ (match elem : decls2[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls2 assign ⋯ hdag2;
      let rval := go rhs decls2 assign ⋯ hdag2;
      xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
⊢ (match elem : decls2[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls2 assign ⋯ hdag2;
      let rval := go rhs decls2 assign ⋯ hdag2;
      xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
split
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq✝ : decls2[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq✝ : decls2[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
. next heq =>
  rw [hidx1] at heq
  split <;> simp_all
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
. next heq =>
  rw [hidx1] at heq
  split <;> simp_all
State after:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
. next lhs rhs linv rinv heq =>
  rw [hidx1] at heq
  have foo := hdag1 start lhs rhs linv rinv hbounds1 heq
  have hidx2 := hprefix.idx_eq lhs (by omega)
  have hidx3 := hprefix.idx_eq rhs (by omega)
  split
  . simp_all
  . simp_all
  . simp_all
    congr 2
    . apply denote.go_eq_of_aig_eq
      assumption
    . apply denote.go_eq_of_aig_eq
      assumption
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq✝ : decls2[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
next heq =>
rw [hidx1] at heq
split <;> simp_all
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq : decls2[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
rw [hidx1] at heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq : decls1[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq : decls1[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
split <;> simp_all
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
next heq =>
rw [hidx1] at heq
split <;> simp_all
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
rw [hidx1] at heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq : decls1[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq : decls1[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
split <;> simp_all
State after:
no goals

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
next lhs rhs linv rinv heq =>
rw [hidx1] at heq
have foo := hdag1 start lhs rhs linv rinv hbounds1 heq
have hidx2 := hprefix.idx_eq lhs (by omega)
have hidx3 := hprefix.idx_eq rhs (by omega)
split
. simp_all
. simp_all
. simp_all
  congr 2
  . apply denote.go_eq_of_aig_eq
    assumption
  . apply denote.go_eq_of_aig_eq
    assumption
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq : decls2[start] = Decl.gate lhs rhs linv rinv
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
rw [hidx1] at heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
have foo := hdag1 start lhs rhs linv rinv hbounds1 heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
have hidx2 := hprefix.idx_eq lhs (by omega)
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
have hidx3 := hprefix.idx_eq rhs (by omega)
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
split
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
b✝ : Bool
heq✝ : decls1[start] = Decl.const b✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    b✝

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
idx✝ : α
heq✝ : decls1[start] = Decl.atom idx✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    assign idx✝

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
b✝ : Bool
heq✝ : decls1[start] = Decl.const b✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    b✝

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
idx✝ : α
heq✝ : decls1[start] = Decl.atom idx✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    assign idx✝

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝
Tactic:
. simp_all
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
idx✝ : α
heq✝ : decls1[start] = Decl.atom idx✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    assign idx✝

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
idx✝ : α
heq✝ : decls1[start] = Decl.atom idx✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    assign idx✝

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝
Tactic:
. simp_all
State after:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝
Tactic:
. simp_all
  congr 2
  . apply denote.go_eq_of_aig_eq
    assumption
  . apply denote.go_eq_of_aig_eq
    assumption
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
⊢ lhs < decls1.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
⊢ rhs < decls1.size
Tactic:
omega
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
b✝ : Bool
heq✝ : decls1[start] = Decl.const b✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    b✝
Tactic:
simp_all
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
idx✝ : α
heq✝ : decls1[start] = Decl.atom idx✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    assign idx✝
Tactic:
simp_all
State after:
no goals

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lhs rhs : Nat
linv rinv : Bool
heq✝¹ : decls2[start] = Decl.gate lhs rhs linv rinv
heq : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    let_fun this := ⋯;
    let lval := go lidx✝ decls1 assign ⋯ hdag1;
    let rval := go ridx✝ decls1 assign ⋯ hdag1;
    xor lval linv✝ && xor rval rinv✝
Tactic:
simp_all
State after:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ (xor (go lhs decls2 assign ⋯ hdag2) linv && xor (go rhs decls2 assign ⋯ hdag2) rinv) =
    (xor (go lhs decls1 assign ⋯ hdag1) linv && xor (go rhs decls1 assign ⋯ hdag1) rinv)

State before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ (xor (go lhs decls2 assign ⋯ hdag2) linv && xor (go rhs decls2 assign ⋯ hdag2) rinv) =
    (xor (go lhs decls1 assign ⋯ hdag1) linv && xor (go rhs decls1 assign ⋯ hdag1) rinv)
Tactic:
congr 2
State after:
case h_3.e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go lhs decls2 assign ⋯ hdag2 = go lhs decls1 assign ⋯ hdag1

case h_3.e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go rhs decls2 assign ⋯ hdag2 = go rhs decls1 assign ⋯ hdag1

State before:
case h_3.e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go lhs decls2 assign ⋯ hdag2 = go lhs decls1 assign ⋯ hdag1

case h_3.e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go rhs decls2 assign ⋯ hdag2 = go rhs decls1 assign ⋯ hdag1
Tactic:
. apply denote.go_eq_of_aig_eq
  assumption
State after:
case h_3.e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go rhs decls2 assign ⋯ hdag2 = go rhs decls1 assign ⋯ hdag1

State before:
case h_3.e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go rhs decls2 assign ⋯ hdag2 = go rhs decls1 assign ⋯ hdag1
Tactic:
. apply denote.go_eq_of_aig_eq
  assumption
State after:
no goals

State before:
case h_3.e_x.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go lhs decls2 assign ⋯ hdag2 = go lhs decls1 assign ⋯ hdag1
Tactic:
apply denote.go_eq_of_aig_eq
State after:
case h_3.e_x.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ IsPrefix decls1 decls2

State before:
case h_3.e_x.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ IsPrefix decls1 decls2
Tactic:
assumption
State after:
no goals

State before:
case h_3.e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go rhs decls2 assign ⋯ hdag2 = go rhs decls1 assign ⋯ hdag1
Tactic:
apply denote.go_eq_of_aig_eq
State after:
case h_3.e_y.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ IsPrefix decls1 decls2

State before:
case h_3.e_y.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ IsPrefix decls1 decls2
Tactic:
assumption
State after:
no goals