Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig expr).val.aig.decls.size
⊢ (go aig expr).val.aig.decls[idx] = aig.decls[idx]
Tactic:
induction expr generalizing aig with
| var =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastVar)]
| const =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastConst)]
| bin lhs op rhs lih rih =>
  match op with
  | .and | .or | .xor =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := AIG.RefStream.zip)]
    rw [rih, lih]
    . apply Nat.lt_of_lt_of_le
      . exact h1
      . exact (bitblast.go aig lhs).property
    . apply Nat.lt_of_lt_of_le
      . exact h1
      . apply Nat.le_trans
        . exact (bitblast.go aig lhs).property
        . exact (go (go aig lhs).1.aig rhs).property
  | .add =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastAdd)]
    rw [rih, lih]
    . apply Nat.lt_of_lt_of_le
      . exact h1
      . exact (bitblast.go aig lhs).property
    . apply Nat.lt_of_lt_of_le
      . exact h1
      . apply Nat.le_trans
        . exact (bitblast.go aig lhs).property
        . exact (go (go aig lhs).1.aig rhs).property
| un op expr ih =>
  match op with
  | .not =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastNot)]
    rw [ih]
    apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (go aig expr).property
  | .shiftLeftConst _ =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftLeftConst)]
    rw [ih]
    apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (go aig expr).property
  | .shiftRightConst _ =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftRightConst)]
    rw [ih]
    apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (go aig expr).property
  | .rotateLeft _ =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastRotateLeft)]
    rw [ih]
    apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (go aig expr).property
  | .rotateRight _ =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastRotateRight)]
    rw [ih]
    apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (go aig expr).property
  | .arithShiftRightConst _ =>
    dsimp [go]
    rw [AIG.LawfulStreamOperator.decl_eq (f := blastArithShiftRightConst)]
    rw [ih]
    apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (go aig expr).property
| zeroExtend w inner ih =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastZeroExtend)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig inner).property
| signExtend w inner ih =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastSignExtend)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig inner).property
| append lhs rhs lih rih =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastAppend)]
  rw [rih, lih]
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (bitblast.go aig lhs).property
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . apply Nat.le_trans
      . exact (bitblast.go aig lhs).property
      . exact (go (go aig lhs).1.aig rhs).property
| extract hi lo inner ih =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastExtract)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig inner).property
Proof state after:
no goals