proposition: Lemma ra_ca_inv k (f : recalg k) v n x : [f;v] -[n>> x -> (n = 1 /\ exists (H : k = 0), eq_rect _ _ f _ H = ra_cst x) \/ (n = 1 /\ x = 0 /\ exists (H : k = 1), eq_rect _ _ f _ H = ra_zero) \/ (n = 1 /\ exists (H : k = 1), x = S (vec_head (eq_rect _ _ v _ H)) /\ eq_rect _ _ f _ H = ra_succ) \/ (n = 1 /\ exists p, x = vec_pos v p /\ f = ra_proj p) \/ (exists i (h : recalg i) gj w q m, n = 1+q+vec_sum m /\ [h;w] -[q>> x /\ (forall p, [vec_pos gj p;v] -[vec_pos m p>> vec_pos w p) /\ f = ra_comp h gj) \/ (exists k' (H : k = S k') (h : recalg k') g m, n = S m /\ vec_head (eq_rect _ _ v _ H) = 0 /\ [h;vec_tail (eq_rect _ _ v _ H)] -[m>> x /\ eq_rect _ _ f _ H = ra_rec h g) \/ (exists k' (H : k = S k') m y (h : recalg k') g p q, vec_head (eq_rect _ _ v _ H) = S m /\ n = 1+p+q /\ [ra_rec h g; m##vec_tail (eq_rect _ _ v _ H)] -[p>> y /\ [g; m##y##vec_tail (eq_rect _ _ v _ H)] -[q>> x /\ eq_rect _ _ f _ H = ra_rec h g) \/ (exists (g : recalg (S k)) (m w : vec _ x) q, n = 1+q+vec_sum m /\ (forall p, [g; pos2nat p##v] -[vec_pos m p>> S (vec_pos w p)) /\ [g; x##v] -[q>> 0 /\ f = ra_min g) .
proof: Proof. induction 1 as [ | | | k v j | k i f gj v q w p x | k f g v n x | k f g v n p x q y | k f v x p w q ]. do 0 right; left; split; auto; exists eq_refl; auto. do 1 right; left; do 2 (split; auto); exists eq_refl; auto. do 2 right; left; split; auto; exists eq_refl; split; simpl; auto. do 3 right; left; split; auto; exists j; auto. do 4 right; left; exists k, f, gj, w, p, q; auto. do 5 right; left; exists k, eq_refl, f, g, n; auto. do 6 right; left; exists k, eq_refl, n, x, f, g, p, q; auto. do 7 right; exists f, q, w, p; auto. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)