fact: Fixpoint depth_q (xi:Tensor) (alpha beta:Reals) (H1:emits_q xi alpha beta) {struct H1}:nat:= match Incl_T_dec_D xi LL with | left _ => 0 | right H_emission_L => match Incl_T_dec_D xi RR with | left _ => 0 | right H_emission_R => match Incl_T_dec_D xi MM with | left _ => 0 | right H_emission_M => S(depth_q (right_product (left_product xi (Streams.hd alpha)) (Streams.hd beta)) (Streams.tl alpha) (Streams.tl beta) (emits_q_absorbs_inv xi alpha beta H_emission_L H_emission_R H_emission_M H1)) end end end.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)