FormalConjectures.Paper.BranchingVAS

FormalConjectures
Paper
BranchingVAS

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesUtil

Decidability of reachability for branching vector addition systems

A branching vector addition system (BVAS) of dimension d is given by a finite list of axioms, a finite list of unary rules, and a finite list of binary rules, each of which is a vector in ℤ^d. A configuration is a vector in ℕ^d, which here is represented as a vector v ∈ ℤ^d subject to 0 ≤ v. The set of reachable configurations is defined inductively:

every axiom that is a valid configuration (i.e. lies in ℕ^d) is reachable;

if v is a reachable configuration, r is a unary rule and v + r ∈ ℕ^d, then v + r is reachable;

if v₁, v₂ are both reachable configurations, r is a binary rule and v₁ + v₂ + r ∈ ℕ^d, then v₁ + v₂ + r is reachable.

Modelling axioms as vectors in ℤ^d and only counting the non-negative ones as reachable yields the same set of reachable configurations as the usual definition in which axioms are required to lie in ℕ^d.

Branching vector addition systems are distinguished from ordinary vector addition systems (VAS) by allowing binary rules. VAS reachability is known to be decidable.

References:

The covering and boundedness problems for branching vector addition systems (Stéphane Demri, Marcin Jurdziński, Oded Lachish, Ranko Lazić, FSTTCS 2009) Gives a similar definition of BVAS, and compares it to related equivalent definitions.

On the Reachability Problem for Two-Dimensional Branching VASS by Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, Grégoire Sutre, MFCS 2025, which settles the two-dimensional case and states that "the decidability status of the reachability problem for BVASS remains open in higher dimensions".

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants by Jérôme Leroux (2010), for the decidability of reachability for ordinary VAS.

Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants by Clotilde Bizière, Jérôme Leroux, Grégoire Sutre (2026), a recent preprint claiming a positive resolution to the conjecture: reachability for branching vector addition systems is decidable.

@[expose] public sectionnamespace BranchingVAS

A branching vector addition system of dimension d.

structure Bvas (d : ℕ) where
  axioms : List (Fin d → ℤ)
  unaryRules : List (Fin d → ℤ)
  binaryRules : List (Fin d → ℤ)

The reachable configurations of a branching vector addition system.

inductive Bvas.Reachable {d : ℕ} (b : Bvas d) : (Fin d → ℤ) → Prop
  | base {v : Fin d → ℤ} (hmem : v ∈ b.axioms) (hcfg : 0 ≤ v) : b.Reachable v
  | unary {v r w : Fin d → ℤ} (hv : b.Reachable v) (hr : r ∈ b.unaryRules)
      (hcfg : 0 ≤ w) (hw : w = v + r) : b.Reachable w
  | binary {v₁ v₂ r w : Fin d → ℤ} (hv₁ : b.Reachable v₁) (hv₂ : b.Reachable v₂)
      (hr : r ∈ b.binaryRules) (hcfg : 0 ≤ w) (hw : w = v₁ + v₂ + r) : b.Reachable w

The vector in ℤ^d whose i-th coordinate is the i-th entry of the list l, or 0 if l has fewer than i + 1 entries. Used to encode the inputs of the reachability problem.

def vecOfList (d : ℕ) (l : List ℤ) : Fin d → ℤ := fun i => l.getD i 0

@[category API, AMS 3 68]
theorem vecOfList_ofFn {d : ℕ} (v : Fin d → ℤ) : vecOfList d (List.ofFn v) = v := byd:ℕv:Fin d → ℤ⊢ vecOfList d (List.ofFn v) = v
  funext id:ℕv:Fin d → ℤi:Fin d⊢ vecOfList d (List.ofFn v) i = v i
  simp [vecOfList, List.getD_eq_getElem?_getD]All goals completed! 🐙



@[category API, AMS 3 68]
theorem ofFn_vecOfList (d : ℕ) (l : List ℤ) :
    List.ofFn (vecOfList d l) = (List.range d).map fun i => l.getD i 0 := byd:ℕl:List ℤ⊢ List.ofFn (vecOfList d l) = List.map (fun i ↦ l.getD i 0) (List.range d)
  rw [List.ofFn_eq_map,d:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map (fun i ↦ l.getD i 0) (List.range d)d:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map ((fun i ↦ l.getD i 0) ∘ fun x ↦ ↑x) (List.finRange d) ← List.map_coe_finRange_eq_range,d:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map (fun i ↦ l.getD i 0) (List.map (fun x ↦ ↑x) (List.finRange d))d:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map ((fun i ↦ l.getD i 0) ∘ fun x ↦ ↑x) (List.finRange d) List.map_mapd:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map ((fun i ↦ l.getD i 0) ∘ fun x ↦ ↑x) (List.finRange d)d:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map ((fun i ↦ l.getD i 0) ∘ fun x ↦ ↑x) (List.finRange d)]d:ℕl:List ℤ⊢ List.map (vecOfList d l) (List.finRange d) = List.map ((fun i ↦ l.getD i 0) ∘ fun x ↦ ↑x) (List.finRange d)
  rflAll goals completed! 🐙

