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 Def13, Lm6, Lm7;
( nt ==> <*(root-label tl),(root-label tr)*> & max_Data-Loc_in (nt -tree tl,tr) = f . (nt -tree tl,tr) ) by Def1, Def13, Lm6, Lm7, Lm8;
hence max_Data-Loc_in (nt -tree tl,tr) = max (max_Data-Loc_in tl),(max_Data-Loc_in tr) by A1, Lm7; :: thesis: verum