let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
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 V5() ManySortedSet of ; :: 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;
A1:
( dom (LeastSorts x) = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & (LeastSorts x) . y = LeastSort t ) ) )
by Def14;
reconsider SPTA = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of ;
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
(
len (LeastSorts x) = len (the_arity_of o) & ( for
i being
set st
i in dom (LeastSorts x) holds
for
s1,
s2 being
Element of
S st
s1 = (LeastSorts x) . i &
s2 = (the_arity_of o) . i holds
s1 <= s2 ) )
by OSALG_1:def 7;
then A3:
(
dom (LeastSorts x) = dom (the_arity_of o) &
len x = len (the_arity_of o) )
by A1, FINSEQ_3:31;
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 A4:
k in dom x
;
:: thesis: x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k)
A5:
(the_arity_of o) /. k = (the_arity_of o) . k
by A1, A3, A4, PARTFUN1:def 8;
reconsider wk =
(the_arity_of o) /. k as
Element of
S ;
consider t2 being
Element of
TS (DTConOSA X) such that A6:
(
t2 = x . k &
(LeastSorts x) . k = LeastSort t2 )
by A4, Def14;
A7:
t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2)
by Def12;
LeastSort t2 <= wk
by A1, A2, A4, A5, A6, OSALG_1:def 7;
then
SPTA . (LeastSort t2) c= SPTA . wk
by OSALG_1:def 18;
hence
x . k in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. k)
by A6, A7;
:: thesis: verum
end; hence
x in Args o,
(ParsedTermsOSA X)
by A3, MSAFREE2:7;
:: thesis: verum
end;
assume A8:
x in Args o,(ParsedTermsOSA X)
; :: thesis: LeastSorts x <= the_arity_of o
then A9:
( dom x = dom (the_arity_of o) & ( for i being Nat st i in dom (the_arity_of o) holds
x . i in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. i) ) )
by MSUALG_6:2;
hence
len (LeastSorts x) = len (the_arity_of o)
by A1, FINSEQ_3:31; :: according to OSALG_1:def 7 :: 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 A10:
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 )
A11:
( i in dom (the_arity_of o) & i in dom x )
by A9, A10, Def14;
reconsider k = i as Nat by A10;
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 A12:
( s1 = (LeastSorts x) . i & s2 = (the_arity_of o) . i )
; :: thesis: s1 <= s2
consider t2 being Element of TS (DTConOSA X) such that
A13:
( t2 = x . k & (LeastSorts x) . k = LeastSort t2 )
by A11, Def14;
A14:
(the_arity_of o) /. k = (the_arity_of o) . k
by A1, A9, A10, PARTFUN1:def 8;
x . k in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. k)
by A8, A11, MSUALG_6:2;
hence
s1 <= s2
by A12, A13, A14, Def12; :: thesis: verum