@[category API, AMS 3 68]
theorem primrec_ofFn_vecOfList : Primrec₂ fun d l => List.ofFn (vecOfList d l) :=
  (Primrec.list_map (Primrec.list_range.comp Primrec.fst)
    ((Primrec.list_getD 0).comp₂ (Primrec.snd.comp₂ Primrec₂.left) Primrec₂.right)).of_eq
      fun ⟨d, l⟩ => (ofFn_vecOfList d l).symm

An input of the reachability problem, that is, a dimension d, a branching vector addition system of dimension d and a target vector in ℤ^d, is encoded by d together with the lists of entries of the axioms, of the rules and of the target.

instance : Primcodable (Σ d : ℕ, Bvas d × (Fin d → ℤ)) :=
  Primcodable.ofLeftInverse
    (fun p => (p.1, p.2.1.axioms.map List.ofFn, p.2.1.unaryRules.map List.ofFn,
      p.2.1.binaryRules.map List.ofFn, List.ofFn p.2.2))
    (fun q => ⟨q.1, ⟨q.2.1.map (vecOfList q.1), q.2.2.1.map (vecOfList q.1),
      q.2.2.2.1.map (vecOfList q.1)⟩, vecOfList q.1 q.2.2.2.2⟩)
    (fun p => byp:(d : ℕ) × Bvas d × (Fin d → ℤ)⊢ ⟨(p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
        List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).1,
    ({
        axioms :=
          List.map
            (vecOfList
              (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                  List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).1)
            (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                  List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).2.1,
        unaryRules :=
          List.map
            (vecOfList
              (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                  List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).1)
            (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                    List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).2.2.1,
        binaryRules :=
          List.map
            (vecOfList
              (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                  List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).1)
            (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                      List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).2.2.2.1 },
      vecOfList
        (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
            List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).1
        (p.fst, List.map List.ofFn p.snd.1.axioms, List.map List.ofFn p.snd.1.unaryRules,
                  List.map List.ofFn p.snd.1.binaryRules, List.ofFn p.snd.2).2.2.2.2)⟩ =
  p simp [List.map_map, Function.comp_def, vecOfList_ofFn]All goals completed! 🐙)
    (by⊢ Primrec fun a ↦
  (⟨a.1,
        ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
            binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
          vecOfList a.1 a.2.2.2.2)⟩.fst,
    List.map List.ofFn
      ⟨a.1,
              ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                  binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
                vecOfList a.1 a.2.2.2.2)⟩.snd.1.axioms,
    List.map List.ofFn
      ⟨a.1,
              ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                  binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
                vecOfList a.1 a.2.2.2.2)⟩.snd.1.unaryRules,
    List.map List.ofFn
      ⟨a.1,
              ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                  binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
                vecOfList a.1 a.2.2.2.2)⟩.snd.1.binaryRules,
    List.ofFn
      ⟨a.1,
            ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
              vecOfList a.1 a.2.2.2.2)⟩.snd.2)
      have h : Primrec fun q : ℕ × List (List ℤ) × List (List ℤ) × List (List ℤ) × List ℤ =>
          (q.1, q.2.1.map fun l => List.ofFn (vecOfList q.1 l),
            q.2.2.1.map fun l => List.ofFn (vecOfList q.1 l),
            q.2.2.2.1.map fun l => List.ofFn (vecOfList q.1 l),
            List.ofFn (vecOfList q.1 q.2.2.2.2)) :=
        Primrec.pair Primrec.fst <| Primrec.pair (Primrec.list_map (Primrec.fst.comp Primrec.snd)
            (primrec_ofFn_vecOfList.comp₂ (Primrec.fst.comp₂ Primrec₂.left) Primrec₂.right)) <|
          Primrec.pair (Primrec.list_map (Primrec.fst.comp <| Primrec.snd.comp Primrec.snd)
            (primrec_ofFn_vecOfList.comp₂ (Primrec.fst.comp₂ Primrec₂.left) Primrec₂.right)) <|
          Primrec.pair
            (Primrec.list_map
              (Primrec.fst.comp <| Primrec.snd.comp <| Primrec.snd.comp Primrec.snd)
              (primrec_ofFn_vecOfList.comp₂ (Primrec.fst.comp₂ Primrec₂.left) Primrec₂.right))
            (primrec_ofFn_vecOfList.comp Primrec.fst
              (Primrec.snd.comp <| Primrec.snd.comp <| Primrec.snd.comp Primrec.snd))h:Primrec fun q ↦
  (q.1, List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.1, List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.2.1,
    List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.2.2.1, List.ofFn (vecOfList q.1 q.2.2.2.2))⊢ Primrec fun a ↦
  (⟨a.1,
        ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
            binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
          vecOfList a.1 a.2.2.2.2)⟩.fst,
    List.map List.ofFn
      ⟨a.1,
              ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                  binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
                vecOfList a.1 a.2.2.2.2)⟩.snd.1.axioms,
    List.map List.ofFn
      ⟨a.1,
              ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                  binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
                vecOfList a.1 a.2.2.2.2)⟩.snd.1.unaryRules,
    List.map List.ofFn
      ⟨a.1,
              ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                  binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
                vecOfList a.1 a.2.2.2.2)⟩.snd.1.binaryRules,
    List.ofFn
      ⟨a.1,
            ({ axioms := List.map (vecOfList a.1) a.2.1, unaryRules := List.map (vecOfList a.1) a.2.2.1,
                binaryRules := List.map (vecOfList a.1) a.2.2.2.1 },
              vecOfList a.1 a.2.2.2.2)⟩.snd.2)
      exact h.of_eq fun q => byh:Primrec fun q ↦
  (q.1, List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.1, List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.2.1,
    List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.2.2.1, List.ofFn (vecOfList q.1 q.2.2.2.2))q:ℕ × List (List ℤ) × List (List ℤ) × List (List ℤ) × List ℤ⊢ (q.1, List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.1, List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.2.1,
    List.map (fun l ↦ List.ofFn (vecOfList q.1 l)) q.2.2.2.1, List.ofFn (vecOfList q.1 q.2.2.2.2)) =
  (⟨q.1,
        ({ axioms := List.map (vecOfList q.1) q.2.1, unaryRules := List.map (vecOfList q.1) q.2.2.1,
            binaryRules := List.map (vecOfList q.1) q.2.2.2.1 },
          vecOfList q.1 q.2.2.2.2)⟩.fst,
    List.map List.ofFn
      ⟨q.1,
              ({ axioms := List.map (vecOfList q.1) q.2.1, unaryRules := List.map (vecOfList q.1) q.2.2.1,
                  binaryRules := List.map (vecOfList q.1) q.2.2.2.1 },
                vecOfList q.1 q.2.2.2.2)⟩.snd.1.axioms,
    List.map List.ofFn
      ⟨q.1,
              ({ axioms := List.map (vecOfList q.1) q.2.1, unaryRules := List.map (vecOfList q.1) q.2.2.1,
                  binaryRules := List.map (vecOfList q.1) q.2.2.2.1 },
                vecOfList q.1 q.2.2.2.2)⟩.snd.1.unaryRules,
    List.map List.ofFn
      ⟨q.1,
              ({ axioms := List.map (vecOfList q.1) q.2.1, unaryRules := List.map (vecOfList q.1) q.2.2.1,
                  binaryRules := List.map (vecOfList q.1) q.2.2.2.1 },
                vecOfList q.1 q.2.2.2.2)⟩.snd.1.binaryRules,
    List.ofFn
      ⟨q.1,
            ({ axioms := List.map (vecOfList q.1) q.2.1, unaryRules := List.map (vecOfList q.1) q.2.2.1,
                binaryRules := List.map (vecOfList q.1) q.2.2.2.1 },
              vecOfList q.1 q.2.2.2.2)⟩.snd.2) simp [List.map_map, Function.comp_def]All goals completed! 🐙)

