Proof step 1 from proof valid-group-nodes-entire (conclusion)

User applied rule induction

And obtained the following new goals

• Proof step 2:

  φ([]) ∧ (∀ gndx, gnd. φ(gndx) → φ(gndx + gnd)) ⊦ φ(gndx)

Rule argument

Additional information

Used simplifier rules: valid-group-nodes-base: ⊦ valid-group-nodes([]) = 0;%valid-group-nodes-rec: ⊦ valid-group-nodes(gndx + gnd ') = (gnd.end ⊃ # gndx + 1;valid-group-nodes(gndx));%valid-group-nodes-ls: ⊦ n < valid-group-nodes(gndx) → n < # gndx;% ⊦ # [] = 0; (s)% ⊦ gndx + gnd = gndx + gnd '; (s)% ⊦ #(gndx + gndx0) = # gndx + # gndx0; (s)% ⊦ # gnd ' = 0 +1; (s)%a: ⊦ (gndx + gndx0) + gndx1 = gndx + gndx0 + gndx1; from specification list[group-store]% ⊦ m + 1 ≤ n ↔ m < n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%in-15: ⊦ gndx + gnd ' = gndx0 → gnd ∈ gndx0; (forward) from specification list[group-store]% ⊦ m + n = m + n0 ↔ n = n0; (s)% ⊦ m < n → m ≤ n; (s)% ⊦ gnd ∈ gndx + gndx0 ↔ gnd ∈ gndx ∨ gnd ∈ gndx0; (s)% ⊦ gnd ∈ gnd0 ' ↔ gnd = gnd0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ m < n → n ≠ 0; (s)% ⊦ ¬ n < n; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ # gndx = 0 ↔ gndx = []; (s)% ⊦ ¬ m + n < m; (s)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat% ⊦ m = m + n ↔ n = 0; (s) Used terms: λ gndx0. ∀ gndx. gndx0 = gndx → ( # gndx ≤ valid-group-nodes(gndx) ↔ valid-group-nodes(gndx) = # gndx), gndx