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