The reachability problem for branching vector addition systems is decidable.

That is, the predicate taking a dimension d, a branching vector addition system b of dimension d and a target vector t ∈ ℤ^d, and returning whether t is reachable in b, is a computable predicate. Note that the dimension is part of the input: a single algorithm must work for all dimensions.

As of August 2026, the solution is quite recently announced and is not yet peer-reviewed.

@[category research solved, AMS 3 68]
theorem reachability_decidable :
    ComputablePred fun p : Σ d : ℕ, Bvas d × (Fin d → ℤ) => p.2.1.Reachable p.2.2 := by⊢ ComputablePred fun p ↦ p.snd.1.Reachable p.snd.2
  sorryAll goals completed! 🐙

Every axiom that is non-negative is reachable.

@[category test, AMS 3 68]
theorem reachable_of_mem_axioms {d : ℕ} (b : Bvas d) {v : Fin d → ℤ}
    (hmem : v ∈ b.axioms) (hcfg : 0 ≤ v) : b.Reachable v :=
  .base hmem hcfg

Reachable vectors are always non-negative.

@[category test, AMS 3 68]
theorem reachable_imp_pos {d : ℕ} (v : Fin d → ℤ) (b : Bvas d) :
    b.Reachable v → 0 ≤ v := byd:ℕv:Fin d → ℤb:Bvas d⊢ b.Reachable v → 0 ≤ v
  intro hd:ℕv:Fin d → ℤb:Bvas dh:b.Reachable v⊢ 0 ≤ v; cases hbased:ℕv:Fin d → ℤb:Bvas dhmem✝:v ∈ b.axiomshcfg✝:0 ≤ v⊢ 0 ≤ vunaryd:ℕv:Fin d → ℤb:Bvas dv✝:Fin d → ℤr✝:Fin d → ℤhv✝:b.Reachable v✝hr✝:r✝ ∈ b.unaryRuleshcfg✝:0 ≤ vhw✝:v = v✝ + r✝⊢ 0 ≤ vbinaryd:ℕv:Fin d → ℤb:Bvas dv₁✝:Fin d → ℤv₂✝:Fin d → ℤr✝:Fin d → ℤhv₁✝:b.Reachable v₁✝hv₂✝:b.Reachable v₂✝hr✝:r✝ ∈ b.binaryRuleshcfg✝:0 ≤ vhw✝:v = v₁✝ + v₂✝ + r✝⊢ 0 ≤ v; all_goals assumptionAll goals completed! 🐙

