let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
let X be V5() ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: T height<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
set I = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } ;
set J = { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } ;
thus T height<= 0 c= { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } :: according to XBOOLE_0:def 10 :: thesis: { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } c= T height<= 0
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in T height<= 0 or a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } )
assume a in T height<= 0 ; :: thesis: a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
then consider t being Element of (Free (S,X)) such that
A1: ( a = t & t in T & height t <= 0 ) ;
per cases ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ) by Th16;
suppose ex s being SortSymbol of S ex x being Element of X . s st t = x -term ; :: thesis: a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
then t in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } ;
hence a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by A1, XBOOLE_0:def 3; :: thesis: verum
end;
suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ; :: thesis: a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A2: t = o -term p ;
reconsider n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } as Nat by Th25;
per cases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
suppose the_arity_of o = {} ; :: thesis: a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
then t in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by A1, A2;
hence a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by A1, XBOOLE_0:def 3; :: thesis: verum
end;
suppose the_arity_of o <> {} ; :: thesis: a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }
then height t = n + 1 by A2, Th26;
hence a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by A1; :: thesis: verum
end;
end;
end;
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } or a in T height<= 0 )
assume a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } ; :: thesis: a in T height<= 0
per cases then ( a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } or a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } ) by XBOOLE_0:def 3;
suppose a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } ; :: thesis: a in T height<= 0
then consider s being SortSymbol of S, x being Element of X . s such that
A3: a = x -term ;
( height (x -term) = 0 & x -term in T ) by Th24, TREES_1:42;
hence a in T height<= 0 by A3; :: thesis: verum
end;
suppose a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } ; :: thesis: a in T height<= 0
then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A4: ( a = o -term p & o -term p in T & the_arity_of o = {} ) ;
height (o -term p) = 0 by A4, Th20;
hence a in T height<= 0 by A4; :: thesis: verum
end;
end;