let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for o being OperSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let s be SortSymbol of S; for o being OperSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let o be OperSymbol of S; for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let Z be non-trivial ManySortedSet of the carrier of S; for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let z be Element of Z . s; for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let C9 be context of z; for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let w, p be Element of Args (o,(Free (S,Z))); for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p
let t be Element of (Free (S,Z)); ( w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s implies C9 -sub t = o -term p )
assume that
A1:
w is z -context_including
and
A2:
C9 = o -term w
and
A3:
p = w +* ((z -context_pos_in w),((z -context_in w) -sub t))
and
A4:
the_sort_of t = s
; C9 -sub t = o -term p
A5:
( dom p = dom (the_arity_of o) & dom (the_arity_of o) = dom w & dom w <> {} )
by A1, MSUALG_3:6;
then reconsider v = w, q = p as non empty DTree-yielding FinSequence ;
now for i being Nat
for d1 being DecoratedTree st i in dom v & d1 = v . i holds
q . i = (d1,[z,s]) <- tlet i be
Nat;
for d1 being DecoratedTree st i in dom v & d1 = v . i holds
q . b2 = (b3,[z,s]) <- tlet d1 be
DecoratedTree;
( i in dom v & d1 = v . i implies q . b1 = (b2,[z,s]) <- t )assume A6:
(
i in dom v &
d1 = v . i )
;
q . b1 = (b2,[z,s]) <- tA7:
(z -context_in w) -sub t = (
(z -context_in w),
[z,s])
<- t
by A4, SUB;
per cases
( i = z -context_pos_in w or i <> z -context_pos_in w )
;
suppose A8:
i <> z -context_pos_in w
;
q . b1 = (b2,[z,s]) <- tthen
(
w /. i is
z -omitting &
w /. i = d1 )
by A1, A6, Th72, PARTFUN1:def 6;
then
(
d1,
[z,s])
<- t = d1
by Th23;
hence
q . i = (
d1,
[z,s])
<- t
by A3, A6, A8, FUNCT_7:32;
verum end; end; end;
then
(([o, the carrier of S] -tree v),[z,s]) <- t = [o, the carrier of S] -tree q
by A5, ThL8;
hence
C9 -sub t = o -term p
by A2, A4, SUB; verum