A small BVAS of dimension 3 used for a test below.

def exampleBvas : Bvas 3 := {
  axioms := [![3,1,0], ![0,0,0]],
  unaryRules := [![1,-10,-10], ![-1,0,1]],
  binaryRules := [![-1,-1,10]],
}

A small (indeed, degenerate, since it contains no binary rules) BVAS of dimension 2 used for a test below.

def exampleBvas2 : Bvas 2 := {
  axioms := [![10,0]],
  unaryRules := [![-1, 1]],
  binaryRules := [],
}

The vector [0, 0, 12] is reachable in the first example BVAS.

@[category test, AMS 3 68]
theorem reachable_example : exampleBvas.Reachable ![0,0,12] :=
  have h1 : exampleBvas.Reachable ![3,1,0] := .base
    (by⊢ ![3, 1, 0] ∈ exampleBvas.axioms decideAll goals completed! 🐙)
    (by⊢ 0 ≤ ![3, 1, 0] intro ii:Fin 3⊢ 0 i ≤ ![3, 1, 0] i; fin_cases i«0»⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩)«1»⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩)«2»⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩)«1»⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩)«2»⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨2, ⋯⟩) simpAll goals completed! 🐙)
  have h2 : exampleBvas.Reachable ![0,0,0] := .base
    (byh1:exampleBvas.Reachable ![3, 1, 0]⊢ ![0, 0, 0] ∈ exampleBvas.axioms decideAll goals completed! 🐙)
    (byh1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ≤ ![0, 0, 0] intro ih1:exampleBvas.Reachable ![3, 1, 0]i:Fin 3⊢ 0 i ≤ ![0, 0, 0] i; fin_cases i«0»h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨2, ⋯⟩) simpAll goals completed! 🐙)
  have h3 : exampleBvas.Reachable ![2,0,10] := byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ exampleBvas.Reachable ![2, 0, 10]
    refine .binary (r := ![-1, -1, 10]) h1 h2 (byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ ![-1, -1, 10] ∈ exampleBvas.binaryRules decideAll goals completed! 🐙) ?_ (byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ ![2, 0, 10] = ![3, 1, 0] + ![0, 0, 0] + ![-1, -1, 10] decideAll goals completed! 🐙)
    intro ih1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]i:Fin (Nat.succ 0).succ.succ⊢ 0 i ≤ ![2, 0, 10] i; fin_cases i«0»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨2, ⋯⟩) simpAll goals completed! 🐙
  have h4 : exampleBvas.Reachable ![1,0,11] := byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ exampleBvas.Reachable ![1, 0, 11]
    refine .unary  (r := ![-1, 0, 1]) h3 (byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ ![-1, 0, 1] ∈ exampleBvas.unaryRules decideAll goals completed! 🐙) ?_ (byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ ![1, 0, 11] = ![2, 0, 10] + ![-1, 0, 1] decideAll goals completed! 🐙)
    intro ih1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]i:Fin (Nat.succ 0).succ.succ⊢ 0 i ≤ ![1, 0, 11] i; fin_cases i«0»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨2, ⋯⟩) simpAll goals completed! 🐙
  have h5 : exampleBvas.Reachable ![0,0,12] := byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ exampleBvas.Reachable ![0, 0, 12]
    refine .unary (r := ![-1, 0, 1]) h4 (byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ ![-1, 0, 1] ∈ exampleBvas.unaryRules decideAll goals completed! 🐙) ?_ (byh1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ ![0, 0, 12] = ![1, 0, 11] + ![-1, 0, 1] decideAll goals completed! 🐙)
    intro ih1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]i:Fin (Nat.succ 0).succ.succ⊢ 0 i ≤ ![0, 0, 12] i; fin_cases i«0»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨0, ⋯⟩)«1»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨1, ⋯⟩)«2»h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨2, ⋯⟩) simpAll goals completed! 🐙
  h5

