let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let X be V5() ManySortedSet of the carrier of S; for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let x be Element of X . s; for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let t be Element of (Free (S,X)); for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let C be context of x; ( X is non-trivial implies for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t) )
assume ZZ:
X is non-trivial
; for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let xi be Element of dom C; ( C . xi = [x,s] & the_sort_of t = s implies C -sub t = C with-replacement (xi,t) )
assume Z0:
C . xi = [x,s]
; ( not the_sort_of t = s or C -sub t = C with-replacement (xi,t) )
assume Z1:
the_sort_of t = s
; C -sub t = C with-replacement (xi,t)
defpred S1[ Element of (Free (S,X))] means for C being context of x st C = $1 holds
for xi being Element of dom C st C . xi = [x,s] holds
C -sub t = C with-replacement (xi,t);
A1:
S1[x -term ]
proof
let C be
context of
x;
( C = x -term implies for xi being Element of dom C st C . xi = [x,s] holds
C -sub t = C with-replacement (xi,t) )
assume A2:
C = x -term
;
for xi being Element of dom C st C . xi = [x,s] holds
C -sub t = C with-replacement (xi,t)
let xi be
Element of
dom C;
( C . xi = [x,s] implies C -sub t = C with-replacement (xi,t) )
xi in {{}}
by A2, TREES_1:29;
then
xi = <*> NAT
;
hence
(
C . xi = [x,s] implies
C -sub t = C with-replacement (
xi,
t) )
by Z1, A2, Th41;
verum
end;
A3:
for o being OperSymbol of S
for w being Element of Args (o,(Free (S,X))) st w is x -context_including & S1[x -context_in w] holds
for C being context of x st C = o -term w holds
S1[C]
proof
let o be
OperSymbol of
S;
for w being Element of Args (o,(Free (S,X))) st w is x -context_including & S1[x -context_in w] holds
for C being context of x st C = o -term w holds
S1[C]let w be
Element of
Args (
o,
(Free (S,X)));
( w is x -context_including & S1[x -context_in w] implies for C being context of x st C = o -term w holds
S1[C] )
assume Z2:
w is
x -context_including
;
( not S1[x -context_in w] or for C being context of x st C = o -term w holds
S1[C] )
assume Z3:
S1[
x -context_in w]
;
for C being context of x st C = o -term w holds
S1[C]
let C be
context of
x;
( C = o -term w implies S1[C] )
assume Z4:
C = o -term w
;
S1[C]
let D be
context of
x;
( D = C implies for xi being Element of dom D st D . xi = [x,s] holds
D -sub t = D with-replacement (xi,t) )
assume Z5:
D = C
;
for xi being Element of dom D st D . xi = [x,s] holds
D -sub t = D with-replacement (xi,t)
let xi be
Element of
dom D;
( D . xi = [x,s] implies D -sub t = D with-replacement (xi,t) )
assume Z6:
D . xi = [x,s]
;
D -sub t = D with-replacement (xi,t)
dom D = tree (doms w)
by Z4, Z5, TREES_4:10;
per cases then
( xi = {} or ex i being Nat ex r being FinSequence st
( i < len (doms w) & r in (doms w) . (i + 1) & xi = <*i*> ^ r ) )
by TREES_3:def 15;
suppose
ex
i being
Nat ex
r being
FinSequence st
(
i < len (doms w) &
r in (doms w) . (i + 1) &
xi = <*i*> ^ r )
;
D -sub t = D with-replacement (xi,t)then consider i being
Nat,
r being
FinSequence such that A4:
(
i < len (doms w) &
r in (doms w) . (i + 1) &
xi = <*i*> ^ r )
;
A5:
len (doms w) = len w
by TREES_3:38;
then AB:
( 1
<= i + 1 &
i + 1
<= len w )
by A4, NAT_1:12, NAT_1:13;
then A6:
i + 1
in dom w
by FINSEQ_3:25;
then A7:
(
w /. (i + 1) = w . (i + 1) &
w . (i + 1) in rng w &
(doms w) . (i + 1) = dom (w . (i + 1)) )
by PARTFUN1:def 6, FUNCT_6:def 2, FUNCT_1:def 3;
then reconsider r =
r as
Element of
dom (w /. (i + 1)) by A4;
A8:
(
D . xi = (w /. (i + 1)) . r &
[x,s] in {[x,s]} )
by Z4, Z5, A4, A5, A7, TARSKI:def 1, TREES_4:12;
then
not
w /. (i + 1) is
x -omitting
by Z6, FUNCT_1:def 7;
then AA:
x -context_pos_in w = i + 1
by Z2, AB, Th72, FINSEQ_3:25;
then A9:
x -context_in w = w /. (i + 1)
by Z2, A7, Th71;
the_sort_of (x -context_in w) = (the_arity_of o) /. (x -context_pos_in w)
by A6, AA, A9, Th4A;
then reconsider u =
w +* (
(x -context_pos_in w),
((x -context_in w) -sub t)) as
Element of
Args (
o,
(Free (S,X)))
by MSUALG_6:7;
A11:
D -sub t = o -term u
by ZZ, Z1, Z2, Z4, Z5, Th43;
xi in dom D
;
then
(
i < len w &
xi in tree (doms w) &
x -context_in w = w . (i + 1) &
u = w +* (
(i + 1),
((x -context_in w) with-replacement (r,t))) )
by Z4, Z5, A4, AA, A9, Z3, Z6, A8, A6, TREES_3:38, TREES_4:10, PARTFUN1:def 6;
hence
D -sub t = D with-replacement (
xi,
t)
by A11, Z4, Z5, A4, Th123;
verum end;
end;
S1[C]
from MSAFREE5:sch 4(A1, A3);
hence
C -sub t = C with-replacement (xi,t)
by Z0; verum