fact: Definition phi_rec_psi f a b c := if (c==zero) then if(b==zero) then if(a==zero) then phi0 else if(T3is_succ a) then phi4 (T3pred a) else phi5 (f a) else if(T3is_succ b) then phi6 a (T3pred b) else phi7 a b (f b) else if(T3is_succ c) then if(b==zero) then if(a==zero) then phi3 [zero,zero, T3pred c] else if (T3is_succ a) then phi8 (T3pred a) (T3pred c) else phi9 a (T3pred c) (f a) else if(T3is_succ b) then phi10 a (T3pred b) (T3pred c) else phi11 a b (T3pred c) (f b) else if (limit12_hyp a b c) then if(b==zero) then if(a==zero) then phi3 c else if(T3is_succ a) then phi12b2 (T3pred a) c else phi12b3 c (f a) else if (T3is_succ b) then phi12b4 a (T3pred b) c else phi12b5 a c (f b) else phi12a a b (f c).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)