let S be locally_directed OrderSortedSign; :: thesis: for X being V2() ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence of TS (DTConOSA X) holds
( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )
let X be V2() ManySortedSet of S; :: thesis: for o being OperSymbol of S
for x being FinSequence of TS (DTConOSA X) holds
( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )
let o be OperSymbol of S; :: thesis: for x being FinSequence of TS (DTConOSA X) holds
( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )
let x be FinSequence of TS (DTConOSA X); :: thesis: ( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
set w = the_arity_of o;
set LSx = LeastSorts x;
reconsider SPTA = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of S ;
A1: dom (LeastSorts x) = dom x by Def13;
hereby :: thesis: ( x in Args (o,(ParsedTermsOSA X)) implies LeastSorts x <= the_arity_of o )
assume A2: LeastSorts x <= the_arity_of o ; :: thesis: x in Args (o,(ParsedTermsOSA X))
then A3: len (LeastSorts x) = len (the_arity_of o) ;
then A4: dom (LeastSorts x) = dom (the_arity_of o) by FINSEQ_3:29;
A5: for k being Nat st k in dom x holds
x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k)
proof
let k be Nat; :: thesis: ( k in dom x implies x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k) )
assume A6: k in dom x ; :: thesis: x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k)
consider t2 being Element of TS (DTConOSA X) such that
A7: t2 = x . k and
A8: (LeastSorts x) . k = LeastSort t2 by A6, Def13;
reconsider wk = (the_arity_of o) /. k as Element of S ;
(the_arity_of o) /. k = (the_arity_of o) . k by A1, A4, A6, PARTFUN1:def 6;
then LeastSort t2 <= wk by A1, A2, A6, A8;
then A9: SPTA . (LeastSort t2) c= SPTA . wk by OSALG_1:def 16;
t2 in the Sorts of (ParsedTermsOSA X) . (LeastSort t2) by Def12;
hence x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k) by A7, A9; :: thesis: verum
end;
len x = len (the_arity_of o) by A1, A3, FINSEQ_3:29;
hence x in Args (o,(ParsedTermsOSA X)) by A5, MSAFREE2:5; :: thesis: verum
end;
assume A10: x in Args (o,(ParsedTermsOSA X)) ; :: thesis: LeastSorts x <= the_arity_of o
then A11: dom x = dom (the_arity_of o) by MSUALG_6:2;
hence len (LeastSorts x) = len (the_arity_of o) by A1, FINSEQ_3:29; :: according to OSALG_1:def 6 :: thesis: for b1 being set holds
( not b1 in dom (LeastSorts x) or for b2, b3 being Element of the carrier of S holds
( not b2 = (LeastSorts x) . b1 or not b3 = (the_arity_of o) . b1 or b2 <= b3 ) )
let i be set ; :: thesis: ( not i in dom (LeastSorts x) or for b1, b2 being Element of the carrier of S holds
( not b1 = (LeastSorts x) . i or not b2 = (the_arity_of o) . i or b1 <= b2 ) )
assume A12: i in dom (LeastSorts x) ; :: thesis: for b1, b2 being Element of the carrier of S holds
( not b1 = (LeastSorts x) . i or not b2 = (the_arity_of o) . i or b1 <= b2 )
reconsider k = i as Nat by A12;
i in dom (the_arity_of o) by A11, A12, Def13;
then A13: x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k) by A10, MSUALG_6:2;
i in dom x by A12, Def13;
then A14: ex t2 being Element of TS (DTConOSA X) st
( t2 = x . k & (LeastSorts x) . k = LeastSort t2 ) by Def13;
let s1, s2 be Element of S; :: thesis: ( not s1 = (LeastSorts x) . i or not s2 = (the_arity_of o) . i or s1 <= s2 )
assume that
A15: s1 = (LeastSorts x) . i and
A16: s2 = (the_arity_of o) . i ; :: thesis: s1 <= s2
(the_arity_of o) /. k = (the_arity_of o) . k by A1, A11, A12, PARTFUN1:def 6;
hence s1 <= s2 by A15, A16, A14, A13, Def12; :: thesis: verum