proposition: Lemma step_productive_q_S_inv_2: forall n (xi:Tensor) (alpha beta:Reals) (h:emits_q xi alpha beta), step_productive_q (S n) xi alpha beta -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h)))).
proof: Proof. exact ( fun (n : nat) (xi : Tensor) (alpha beta : Reals) (h : emits_q xi alpha beta) (H : step_productive_q (S n) xi alpha beta) => let H0 := match H in (step_productive_q n0 t r r0) return (n0 = S n -> t = xi -> r = alpha -> r0 = beta -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h))))) with | step_productive_q_O xi0 alpha0 beta0 H0 => fun (H1 : 0 = S n) (H2 : xi0 = xi) (H3 : alpha0 = alpha) (H4 : beta0 = beta) => let H := (let H0 := eq_ind 0 (fun e : nat => match e with | O => True | S _ => False end) I (S n) H1 in False_ind (xi0 = xi -> alpha0 = alpha -> beta0 = beta -> emits_q xi0 alpha0 beta0 -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h))))) H0) H2 H3 H4 in H H0 | step_productive_q_S n0 xi0 alpha0 beta0 h0 H0 => fun (H1 : S n0 = S n) (H2 : xi0 = xi) (H3 : alpha0 = alpha) (H4 : beta0 = beta) => let H := (let H0 := f_equal (fun e : nat => match e with | O => n0 | S n => n end) H1 in eq_ind n (fun n0 : nat => xi0 = xi -> alpha0 = alpha -> beta0 = beta -> step_productive_q n0 (fstT (sndT (modulus_q xi0 alpha0 beta0 h0))) (fstT (sndT (sndT (modulus_q xi0 alpha0 beta0 h0)))) (sndT (sndT (sndT (modulus_q xi0 alpha0 beta0 h0)))) -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h))))) (fun H2 : xi0 = xi => let H := eq_ind xi (fun t : Tensor => forall h0 : emits_q t alpha0 beta0, alpha0 = alpha -> beta0 = beta -> step_productive_q n (fstT (sndT (modulus_q t alpha0 beta0 h0))) (fstT (sndT (sndT (modulus_q t alpha0 beta0 h0)))) (sndT (sndT (sndT (modulus_q t alpha0 beta0 h0)))) -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h))))) (fun (h0 : emits_q xi alpha0 beta0) (H3 : alpha0 = alpha) (H4 : beta0 = beta) (H1 : step_productive_q n (fstT (sndT (modulus_q xi alpha0 beta0 h0))) (fstT (sndT (sndT (modulus_q xi alpha0 beta0 h0)))) (sndT (sndT (sndT (modulus_q xi alpha0 beta0 h0))))) => (let H := eq_ind_r (fun beta0 : Reals => forall h0 : emits_q xi alpha0 beta0, step_productive_q n (fstT (sndT (modulus_q xi alpha0 beta0 h0))) (fstT (sndT (sndT (modulus_q xi alpha0 beta0 h0)))) (sndT (sndT (sndT (modulus_q xi alpha0 beta0 h0)))) -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h))))) (fun h0 : emits_q xi alpha0 beta => let H := eq_ind_r (fun alpha0 : Reals => forall h0 : emits_q xi alpha0 beta, step_productive_q n (fstT (sndT (modulus_q xi alpha0 beta h0))) (fstT (sndT (sndT (modulus_q xi alpha0 beta h0)))) (sndT (sndT (sndT (modulus_q xi alpha0 beta h0)))) -> step_productive_q n (fstT (sndT (modulus_q xi alpha beta h))) (fstT (sndT (sndT (modulus_q xi alpha beta h)))) (sndT (sndT (sndT (modulus_q xi alpha beta h))))) (fun h0 : emits_q xi alpha beta => eq_ind_r (fun p : prodT Digit (prodT Tensor (prodT Reals Reals)) => step_productive_q n (fstT (sndT (modulus_q xi alpha beta h0))) (fstT (sndT (sndT (modulus_q xi alpha beta h0)))) (sndT (sndT (sndT (modulus_q xi alpha beta h0)))) -> step_productive_q n (fstT (sndT p)) (fstT (sndT (sndT p))) (sndT (sndT (sndT p)))) (fun H1 : step_productive_q n (fstT (sndT (modulus_q xi alpha beta h0))) (fstT (sndT (sndT (modulus_q xi alpha beta h0)))) (sndT (sndT (sndT (modulus_q xi alpha beta h0)))) => H1) (modulus_q_PI xi alpha beta h h0)) H3 in H h0) H4 in H h0) H1) xi0 (sym_eq H2) in H h0) n0 (sym_eq H0)) H2 H3 H4 in H H0 end in H0 (refl_equal (S n)) (refl_equal xi) (refl_equal alpha) (refl_equal beta) ). Defined.
imports: digits