let nt be NonTerminal of SCM-AE; 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; 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; verum