let S be non empty non void ManySortedSign ; for Y being infinite-yielding ManySortedSet of the carrier of S
for v being Element of (Free (S,Y))
for h being Endomorphism of Free (S,Y)
for f being vf-sequence of v st f <> {} holds
ex B being non empty FinSequence of the carrier of S ex V1 being b5 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b5 -sorts FinSequence of (Free (S,Y)) ex V2 being b5 -sorts b6 -omitting b7 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b8 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
let Y be infinite-yielding ManySortedSet of the carrier of S; for v being Element of (Free (S,Y))
for h being Endomorphism of Free (S,Y)
for f being vf-sequence of v st f <> {} holds
ex B being non empty FinSequence of the carrier of S ex V1 being b4 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b4 -sorts FinSequence of (Free (S,Y)) ex V2 being b4 -sorts b5 -omitting b6 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b7 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
let v be Element of (Free (S,Y)); for h being Endomorphism of Free (S,Y)
for f being vf-sequence of v st f <> {} holds
ex B being non empty FinSequence of the carrier of S ex V1 being b3 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b3 -sorts FinSequence of (Free (S,Y)) ex V2 being b3 -sorts b4 -omitting b5 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b6 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
let h be Endomorphism of Free (S,Y); for f being vf-sequence of v st f <> {} holds
ex B being non empty FinSequence of the carrier of S ex V1 being b2 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b2 -sorts FinSequence of (Free (S,Y)) ex V2 being b2 -sorts b3 -omitting b4 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b5 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
let f be vf-sequence of v; ( f <> {} implies ex B being non empty FinSequence of the carrier of S ex V1 being b1 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b1 -sorts FinSequence of (Free (S,Y)) ex V2 being b1 -sorts b2 -omitting b3 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b4 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) ) )
assume A0:
f <> {}
; ex B being non empty FinSequence of the carrier of S ex V1 being b1 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b1 -sorts FinSequence of (Free (S,Y)) ex V2 being b1 -sorts b2 -omitting b3 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b4 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
then
( {} <> dom f & dom f = dom (pr2 f) )
by MCART_1:def 13;
then reconsider B = pr2 f as non empty FinSequence of the carrier of S by Th96;
consider g being one-to-one FinSequence such that
AA:
( rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom f = dom g & ( for i being Nat st i in dom f holds
f . i = v . (g . i) ) )
by VFS;
rng g c= dom v
then reconsider g = g as one-to-one FinSequence of dom v by FINSEQ_1:def 4;
take
B
; ex V1 being B -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being B -sorts FinSequence of (Free (S,Y)) ex V2 being B -sorts b1 -omitting b2 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b3 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
B = pr2 f
;
then reconsider V1 = pr1 f as B -sorts FinSequence of Union Y by Th97;
take
V1
; ( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being B -sorts FinSequence of (Free (S,Y)) ex V2 being B -sorts V1 -omitting b1 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b2 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )
thus AB:
( dom B = dom f & B = pr2 f & V1 = pr1 f )
by MCART_1:def 13; ex D being B -sorts FinSequence of (Free (S,Y)) ex V2 being B -sorts V1 -omitting b1 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b2 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) )
deffunc H1( Element of dom B) -> Element of (Free (S,Y)) = h . ((V1 . $1) -term);
consider D being non empty FinSequence such that
A2:
( dom D = dom B & ( for i being Element of dom B holds D . i = H1(i) ) )
from MSAFREE5:sch 6();
D is FinSequence of (Free (S,Y))
then reconsider D = D as FinSequence of (Free (S,Y)) ;
D is B -sorts
then reconsider D = D as B -sorts FinSequence of (Free (S,Y)) ;
take
D
; ex V2 being B -sorts V1 -omitting D -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b1 -context-sequence FinSequence of (Free (S,Y)) st
( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) )
set V2 = the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y;
take
the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y
; ( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y -context-sequence FinSequence of (Free (S,Y)) st
( F is V1, the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) )
thus
for i being Element of dom B holds D . i = h . ((V1 . i) -term)
by A2; ex F being the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y -context-sequence FinSequence of (Free (S,Y)) st
( F is V1, the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) )
deffunc H2( Element of dom B, DecoratedTree) -> set = ($2 with-replacement ((g /. $1),(D . $1))) with-replacement ((g /. ($1 + 1)),(root-tree [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . ($1 + 1)),(B . ($1 + 1))]));
consider F being non empty DTree-yielding FinSequence such that
A7:
( dom F = dom B & F . 1 = v with-replacement ((g /. 1),(root-tree [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)])) & ( for i, j being Element of dom B st j = i + 1 holds
for d being DecoratedTree st d = F . i holds
F . j = H2(i,d) ) )
from MSAFREE5:sch 8();
rng F c= Union the Sorts of (Free (S,Y))
proof
let a be
object ;
TARSKI:def 3 ( not a in rng F or a in Union the Sorts of (Free (S,Y)) )
assume
a in rng F
;
a in Union the Sorts of (Free (S,Y))
then consider b being
object such that B1:
(
b in dom F &
a = F . b )
by FUNCT_1:def 3;
reconsider b =
b as
Element of
dom B by A7, B1;
defpred S1[
Nat]
means ( $1
in dom B implies (
F . $1
in Union the
Sorts of
(Free (S,Y)) &
g . $1
in dom (F . $1) &
(F . $1) . (g . $1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . $1),(B . $1)] & ( for
j being
Nat st
j > $1 &
j in dom B holds
(
g . j in dom (F . $1) &
(F . $1) . (g . j) = [(V1 . j),(B . j)] ) ) ) );
B2:
S1[1]
proof
assume
1
in dom B
;
( F . 1 in Union the Sorts of (Free (S,Y)) & g . 1 in dom (F . 1) & (F . 1) . (g . 1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)] & ( for j being Nat st j > 1 & j in dom B holds
( g . j in dom (F . 1) & (F . 1) . (g . j) = [(V1 . j),(B . j)] ) ) )
then reconsider b = 1 as
Element of
dom B ;
reconsider bb =
b as
Element of
dom g by AA, MCART_1:def 13;
g . b in rng g
by AA, AB, FUNCT_1:def 3;
then consider xi being
Element of
dom v such that B3:
(
g . b = xi & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . xi = [y,s] )
by AA;
consider s being
SortSymbol of
S,
y being
Element of
Y . s such that B4:
v . xi = [y,s]
by B3;
reconsider v2 =
( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term as
Element of
(Free (S,Y)) ;
f . b = v . (g . b)
by AA, AB;
then
(
V1 . b = [y,s] `1 &
B . b = [y,s] `2 )
by B3, B4, AB, MCART_1:def 12, MCART_1:def 13;
then B6:
(
v . (g . b) = [(V1 . b),(B . b)] &
the_sort_of v2 = B . b )
by B3, B4, SORT;
B7:
g /. bb = g . bb
by AA, A0, PARTFUN1:def 6;
F . b is
Element of
(Free (S,Y)),
(the_sort_of v)
by A7, B6, B7, Th117;
hence
F . 1
in Union the
Sorts of
(Free (S,Y))
;
( g . 1 in dom (F . 1) & (F . 1) . (g . 1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)] & ( for j being Nat st j > 1 & j in dom B holds
( g . j in dom (F . 1) & (F . 1) . (g . j) = [(V1 . j),(B . j)] ) ) )
C1:
dom (F . b) = (dom v) with-replacement (
(g /. bb),
(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term)))
by B3, B7, A7, TREES_2:def 11;
hence
g . 1
in dom (F . 1)
by B3, B7, TREES_1:def 9;
( (F . 1) . (g . 1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)] & ( for j being Nat st j > 1 & j in dom B holds
( g . j in dom (F . 1) & (F . 1) . (g . j) = [(V1 . j),(B . j)] ) ) )
then consider r being
FinSequence of
NAT such that CD:
(
r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) &
xi = xi ^ r &
(F . b) . xi = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r )
by C1, A7, B7, B3, TREES_2:def 11;
r = {}
by CD, FINSEQ_1:87;
hence
(F . 1) . (g . 1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)]
by CD, B3, TREES_4:3;
for j being Nat st j > 1 & j in dom B holds
( g . j in dom (F . 1) & (F . 1) . (g . j) = [(V1 . j),(B . j)] )
let j be
Nat;
( j > 1 & j in dom B implies ( g . j in dom (F . 1) & (F . 1) . (g . j) = [(V1 . j),(B . j)] ) )
assume C2:
(
j > 1 &
j in dom B )
;
( g . j in dom (F . 1) & (F . 1) . (g . j) = [(V1 . j),(B . j)] )
then
g . j in rng g
by AA, AB, FUNCT_1:def 3;
then consider xi2 being
Element of
dom v such that C3:
(
g . j = xi2 & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . xi2 = [y,s] )
by AA;
consider s being
SortSymbol of
S,
y being
Element of
Y . s such that C4:
v . xi2 = [y,s]
by C3;
f . j = v . (g . j)
by C2, AA, AB;
then B0:
(
V1 . j = [y,s] `1 &
B . j = [y,s] `2 )
by C3, C4, C2, AB, MCART_1:def 12, MCART_1:def 13;
xi <> xi2
by AA, AB, C2, C3, B3, FUNCT_1:def 4;
then C6:
not
xi c= xi2
by B4, Lem9;
then C8:
for
r being
FinSequence of
NAT holds
( not
r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not
xi2 = xi ^ r or not
(v with-replacement ((g /. bb),(( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) . xi2 = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r )
by TREES_1:1;
C7:
( not
xi c< xi2 &
dom (F . b) = (dom v) with-replacement (
xi,
(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) )
by A7, B3, C6, B7, TREES_2:def 11, XBOOLE_0:def 8;
hence
g . j in dom (F . 1)
by C3, TREES_1:def 9;
(F . 1) . (g . j) = [(V1 . j),(B . j)]
hence
(F . 1) . (g . j) = [(V1 . j),(B . j)]
by C7, C8, B3, B7, A7, B0, C3, C4, TREES_2:def 11;
verum
end;
B8:
for
i being
Nat st
i >= 1 &
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( i >= 1 & S1[i] implies S1[i + 1] )
assume Z1:
i >= 1
;
( not S1[i] or S1[i + 1] )
assume Z2:
S1[
i]
;
S1[i + 1]
assume Z3:
i + 1
in dom B
;
( F . (i + 1) in Union the Sorts of (Free (S,Y)) & g . (i + 1) in dom (F . (i + 1)) & (F . (i + 1)) . (g . (i + 1)) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (i + 1)),(B . (i + 1))] & ( for j being Nat st j > i + 1 & j in dom B holds
( g . j in dom (F . (i + 1)) & (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] ) ) )
then
i + 1
<= len B
by FINSEQ_3:25;
then D0:
i < len B
by NAT_1:13;
then D1:
(
i in dom B &
i + 1
> i )
by Z1, NAT_1:13, FINSEQ_3:25;
reconsider v1 =
F . i as
Element of
(Free (S,Y)) by Z2, D0, Z1, FINSEQ_3:25;
reconsider b =
i,
b1 =
i + 1 as
Element of
dom B by D0, Z3, Z1, FINSEQ_3:25;
D2:
(
g . (i + 1) in dom v1 &
v1 . (g . (i + 1)) = [(V1 . b1),(B . b1)] )
by D1, Z2, Z3;
D3:
(
g . b in dom v1 &
v1 . (g . b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] )
by Z2;
reconsider xi1 =
g . b,
xi2 =
g . (i + 1) as
Element of
dom v1 by Z2, D1, Z3;
D4:
(
g /. b = xi1 &
g /. b1 = xi2 )
by AA, AB, PARTFUN1:def 6;
the_sort_of (D . b) = B . b
by SORT;
then reconsider v2 =
v1 with-replacement (
xi1,
(D . b)) as
Element of
(Free (S,Y)),
(the_sort_of v1) by D3, Th117;
xi1 <> xi2
by AA, AB, Z3, D1, FUNCT_1:def 4;
then D5:
not
xi1 c= xi2
by D3, Lem9;
then D6:
for
r being
FinSequence of
NAT holds
( not
r in dom (D . b) or not
xi2 = xi1 ^ r or not
v2 . xi2 = (D . b) . r )
by TREES_1:1;
reconsider t1 =
( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1) -term as
Element of
(Free (S,Y)) ;
not
xi1 c< xi2
by D5, XBOOLE_0:def 8;
then DD:
xi2 in (dom v1) with-replacement (
xi1,
(dom (D . b)))
by TREES_1:def 9;
then D7:
(
xi2 in dom v2 &
v2 . xi2 = [(V1 . b1),(B . b1)] &
the_sort_of t1 = B . b1 )
by D6, D2, SORT, TREES_2:def 11;
reconsider xi3 =
xi2 as
Element of
dom v2 by DD, TREES_2:def 11;
reconsider v3 =
v2 with-replacement (
xi3,
t1) as
Element of
(Free (S,Y)),
(the_sort_of v2) by D7, Th117;
D8:
F . (i + 1) = v3
by D4, A7;
hence
F . (i + 1) in Union the
Sorts of
(Free (S,Y))
;
( g . (i + 1) in dom (F . (i + 1)) & (F . (i + 1)) . (g . (i + 1)) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (i + 1)),(B . (i + 1))] & ( for j being Nat st j > i + 1 & j in dom B holds
( g . j in dom (F . (i + 1)) & (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] ) ) )
D9:
dom (F . b1) = (dom v2) with-replacement (
xi3,
(dom t1))
by D8, TREES_2:def 11;
thus
g . (i + 1) in dom (F . (i + 1))
by D9, TREES_1:def 9;
( (F . (i + 1)) . (g . (i + 1)) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (i + 1)),(B . (i + 1))] & ( for j being Nat st j > i + 1 & j in dom B holds
( g . j in dom (F . (i + 1)) & (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] ) ) )
then consider r being
FinSequence of
NAT such that D10:
(
r in dom t1 &
xi3 = xi3 ^ r &
v3 . xi3 = t1 . r )
by D9, TREES_2:def 11;
r = {}
by D10, FINSEQ_1:87;
hence
(F . (i + 1)) . (g . (i + 1)) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (i + 1)),(B . (i + 1))]
by D8, D10, TREES_4:3;
for j being Nat st j > i + 1 & j in dom B holds
( g . j in dom (F . (i + 1)) & (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] )
let j be
Nat;
( j > i + 1 & j in dom B implies ( g . j in dom (F . (i + 1)) & (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] ) )
assume E1:
(
j > i + 1 &
j in dom B )
;
( g . j in dom (F . (i + 1)) & (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] )
then reconsider b2 =
j as
Element of
dom B ;
EE:
j > i
by E1, NAT_1:13;
then E2:
(
g . j in dom v1 &
v1 . (g . j) = [(V1 . b2),(B . b2)] )
by E1, Z2, D0, Z1, FINSEQ_3:25;
reconsider xi =
g . j as
Element of
dom v1 by EE, E1, Z2, D0, Z1, FINSEQ_3:25;
xi1 <> xi
by E1, AA, AB, D1, FUNCT_1:def 4;
then E5:
not
xi1 c= xi
by D3, Lem9;
then E6:
for
r being
FinSequence of
NAT holds
( not
r in dom (D . b) or not
xi = xi1 ^ r or not
v2 . xi = (D . b) . r )
by TREES_1:1;
reconsider t2 =
( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b2) -term as
Element of
(Free (S,Y)) ;
not
xi1 c< xi
by E5, XBOOLE_0:def 8;
then EF:
xi in (dom v1) with-replacement (
xi1,
(dom (D . b)))
by TREES_1:def 9;
then E7:
(
xi in dom v2 &
v2 . xi = [(V1 . b2),(B . b2)] &
the_sort_of t2 = B . b2 )
by E6, E2, SORT, TREES_2:def 11;
reconsider xi =
xi as
Element of
dom v2 by EF, TREES_2:def 11;
xi3 <> xi
by AA, AB, Z3, E1, FUNCT_1:def 4;
then E9:
not
xi3 c= xi
by Lem9, D2;
then
not
xi3 c< xi
by XBOOLE_0:def 8;
hence E8:
g . j in dom (F . (i + 1))
by D9, TREES_1:def 9;
(F . (i + 1)) . (g . j) = [(V1 . j),(B . j)]
for
r being
FinSequence of
NAT holds
( not
r in dom t1 or not
xi = xi3 ^ r or not
v3 . xi = t1 . r )
by E9, TREES_1:1;
hence
(F . (i + 1)) . (g . j) = [(V1 . j),(B . j)]
by E7, D8, D9, E8, TREES_2:def 11;
verum
end;
B9:
for
i being
Nat st
i >= 1 holds
S1[
i]
from NAT_1:sch 8(B2, B8);
b >= 1
by FINSEQ_3:25;
hence
a in Union the
Sorts of
(Free (S,Y))
by B1, B9;
verum
end;
then reconsider F = F as FinSequence of (Free (S,Y)) by FINSEQ_1:def 4;
defpred S1[ Nat] means for b being Element of dom B st $1 = b holds
( F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b & dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) );
F1:
S1[1]
proof
let b be
Element of
dom B;
( 1 = b implies ( F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b & dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) ) )
assume F2:
1
= b
;
( F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b & dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) )
reconsider xi =
g /. b as
Element of
dom v ;
reconsider t =
( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term as
Element of
(Free (S,Y)) ;
reconsider F1 =
F . 1 as
Element of
(Free (S,Y)) by A7, F2, FUNCT_1:102;
F3:
F1 = v with-replacement (
xi,
t)
by A7, F2;
FD:
dom F1 = (dom v) with-replacement (
xi,
(dom t))
by A7, F2, TREES_2:def 11;
v is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b -omitting
proof
assume
Coim (
v,
[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)])
<> {}
;
MSAFREE5:def 21 contradiction
then consider a being
object such that F4:
a in Coim (
v,
[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)])
by XBOOLE_0:7;
F5:
(
a in dom v &
v . a in {[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)]} )
by F4, FUNCT_1:def 7;
reconsider a =
a as
Element of
dom v by F4, FUNCT_1:def 7;
F7:
v . a = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)]
by F5, TARSKI:def 1;
then
a in rng g
by AA;
then consider i being
object such that F6:
(
i in dom g &
g . i = a )
by FUNCT_1:def 3;
reconsider i =
i as
Element of
dom B by AA, F6, MCART_1:def 13;
f . i = v . a
by AA, F6;
then
(
V1 . i = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] `1 &
dom V1 = dom f )
by AB, F7, MCART_1:def 12;
then
( the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b in rng V1 &
rng V1 misses rng the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y )
by AB, OMIT2, FUNCT_1:def 3;
then
( the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b nin rng the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y &
dom the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y = dom B )
by SORTS, XBOOLE_0:3;
hence
contradiction
by FUNCT_1:def 3;
verum
end;
hence
F . b is
context of the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b
by F2, F3, Lem10;
( dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) )
g . b = xi
by AA, AB, PARTFUN1:def 6;
then
xi in rng g
by AA, AB, FUNCT_1:def 3;
then consider nu being
Element of
dom v such that G0:
(
xi = nu & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . nu = [y,s] )
by AA;
thus
dom v c= dom (F . b)
by G0, F2, F3, Lem11;
( (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) )
then
(
xi ^ {} = xi &
xi in dom F1 )
by F2;
then consider mu being
FinSequence of
NAT such that H0:
(
mu in dom t &
xi = xi ^ mu &
F1 . xi = t . mu )
by A7, F2, FD, TREES_2:def 11;
mu = {}
by H0, FINSEQ_1:87;
hence
(F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)]
by F2, H0, TREES_4:3;
for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] )
let b1 be
Element of
dom B;
( b1 > b implies ( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) )
assume G1:
b1 > b
;
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] )
thus
F /. b is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 -omitting
(F . b) . (g /. b1) = [(V1 . b1),(B . b1)]proof
assume
Coim (
(F /. b),
[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)])
<> {}
;
MSAFREE5:def 21 contradiction
then consider i being
object such that G2:
i in Coim (
(F /. b),
[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)])
by XBOOLE_0:7;
G3:
(
i in dom (F /. b) &
(F /. b) . i in {[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]} )
by G2, FUNCT_1:def 7;
reconsider i =
i as
Element of
dom (F /. b) by G2, FUNCT_1:def 7;
G4:
F /. b = F . b
by A7, PARTFUN1:def 6;
G5:
(F /. b) . i = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]
by G3, TARSKI:def 1;
G7:
dom F1 = (dom v) with-replacement (
xi,
(dom t))
by A7, F2, TREES_2:def 11;
per cases then
( ( not xi is_a_prefix_of i & F1 . i = v . i ) or ex r being FinSequence of NAT st
( r in dom t & i = xi ^ r & F1 . i = t . r ) )
by F2, A7, G4, TREES_2:def 11;
suppose G6:
( not
xi is_a_prefix_of i &
F1 . i = v . i )
;
contradictionthen
for
r being
FinSequence of
NAT holds
( not
r in dom t or not
i = xi ^ r )
by TREES_1:1;
then
i is
Element of
dom v
by G4, G7, F2, TREES_1:def 9;
then
i in rng g
by AA, G5, G6, G4, F2;
then consider j being
object such that G8:
(
j in dom g &
g . j = i )
by FUNCT_1:def 3;
reconsider j =
j as
Element of
dom B by AA, G8, MCART_1:def 13;
f . j = v . (g . j)
by AA, AB;
then
(
V1 . j = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)] `1 &
dom V1 = dom B )
by AB, G8, G6, G5, G4, F2, MCART_1:def 12;
then
( the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 in rng V1 &
rng V1 misses rng the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y )
by OMIT2, FUNCT_1:def 3;
then
( the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 nin rng the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y &
dom the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y = dom B )
by SORTS, XBOOLE_0:3;
hence
contradiction
by FUNCT_1:def 3;
verum end; end;
end;
K2:
(
xi = g . b &
g /. b1 = g . b1 )
by AA, AB, PARTFUN1:def 6;
then K0:
(
v . xi = f . b &
v . (g /. b1) = f . b1 &
g /. b1 in rng g &
xi in rng g )
by AA, AB, FUNCT_1:def 3;
then consider mu being
Element of
dom v such that K1:
(
mu = g /. b1 & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . mu = [y,s] )
by AA;
reconsider fb1 =
f . b1 as
pair object by K2, K1, AA, AB;
K3:
v . mu =
[(fb1 `1),(fb1 `2)]
by K2, K1, AA, AB
.=
[(V1 . b1),(fb1 `2)]
by AB, MCART_1:def 12
.=
[(V1 . b1),(B . b1)]
by AB, MCART_1:def 13
;
consider nu being
Element of
dom v such that K4:
(
nu = xi & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . nu = [y,s] )
by AA, K0;
reconsider fb =
f . b as
pair object by K2, K4, AA, AB;
K5:
v . xi =
[(fb `1),(fb `2)]
by K2, AA, AB
.=
[(V1 . b),(fb `2)]
by AB, MCART_1:def 12
.=
[(V1 . b),(B . b)]
by AB, MCART_1:def 13
;
xi <> mu
by AA, AB, K1, K2, G1, FUNCT_1:def 4;
then K6:
not
xi c= mu
by K5, Lem9;
then
not
xi c< mu
by XBOOLE_0:def 8;
then K7:
mu in (dom v) with-replacement (
xi,
(dom t))
by TREES_1:def 9;
for
r being
FinSequence of
NAT holds
( not
r in dom t or not
mu = xi ^ r or not
F1 . mu = t . r )
by K6, TREES_1:1;
hence
(F . b) . (g /. b1) = [(V1 . b1),(B . b1)]
by F2, A7, K1, K3, K7, TREES_2:def 11;
verum
end;
WW:
for i being Nat st 1 <= i & S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( 1 <= i & S1[i] implies S1[i + 1] )
assume H1:
( 1
<= i &
S1[
i] )
;
S1[i + 1]
let b be
Element of
dom B;
( i + 1 = b implies ( F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b & dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) ) )
assume H2:
i + 1
= b
;
( F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b & dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) )
reconsider xi =
g /. b as
Element of
dom v ;
reconsider t =
( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term as
Element of
(Free (S,Y)) ;
i + 1
<= len F
by A7, H2, FINSEQ_3:25;
then HH:
( 1
<= i &
i < len F )
by H1, NAT_1:13;
reconsider F1 =
F . (i + 1),
Fi =
F . i as
Element of
(Free (S,Y)) by HH, A7, H2, FUNCT_1:102, FINSEQ_3:25;
reconsider bi =
i as
Element of
dom B by HH, A7, FINSEQ_3:25;
reconsider Fi =
Fi as
context of the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . bi by H1;
reconsider nu =
g /. bi as
Element of
dom v ;
F3:
F1 = (Fi with-replacement (nu,(D . bi))) with-replacement (
xi,
t)
by A7, H2;
H8:
(
b > bi &
F /. bi = Fi )
by A7, H2, NAT_1:13, PARTFUN1:def 6;
then H5:
(
Fi is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b -omitting &
Fi . xi = [(V1 . b),(B . b)] )
by H1;
I2:
(
D . bi in the
Sorts of
(Free (S,Y)) . (B . bi) &
dom v c= dom Fi )
by H1;
(
nu = g . bi &
xi = g . b )
by AA, AB, PARTFUN1:def 6;
then H6:
(
Fi . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . bi),(B . bi)] &
the_sort_of (D . bi) = B . bi &
nu in dom Fi &
xi in dom Fi &
nu <> xi )
by AA, AB, I2, H1, H8, SORT, FUNCT_1:def 4;
then H7:
Fi with-replacement (
nu,
(D . bi))
= Fi -sub (D . bi)
by Th118;
I1:
not
nu c= xi
by H6, Lem9;
then
not
nu c< xi
by XBOOLE_0:def 8;
then I3:
xi in (dom Fi) with-replacement (
nu,
(dom (D . bi)))
by H6, TREES_1:def 9;
then H9:
xi in dom (Fi -sub (D . bi))
by H6, H7, TREES_2:def 11;
D . bi is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b -omitting
by OMIT4;
then
Fi -sub (D . bi) is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b -omitting
by H5, H6, Th45A;
hence
F . b is
context of the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b
by H2, F3, H7, H9, Lem10;
( dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) )
for
r being
FinSequence of
NAT holds
( not
r in dom (D . bi) or not
xi = nu ^ r or not
(Fi with-replacement (nu,(D . bi))) . xi = (D . bi) . r )
by I1, TREES_1:1;
then
(Fi -sub (D . bi)) . xi = [(V1 . b),(B . b)]
by I3, H5, H6, H7, TREES_2:def 11;
then L1:
(
dom Fi c= dom (Fi -sub (D . bi)) &
dom (Fi -sub (D . bi)) c= dom F1 )
by F3, H7, H9, H6, Lem11;
hence
dom v c= dom (F . b)
by I2, H2;
( (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) )
(
xi in dom F1 &
dom F1 = (dom (Fi -sub (D . bi))) with-replacement (
xi,
(dom t)) )
by L1, F3, H7, H6, TREES_2:def 11;
then consider r being
FinSequence of
NAT such that J0:
(
r in dom t &
xi = xi ^ r &
F1 . xi = t . r )
by H7, H9, F3, TREES_2:def 11;
r = {}
by J0, FINSEQ_1:87;
hence
(F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)]
by H2, J0, TREES_4:3;
for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] )
let b1 be
Element of
dom B;
( b1 > b implies ( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) )
assume J1:
b1 > b
;
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] )
thus
F /. b is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 -omitting
(F . b) . (g /. b1) = [(V1 . b1),(B . b1)]proof
assume
Coim (
(F /. b),
[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)])
<> {}
;
MSAFREE5:def 21 contradiction
then consider a being
object such that J2:
a in Coim (
(F /. b),
[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)])
by XBOOLE_0:7;
J3:
(
a in dom (F /. b) &
(F /. b) . a in {[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]} )
by J2, FUNCT_1:def 7;
reconsider q =
a as
Element of
dom (F /. b) by J2, FUNCT_1:def 7;
J4:
F /. b = F . b
by A7, PARTFUN1:def 6;
then J5:
(
q in (dom (Fi -sub (D . bi))) with-replacement (
xi,
(dom t)) &
(dom (Fi -sub (D . bi))) with-replacement (
xi,
(dom t))
= dom F1 )
by F3, J3, H2, H7, H9, TREES_2:def 11;
per cases then
( ( not xi is_a_prefix_of q & F1 . q = (Fi -sub (D . bi)) . q ) or ex r being FinSequence of NAT st
( r in dom t & q = xi ^ r & F1 . q = t . r ) )
by F3, H7, H9, TREES_2:def 11;
suppose J6:
( not
xi is_a_prefix_of q &
F1 . q = (Fi -sub (D . bi)) . q )
;
contradictionthen J7:
q in dom (Fi -sub (D . bi))
by H9, J5, Th01;
b1 > bi
by J1, H2, NAT_1:13;
then
(
Fi is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 -omitting &
D . bi is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 -omitting )
by H1, H8, OMIT4;
then
Fi -sub (D . bi) is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . b1 -omitting
by H6, Th45A;
hence
contradiction
by J7, H2, J3, J4, J6, FUNCT_1:def 7;
verum end; end;
end;
reconsider mu =
g /. b1 as
Node of
v ;
L5:
(
bi < b1 &
b > bi )
by J1, H2, NAT_1:13;
then L2:
(
Fi . (g /. b1) = [(V1 . b1),(B . b1)] &
Fi . (g /. b) = [(V1 . b),(B . b)] )
by H1;
(
g /. b1 = g . b1 &
g /. b = g . b &
g /. bi = g . bi )
by AA, AB, PARTFUN1:def 6;
then
(
g /. b1 <> g /. b &
g /. bi <> g /. b1 &
g /. b1 in dom Fi &
g /. b in dom Fi &
g /. bi in dom Fi )
by AB, AA, J1, I2, L5, FUNCT_1:def 4;
then L3:
( not
g /. b c= g /. b1 & not
nu c= mu )
by H6, L2, Lem9;
then L4:
for
r being
FinSequence of
NAT holds
( not
r in dom (D . bi) or not
mu = nu ^ r or not
(Fi -sub (D . bi)) . mu = (D . bi) . r )
by TREES_1:1;
L6:
(
nu in dom Fi &
g /. b1 in dom (Fi -sub (D . bi)) )
by I2, L1;
then
g /. b1 in (dom Fi) with-replacement (
nu,
(dom (D . bi)))
by H7, TREES_2:def 11;
then L7:
(Fi -sub (D . bi)) . (g /. b1) = [(V1 . b1),(B . b1)]
by L4, L2, L6, H7, TREES_2:def 11;
L4:
for
r being
FinSequence of
NAT holds
( not
r in dom t or not
mu = xi ^ r or not
F1 . mu = t . r )
by L3, TREES_1:1;
g /. b1 in dom Fi
by I2;
then L6:
(
xi in dom (Fi -sub (D . bi)) &
g /. b1 in dom F1 )
by I2, L1;
then
g /. b1 in (dom (Fi -sub (D . bi))) with-replacement (
xi,
(dom t))
by H7, F3, TREES_2:def 11;
hence
(F . b) . (g /. b1) = [(V1 . b1),(B . b1)]
by H2, L4, L6, L7, F3, H7, TREES_2:def 11;
verum
end;
L8:
for i being Nat st i >= 1 holds
S1[i]
from NAT_1:sch 8(F1, WW);
F is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y -context-sequence
then reconsider F = F as the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y -context-sequence FinSequence of (Free (S,Y)) ;
take
F
; ( F is V1, the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) )
thus
F is V1, the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y,D -consequent-context-sequence
( (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) )proof
let i,
j be
Element of
dom B;
MSAFREE5:def 40 ( i + 1 = j implies (F . j) -sub ((V1 . j) -term) = (F . i) -sub (D . i) )
reconsider nu =
g /. i,
xi =
g /. j as
Node of
v ;
reconsider Fi =
F . i,
Fj =
F . j as
Element of
(Free (S,Y)) ;
reconsider t =
( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . j) -term as
Element of
(Free (S,Y)) ;
H1:
i >= 1
by FINSEQ_3:25;
assume H2:
i + 1
= j
;
(F . j) -sub ((V1 . j) -term) = (F . i) -sub (D . i)
H3:
j >= 1
by H2, NAT_1:12;
F3:
F . j = (Fi with-replacement (nu,(D . i))) with-replacement (
xi,
t)
by A7, H2;
H8:
(
j > i &
F /. i = Fi )
by A7, H2, NAT_1:13, PARTFUN1:def 6;
then H5:
(
Fi is the
one-to-one B -sorts V1 -omitting D -omitting FinSequence of
Union Y . j -omitting &
Fi . xi = [(V1 . j),(B . j)] )
by H1, L8;
I2:
(
D . i in the
Sorts of
(Free (S,Y)) . (B . i) &
dom v c= dom Fi )
by H1, L8;
(
nu = g . i &
xi = g . j )
by AA, AB, PARTFUN1:def 6;
then H6:
(
Fi . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . i),(B . i)] &
the_sort_of (D . i) = B . i &
nu in dom Fi &
xi in dom Fi &
nu <> xi )
by H1, AA, AB, I2, L8, H8, SORT, FUNCT_1:def 4;
then H7:
Fi with-replacement (
nu,
(D . i))
= (F . i) -sub (D . i)
by Th118;
reconsider q =
(V1 . j) -term as
Element of
(Free (S,Y)) ;
M1:
not
nu c= xi
by H6, Lem9;
then H4:
for
r being
FinSequence of
NAT holds
( not
r in dom (D . i) or not
xi = nu ^ r or not
((F . i) -sub (D . i)) . xi = (D . i) . r )
by TREES_1:1;
not
nu c< xi
by M1, XBOOLE_0:def 8;
then
xi in (dom Fi) with-replacement (
nu,
(dom (D . i)))
by H6, TREES_1:def 9;
then M8:
(
((F . i) -sub (D . i)) . xi = [(V1 . j),(B . j)] &
xi in dom ((F . i) -sub (D . i)) )
by H4, H5, H6, H7, TREES_2:def 11;
then M3:
(
dom ((F . i) -sub (D . i)) = dom Fj &
dom v c= dom Fj )
by H3, L8, F3, H7, Lem11A;
M2:
(
Fj . xi = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . j),(B . j)] &
the_sort_of q = B . j &
xi in dom Fj )
by M8, H3, L8, SORT, F3, H7, Lem11A;
then M5:
(F . j) -sub q = (F . j) with-replacement (
xi,
q)
by Th118;
hence M4:
dom ((F . j) -sub ((V1 . j) -term)) = dom ((F . i) -sub (D . i))
by M3, M2, Lem11A;
TREES_4:def 1 for b1 being Element of proj1 ((F . j) -sub ((V1 . j) -term)) holds ((F . j) -sub ((V1 . j) -term)) . b1 = ((F . i) -sub (D . i)) . b1
let a be
Node of
((F . j) -sub ((V1 . j) -term));
((F . j) -sub ((V1 . j) -term)) . a = ((F . i) -sub (D . i)) . a
(
a in dom ((F . j) -sub ((V1 . j) -term)) &
dom ((F . j) -sub ((V1 . j) -term)) = (dom Fj) with-replacement (
xi,
(dom q)) )
by M2, M5, TREES_2:def 11;
end;
set b = In (1,(dom B));
reconsider nu = g /. (In (1,(dom B))), xi = g /. (len B) as Node of v ;
NK:
( 1 <= In (1,(dom B)) & In (1,(dom B)) <= len B )
by FINSEQ_3:25;
N6:
F . (In (1,(dom B))) = v with-replacement (nu,(( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term))
by A7;
NM:
nu = g . (In (1,(dom B)))
by AA, AB, PARTFUN1:def 6;
then
( v . nu = f . (In (1,(dom B))) & nu in rng g )
by AB, AA, FUNCT_1:def 3;
then consider mu being Node of v such that
N5:
( nu = mu & ex s being SortSymbol of S ex y being Element of Y . s st v . mu = [y,s] )
by AA;
reconsider fb = f . (In (1,(dom B))) as pair object by NM, N5, AB, AA;
N7: v . nu =
[(fb `1),(fb `2)]
by NM, AB, AA
.=
[(V1 . (In (1,(dom B)))),(fb `2)]
by AB, MCART_1:def 12
.=
[(V1 . (In (1,(dom B)))),(B . (In (1,(dom B))))]
by AB, MCART_1:def 13
;
then N8:
dom (F . (In (1,(dom B)))) = dom v
by N6, Lem11A;
reconsider t = (V1 . (In (1,(dom B)))) -term as Element of (Free (S,Y)) ;
O3:
dom (F . (In (1,(dom B)))) = (dom v) with-replacement (nu,(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term)))
by A7, TREES_2:def 11;
then consider mu being FinSequence of NAT such that
N9:
( mu in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) & nu = nu ^ mu & (F . (In (1,(dom B)))) . nu = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) . mu )
by A7, N8, TREES_2:def 11;
OA:
mu = {}
by N9, FINSEQ_1:87;
then
( (F . (In (1,(dom B)))) . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))),(B . (In (1,(dom B))))] & the_sort_of t = B . (In (1,(dom B))) )
by N9, SORT, TREES_4:3;
then O1:
(F . (In (1,(dom B)))) -sub t = (F . (In (1,(dom B)))) with-replacement (nu,t)
by N8, Th118;
hence O5:
dom ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) = dom v
by N8, OA, Lem11A, N9, TREES_4:3; TREES_4:def 1 ( ( for b1 being Element of proj1 ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) holds ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) . b1 = v . b1 ) & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) )
hereby h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))
let a be
Node of
((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term));
((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) . b1 = v . b1
dom ((F . (In (1,(dom B)))) -sub t) = (dom (F . (In (1,(dom B))))) with-replacement (
nu,
(dom t))
by N8, O1, TREES_2:def 11;
per cases then
( ( not nu c= a & ((F . (In (1,(dom B)))) -sub t) . a = (F . (In (1,(dom B)))) . a ) or ex r being FinSequence of NAT st
( r in dom t & a = nu ^ r & ((F . (In (1,(dom B)))) -sub t) . a = t . r ) )
by N8, O1, TREES_2:def 11;
suppose O4:
( not
nu c= a &
((F . (In (1,(dom B)))) -sub t) . a = (F . (In (1,(dom B)))) . a )
;
((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) . b1 = v . b1then
for
r being
FinSequence of
NAT holds
( not
r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) or not
a = nu ^ r or not
(F . (In (1,(dom B)))) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) . r )
by TREES_1:1;
hence
((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) . a = v . a
by A7, N8, O3, O4, O5, TREES_2:def 11;
verum end; end;
end;
defpred S2[ Nat] means for b, b1 being Element of dom B st $1 = b & b1 <= b holds
( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) );
S1:
S2[1]
proof
let b,
b1 be
Element of
dom B;
( 1 = b & b1 <= b implies ( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) ) )
assume S2:
( 1
= b &
b1 <= b )
;
( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) )
b1 >= 1
by FINSEQ_3:25;
then S3:
b1 = 1
by S2, XXREAL_0:1;
reconsider nu =
g /. b as
Node of
v ;
S4:
(
(F . b) . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] &
nu in dom v &
dom v c= dom (F . b) &
the_sort_of (D . b) = B . b )
by S2, F1, SORT;
then S8:
(F . b) -sub (D . b) = (F . b) with-replacement (
nu,
(D . b))
by Th118;
then S7:
((F . b) -sub (D . b)) | nu = D . b
by S4, Th130;
SD:
nu = g . b
by AA, AB, PARTFUN1:def 6;
then S5:
(
v . nu = f . b &
nu in rng g )
by AA, AB, FUNCT_1:def 3;
then consider mu being
Node of
v such that S6:
(
nu = mu & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . mu = [y,s] )
by AA;
reconsider fb =
f . b as
pair object by SD, S6, AA, AB;
SC:
v . nu =
[(fb `1),(fb `2)]
by SD, AA, AB
.=
[(V1 . b),(fb `2)]
by AB, MCART_1:def 12
.=
[(V1 . b),(B . b)]
by AB, MCART_1:def 13
;
then
v | nu = (V1 . b) -term
by Th132;
then
(h . v) | nu = h . ((V1 . b) -term)
by Th131;
hence
((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1)
by A2, S7, S2, S3;
((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g))
dom (F . b) c= dom ((F . b) -sub (D . b))
by S4, S8, Lem11;
then
(dom v) \ (rng g) c= dom ((F . b) -sub (D . b))
by S4;
hence
dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) = dom (v | ((dom v) \ (rng g)))
by RELAT_1:62;
FUNCT_1:def 11 for b1 being object holds
( not b1 in proj1 (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) or (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . b1 = (v | ((dom v) \ (rng g))) . b1 )
let a be
object ;
( not a in proj1 (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) or (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a )
assume SK:
a in dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g)))
;
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a
then
a in (dom v) \ (rng g)
;
then reconsider a =
a as
Node of
v ;
SJ:
(
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = ((F . b) -sub (D . b)) . a &
(v | ((dom v) \ (rng g))) . a = v . a )
by SK, FUNCT_1:49;
nu <> a
by S5, SK, XBOOLE_0:def 5;
then SD:
not
nu c= a
by SC, Lem9;
then SE:
for
r being
FinSequence of
NAT holds
( not
r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not
a = nu ^ r or not
(F . b) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r )
by TREES_1:1;
SG:
not
nu c< a
by SD, XBOOLE_0:def 8;
then
a in (dom v) with-replacement (
nu,
(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term)))
by TREES_1:def 9;
then SI:
v . a = (F . b) . a
by A7, S2, SE, TREES_2:def 11;
SF:
for
r being
FinSequence of
NAT holds
( not
r in dom (D . b) or not
a = nu ^ r or not
((F . b) -sub (D . b)) . a = (D . b) . r )
by SD, TREES_1:1;
(
a in dom (F . b) &
nu in dom (F . b) )
by S4;
then
a in (dom (F . b)) with-replacement (
nu,
(dom (D . b)))
by SG, TREES_1:def 9;
hence
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a
by SI, SJ, SF, S4, S8, TREES_2:def 11;
verum
end;
T1:
for i being Nat st i >= 1 & S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( i >= 1 & S2[i] implies S2[i + 1] )
assume T2:
(
i >= 1 &
S2[
i] )
;
S2[i + 1]
let b,
b1 be
Element of
dom B;
( i + 1 = b & b1 <= b implies ( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) ) )
assume T3:
(
b = i + 1 &
b1 <= b )
;
( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) )
then
i + 1
<= len B
by FINSEQ_3:25;
then
i < len B
by NAT_1:13;
then reconsider b2 =
i as
Element of
dom B by T2, FINSEQ_3:25;
T5:
F . b = ((F . b2) with-replacement ((g /. b2),(D . b2))) with-replacement (
(g /. b),
(( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))
by A7, T3;
(
v . (g . b) = f . b &
g . b in rng g )
by AA, AB, FUNCT_1:def 3;
then consider nu being
Node of
v such that U2:
(
g . b = nu & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . nu = [y,s] )
by AA;
reconsider fb =
f . b as
pair object by U2, AA, AB;
U3:
v . (g /. b) =
v . (g . b)
by AA, AB, PARTFUN1:def 6
.=
[(fb `1),(fb `2)]
by AA, AB
.=
[(V1 . b),(fb `2)]
by AB, MCART_1:def 12
.=
[(V1 . b),(B . b)]
by AB, MCART_1:def 13
;
T7:
(
the_sort_of (D . b2) = B . b2 &
(F . b2) . (g /. b2) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b2),(B . b2)] &
g /. b2 in dom v &
dom v c= dom (F . b2) )
by T2, L8, SORT;
then T6:
(F . b2) -sub (D . b2) = (F . b2) with-replacement (
(g /. b2),
(D . b2))
by Th118;
T18:
(
g /. b1 = g . b1 &
g /. b = g . b )
by AA, AB, PARTFUN1:def 6;
dom (F . b2) c= dom ((F . b2) -sub (D . b2))
by T6, T7, Lem11;
then T21:
(
g /. b in dom ((F . b2) -sub (D . b2)) &
g /. b1 in dom ((F . b2) -sub (D . b2)) )
by T7;
per cases
( b1 < b or b1 = b )
by T3, XXREAL_0:1;
suppose
b1 < b
;
( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) )then T8:
(
b1 <= b2 &
g . b1 <> g . b )
by AA, AB, T3, FUNCT_1:def 4, NAT_1:13;
then T4:
((F . b2) -sub (D . b2)) | (g /. b1) = (h . v) | (g /. b1)
by T2;
(
v . (g . b1) = f . b1 &
g . b1 in rng g )
by AA, AB, FUNCT_1:def 3;
then consider nu being
Node of
v such that U5:
(
g . b1 = nu & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . nu = [y,s] )
by AA;
reconsider fb1 =
f . b1 as
pair object by U5, AA, AB;
U6:
v . (g /. b1) =
v . (g . b1)
by AA, AB, PARTFUN1:def 6
.=
[(fb1 `1),(fb1 `2)]
by AA, AB
.=
[(V1 . b1),(fb1 `2)]
by AB, MCART_1:def 12
.=
[(V1 . b1),(B . b1)]
by AB, MCART_1:def 13
;
T9:
( not
g /. b c= g /. b1 & not
g /. b1 c= g /. b )
by T18, T8, U3, U6, Lem9;
then T10:
(F . b) | (g /. b1) = (h . v) | (g /. b1)
by T21, T4, T5, T6, Th133;
1
<= i + 1
by NAT_1:12;
then T12:
(
(F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] &
g /. b in dom v &
dom v c= dom (F . b) &
g /. b1 in dom v &
the_sort_of (D . b) = B . b )
by T3, L8, SORT;
then T11:
(F . b) -sub (D . b) = (F . b) with-replacement (
(g /. b),
(D . b))
by Th118;
hence
((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1)
by T10, T12, T9, Th133;
((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g))
(
dom v c= dom (F . b) &
dom (F . b) c= dom ((F . b) -sub (D . b)) )
by T12, T11, Lem11;
then
(dom v) \ (rng g) c= dom ((F . b) -sub (D . b))
;
hence
dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) = dom (v | ((dom v) \ (rng g)))
by RELAT_1:62;
FUNCT_1:def 11 for b1 being object holds
( not b1 in proj1 (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) or (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . b1 = (v | ((dom v) \ (rng g))) . b1 )let a be
object ;
( not a in proj1 (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) or (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a )assume TT:
a in dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g)))
;
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . areconsider a =
a as
Node of
((F . b) -sub (D . b)) by TT, RELAT_1:57;
T16:
(
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = ((F . b) -sub (D . b)) . a &
(((F . b2) -sub (D . b2)) | ((dom v) \ (rng g))) . a = ((F . b2) -sub (D . b2)) . a &
(v | ((dom v) \ (rng g))) . a = v . a )
by TT, FUNCT_1:49;
then T17:
((F . b2) -sub (D . b2)) . a = v . a
by T2;
(
g /. b in rng g &
a nin rng g &
a in dom v )
by T18, AA, AB, TT, XBOOLE_0:def 5, FUNCT_1:def 3;
then T19:
( not
g /. b c= a &
a in dom (F . b) &
dom (F . b) = (dom ((F . b2) -sub (D . b2))) with-replacement (
(g /. b),
(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) )
by T18, U2, T21, T5, T6, T12, Lem9, TREES_2:def 11;
then
for
r being
FinSequence of
NAT holds
( not
r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not
a = (g /. b) ^ r or not
(F . b) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r )
by TREES_1:1;
then T22:
(F . b) . a = v . a
by T18, U2, T17, T19, T21, T5, T6, TREES_2:def 11;
T24:
(
a in dom ((F . b) -sub (D . b)) &
dom ((F . b) -sub (D . b)) = (dom (F . b)) with-replacement (
(g /. b),
(dom (D . b))) )
by T12, T18, U2, T11, TREES_2:def 11;
for
r being
FinSequence of
NAT holds
( not
r in dom (D . b) or not
a = (g /. b) ^ r or not
((F . b) -sub (D . b)) . a = (D . b) . r )
by T19, TREES_1:1;
hence
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a
by T16, T18, U2, T11, T22, T12, T24, TREES_2:def 11;
verum end; suppose U7:
b1 = b
;
( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) )reconsider nu =
g /. b as
Node of
v ;
i + 1
>= 1
by NAT_1:12;
then S4:
(
(F . b) . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] &
nu in dom v &
dom v c= dom (F . b) &
the_sort_of (D . b) = B . b )
by T3, L8, SORT;
then T11:
(F . b) -sub (D . b) = (F . b) with-replacement (
nu,
(D . b))
by Th118;
then S7:
((F . b) -sub (D . b)) | nu = D . b
by S4, Th130;
T18:
nu = g . b
by AA, AB, PARTFUN1:def 6;
then
(
v . nu = f . b &
nu in rng g )
by AA, AB, FUNCT_1:def 3;
then consider mu being
Node of
v such that S6:
(
nu = mu & ex
s being
SortSymbol of
S ex
y being
Element of
Y . s st
v . mu = [y,s] )
by AA;
reconsider fb =
f . b as
pair object by T18, S6, AA, AB;
v . nu =
[(fb `1),(fb `2)]
by T18, AA, AB
.=
[(V1 . b),(fb `2)]
by AB, MCART_1:def 12
.=
[(V1 . b),(B . b)]
by AB, MCART_1:def 13
;
then
v | nu = (V1 . b) -term
by Th132;
then
(h . v) | nu = h . ((V1 . b) -term)
by Th131;
hence
((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1)
by A2, S7, U7;
((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g))
(
dom v c= dom (F . b) &
dom (F . b) c= dom ((F . b) -sub (D . b)) )
by S4, T11, Lem11;
then
(dom v) \ (rng g) c= dom ((F . b) -sub (D . b))
;
hence
dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) = dom (v | ((dom v) \ (rng g)))
by RELAT_1:62;
FUNCT_1:def 11 for b1 being object holds
( not b1 in proj1 (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) or (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . b1 = (v | ((dom v) \ (rng g))) . b1 )let a be
object ;
( not a in proj1 (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) or (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a )assume T24:
a in dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g)))
;
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . athen reconsider a =
a as
Node of
((F . b) -sub (D . b)) by RELAT_1:57;
T16:
(
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = ((F . b) -sub (D . b)) . a &
(((F . b2) -sub (D . b2)) | ((dom v) \ (rng g))) . a = ((F . b2) -sub (D . b2)) . a &
(v | ((dom v) \ (rng g))) . a = v . a )
by T24, FUNCT_1:49;
then T17:
((F . b2) -sub (D . b2)) . a = v . a
by T2;
(
g /. b in rng g &
a nin rng g &
a in dom v )
by T18, AA, AB, T24, XBOOLE_0:def 5, FUNCT_1:def 3;
then T19:
( not
g /. b c= a &
a in dom (F . b) &
dom (F . b) = (dom ((F . b2) -sub (D . b2))) with-replacement (
(g /. b),
(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) )
by T21, T5, T6, S4, Lem9, TREES_2:def 11;
then
for
r being
FinSequence of
NAT holds
( not
r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not
a = (g /. b) ^ r or not
(F . b) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r )
by TREES_1:1;
then T22:
(F . b) . a = v . a
by T18, T17, T19, T21, T5, T6, TREES_2:def 11;
T24:
(
a in dom ((F . b) -sub (D . b)) &
dom ((F . b) -sub (D . b)) = (dom (F . b)) with-replacement (
(g /. b),
(dom (D . b))) )
by S4, T11, TREES_2:def 11;
for
r being
FinSequence of
NAT holds
( not
r in dom (D . b) or not
a = (g /. b) ^ r or not
((F . b) -sub (D . b)) . a = (D . b) . r )
by T19, TREES_1:1;
hence
(((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a
by T16, T11, T22, S4, T24, TREES_2:def 11;
verum end; end;
end;
set b = In ((len B),(dom B));
set v1 = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))));
SK:
for i being Nat st i >= 1 holds
S2[i]
from NAT_1:sch 8(S1, T1);
S8:
( (F . (In ((len B),(dom B)))) . (g /. (In ((len B),(dom B)))) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In ((len B),(dom B)))),(B . (In ((len B),(dom B))))] & dom v c= dom (F . (In ((len B),(dom B)))) )
by L8, NK;
then SA:
( the_sort_of (D . (In ((len B),(dom B)))) = B . (In ((len B),(dom B))) & g /. (In ((len B),(dom B))) in dom (F . (In ((len B),(dom B)))) )
by SORT;
then
(F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) = (F . (In ((len B),(dom B)))) with-replacement ((g /. (In ((len B),(dom B)))),(D . (In ((len B),(dom B)))))
by S8, Th118;
then
dom (F . (In ((len B),(dom B)))) c= dom ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))))
by SA, S8, Lem11;
then S9:
( dom v c= dom ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))) & v | ((dom v) \ (rng g)) = ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))) | ((dom v) \ (rng g)) )
by SK, S8, NK;
hence
h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))
by AA, S9, Th138; verum