Theorem: LoopProgram.ofLen_contains_extendLenOne_image
Proof state before:
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈ ofLen (n + 1)
Tactic:
apply Finset.mem_union_left
Proof state after:
case h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈
    Finset.fold (fun a b => a ∪ b) ∅ extendLenOne
        ((fun y a =>
            Acc.rec
              (fun x₁ h ih =>
                (fun a a_1 =>
                    (match (motive :=
                        (x : ℕ) →
                          ((y : ℕ) →
                              (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                            Finset LoopProgram)
                        a with
                      | 0 => fun x => ∅
                      | Nat.succ n => fun x =>
                        Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                            Finset.fold (fun x x_1 => x ∪ x_1) ∅
                              (fun x_1 =>
                                match x_1 with
                                | { val := l, property := h } =>
                                  let_fun this := ⋯;
                                  Finset.image
                                    (fun x =>
                                      match x with
                                      | (a, b) => concat a b)
                                    (Finset.product (x l ⋯) (x (n - l) ⋯)))
                              (Finset.attach (Finset.range n)) ∪
                          baseProgram (n + 1))
                      a_1)
                  x₁ ih)
              ⋯)
          (Nat.add n 0) ⋯) ∪
      Finset.fold (fun x x_1 => x ∪ x_1) ∅
        (fun x =>
          match x with
          | { val := l, property := h } =>
            let_fun this := ⋯;
            Finset.image
              (fun x =>
                match x with
                | (a, b) => concat a b)
              (Finset.product
                ((fun y a =>
                    Acc.rec
                      (fun x₁ h ih =>
                        (fun a a_1 =>
                            (match (motive :=
                                (x : ℕ) →
                                  ((y : ℕ) →
                                      (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x →
                                        Finset LoopProgram) →
                                    Finset LoopProgram)
                                a with
                              | 0 => fun x => ∅
                              | Nat.succ n => fun x =>
                                Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                                    Finset.fold (fun x x_1 => x ∪ x_1) ∅
                                      (fun x_1 =>
                                        match x_1 with
                                        | { val := l, property := h } =>
                                          let_fun this := ⋯;
                                          Finset.image
                                            (fun x =>
                                              match x with
                                              | (a, b) => concat a b)
                                            (Finset.product (x l ⋯) (x (n - l) ⋯)))
                                      (Finset.attach (Finset.range n)) ∪
                                  baseProgram (n + 1))
                              a_1)
                          x₁ ih)
                      ⋯)
                  l ⋯)
                ((fun y a =>
                    Acc.rec
                      (fun x₁ h ih =>
                        (fun a a_1 =>
                            (match (motive :=
                                (x : ℕ) →
                                  ((y : ℕ) →
                                      (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x →
                                        Finset LoopProgram) →
                                    Finset LoopProgram)
                                a with
                              | 0 => fun x => ∅
                              | Nat.succ n => fun x =>
                                Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                                    Finset.fold (fun x x_1 => x ∪ x_1) ∅
                                      (fun x_1 =>
                                        match x_1 with
                                        | { val := l, property := h } =>
                                          let_fun this := ⋯;
                                          Finset.image
                                            (fun x =>
                                              match x with
                                              | (a, b) => concat a b)
                                            (Finset.product (x l ⋯) (x (n - l) ⋯)))
                                      (Finset.attach (Finset.range n)) ∪
                                  baseProgram (n + 1))
                              a_1)
                          x₁ ih)
                      ⋯)
                  (Nat.add n 0 - l) ⋯)))
        (Finset.attach (Finset.range (Nat.add n 0)))