let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; :: thesis: for t being type of T
for a being adjective of T st a is_properly_applicable_to t holds
radix (a ast t) = radix t
let t be type of T; :: thesis: for a being adjective of T st a is_properly_applicable_to t holds
radix (a ast t) = radix t
let a be adjective of T; :: thesis: ( a is_properly_applicable_to t implies radix (a ast t) = radix t )
A1: ( a in adjs t or not a in adjs t ) ;
assume a is_properly_applicable_to t ; :: thesis: radix (a ast t) = radix t
then ( a ast t = t or [(a ast t),t] in T @--> ) by A1, Def31, Th24;
then T @--> reduces a ast t,t by REWRITE1:12, REWRITE1:15;
then A2: a ast t,t are_convertible_wrt T @--> by REWRITE1:25;
T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
hence radix (a ast t) = radix t by A2, REWRITE1:55; :: thesis: verum