let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being bin-term holds max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))
let tl, tr be bin-term; :: thesis: max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))
A1: ( max_Data-Loc_in tl = f . tl & max_Data-Loc_in tr = f . tr ) by Def14, Lm4, Lm5;
( nt ==> <*(root-label tl),(root-label tr)*> & max_Data-Loc_in (nt -tree (tl,tr)) = f . (nt -tree (tl,tr)) ) by Def1, Def14, Lm4, Lm5, Lm6;
hence max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A1, Lm5; :: thesis: verum