The vector [0, 0] is not reachable in the second example BVAS.


@[category test, AMS 3 68]
theorem not_reachable_example : ¬ exampleBvas2.Reachable ![0,0] := by⊢ ¬exampleBvas2.Reachable ![0, 0]
  let rec invariant (v : Fin 2 → ℤ) :
      (hv : exampleBvas2.Reachable v) → v 0 + v 1 = 10
    | .base hmem hcfg =>v:Fin 2 → ℤhmem:v ∈ exampleBvas2.axiomshcfg:0 ≤ v⊢ v 0 + v 1 = 10 byv:Fin 2 → ℤhmem:v ∈ exampleBvas2.axiomshcfg:0 ≤ v⊢ v 0 + v 1 = 10 fin_cases hmem«0»hcfg:0 ≤ ![10, 0]⊢ ![10, 0] 0 + ![10, 0] 1 = 10; simpAll goals completed! 🐙
    | .unary hv hr hcfg hw =>v:Fin 2 → ℤv✝:Fin 2 → ℤr✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hr:r✝ ∈ exampleBvas2.unaryRuleshcfg:0 ≤ vhw:v = v✝ + r✝⊢ v 0 + v 1 = 10 byv:Fin 2 → ℤv✝:Fin 2 → ℤr✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hr:r✝ ∈ exampleBvas2.unaryRuleshcfg:0 ≤ vhw:v = v✝ + r✝⊢ v 0 + v 1 = 10
        fin_cases hr«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ v 0 + v 1 = 10;
        ·«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ v 0 + v 1 = 10 rw [hw«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ (v✝ + ![-1, 1]) 0 + (v✝ + ![-1, 1]) 1 = 10«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ (v✝ + ![-1, 1]) 0 + (v✝ + ![-1, 1]) 1 = 10]«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ (v✝ + ![-1, 1]) 0 + (v✝ + ![-1, 1]) 1 = 10
          simp only [Pi.add_apply, Matrix.cons_val_zero, Matrix.cons_val_one]«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ v✝ 0 + -1 + (v✝ 1 + 1) = 10
          ring_nf«0»v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ v✝ 0 + v✝ 1 = 10
          exact invariant _ hvAll goals completed! 🐙
    | .binary _ _ hr _ _ =>v:Fin 2 → ℤv₁✝:Fin 2 → ℤv₂✝:Fin 2 → ℤr✝:Fin 2 → ℤhv₁✝:exampleBvas2.Reachable v₁✝hv₂✝:exampleBvas2.Reachable v₂✝hr:r✝ ∈ exampleBvas2.binaryRuleshcfg✝:0 ≤ vhw✝:v = v₁✝ + v₂✝ + r✝⊢ v 0 + v 1 = 10 byv:Fin 2 → ℤv₁✝:Fin 2 → ℤv₂✝:Fin 2 → ℤr✝:Fin 2 → ℤhv₁✝:exampleBvas2.Reachable v₁✝hv₂✝:exampleBvas2.Reachable v₂✝hr:r✝ ∈ exampleBvas2.binaryRuleshcfg✝:0 ≤ vhw✝:v = v₁✝ + v₂✝ + r✝⊢ v 0 + v 1 = 10 fin_cases hrAll goals completed! 🐙
  intro hh:exampleBvas2.Reachable ![0, 0]⊢ False
  simpa using invariant _ hAll goals completed! 🐙

end BranchingVAS