let S be non empty non void ManySortedSign ; for s, s1 being SortSymbol 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 st the_sort_of C9 = s1 holds
for z1 being b4 -different Element of Z . s1
for C1 being b4 -omitting context of z1 holds C1 -sub C9 is context of z
let s, s1 be SortSymbol 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 st the_sort_of C9 = s1 holds
for z1 being b2 -different Element of Z . s1
for C1 being b2 -omitting context of z1 holds C1 -sub C9 is context of z
let Z be non-trivial ManySortedSet of the carrier of S; for z being Element of Z . s
for C9 being context of z st the_sort_of C9 = s1 holds
for z1 being b1 -different Element of Z . s1
for C1 being b1 -omitting context of z1 holds C1 -sub C9 is context of z
let z be Element of Z . s; for C9 being context of z st the_sort_of C9 = s1 holds
for z1 being z -different Element of Z . s1
for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z
let C9 be context of z; ( the_sort_of C9 = s1 implies for z1 being z -different Element of Z . s1
for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z )
assume A1:
the_sort_of C9 = s1
; for z1 being z -different Element of Z . s1
for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z
let z1 be z -different Element of Z . s1; for C1 being z -omitting context of z1 holds C1 -sub C9 is context of z
defpred S1[ Element of (Free (S,Z))] means ( $1 is z -omitting implies ($1,[z1,s1]) <- C9 is context of z );
A2:
S1[z1 -term ]
;
A3:
for o being OperSymbol of S
for k being Element of Args (o,(Free (S,Z))) st k is z1 -context_including & S1[z1 -context_in k] holds
for C being context of z1 st C = o -term k holds
S1[C]
proof
let o be
OperSymbol of
S;
for k being Element of Args (o,(Free (S,Z))) st k is z1 -context_including & S1[z1 -context_in k] holds
for C being context of z1 st C = o -term k holds
S1[C]let k be
Element of
Args (
o,
(Free (S,Z)));
( k is z1 -context_including & S1[z1 -context_in k] implies for C being context of z1 st C = o -term k holds
S1[C] )
set p =
k;
assume that A2:
k is
z1 -context_including
and A3:
S1[
z1 -context_in k]
;
for C being context of z1 st C = o -term k holds
S1[C]
let C be
context of
z1;
( C = o -term k implies S1[C] )
assume AA:
C = o -term k
;
S1[C]
assume c:
C is
z -omitting
;
(C,[z1,s1]) <- C9 is context of z
set t =
C9;
deffunc H1(
Nat)
-> set = (
(k /. $1),
[z1,s1])
<- C9;
consider q being
FinSequence such that A4:
(
len q = len k & ( for
i being
Nat st
i in dom q holds
q . i = H1(
i) ) )
from FINSEQ_1:sch 2();
A5:
(
dom q = dom k &
dom k <> {} )
by A2, A4, FINSEQ_3:29;
then A6:
( not
k is
empty & not
q is
empty )
;
A8:
dom k = dom (the_arity_of o)
by MSUALG_6:2;
then A9:
len q = len (the_arity_of o)
by A5, FINSEQ_3:29;
now for i being Nat st i in dom q holds
q . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i)let i be
Nat;
( i in dom q implies q . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1) )assume B1:
i in dom q
;
q . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1)then B2:
k /. i = k . i
by A5, PARTFUN1:def 6;
per cases
( z1 -context_pos_in k = i or z1 -context_pos_in k <> i )
;
suppose
z1 -context_pos_in k = i
;
q . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1)then B3:
(
z1 -context_in k = k . i &
q . i = H1(
i) &
k /. i is
z -omitting )
by c, AA, A5, A4, A2, Th71, Th54;
k . i in the
Sorts of
(Free (S,Z)) . ((the_arity_of o) /. i)
by B1, A5, A8, MSUALG_6:2;
then
the_sort_of (z1 -context_in k) = (the_arity_of o) /. i
by B3, SORT;
hence
q . i in the
Sorts of
(Free (S,Z)) . ((the_arity_of o) /. i)
by A1, B2, B3, aaa1;
verum end; suppose
z1 -context_pos_in k <> i
;
q . b1 in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. b1)then
k /. i is
z1 -omitting
by A2, A5, B1, Th72;
then
(
q . i = H1(
i) &
H1(
i)
= k . i )
by A4, B1, B2, Th23;
hence
q . i in the
Sorts of
(Free (S,Z)) . ((the_arity_of o) /. i)
by B1, A5, A8, MSUALG_6:2;
verum end; end;
then reconsider q =
q as
Element of
Args (
o,
(Free (S,Z)))
by A9, MSAFREE2:5;
now for i being Nat
for d1 being DecoratedTree st i in dom k & d1 = k . i holds
q . i = (d1,[z1,s1]) <- C9let i be
Nat;
for d1 being DecoratedTree st i in dom k & d1 = k . i holds
q . i = (d1,[z1,s1]) <- C9let d1 be
DecoratedTree;
( i in dom k & d1 = k . i implies q . i = (d1,[z1,s1]) <- C9 )assume
(
i in dom k &
d1 = k . i )
;
q . i = (d1,[z1,s1]) <- C9then
(
q . i = H1(
i) &
k /. i = d1 )
by A4, A5, PARTFUN1:def 6;
hence
q . i = (
d1,
[z1,s1])
<- C9
;
verum end;
then A7: (
(o -term k),
[z1,s1])
<- C9 =
[o, the carrier of S] -tree q
by A5, A6, ThL8
.=
o -term q
;
q is
z -context_including
proof
take i =
z1 -context_pos_in k;
MSAFREE5:def 24 ( i in dom q & q . i is context of z & ( for j being Nat
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting ) )
thus
i in dom q
by A2, A5, Th71;
( q . i is context of z & ( for j being Nat
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting ) )
then B2:
k /. i = k . i
by A5, PARTFUN1:def 6;
(
z1 -context_in k = k . i &
q . i = H1(
i) &
k /. i is
z -omitting )
by c, AA, A5, A4, A2, Th71, Th54;
hence
q . i is
context of
z
by B2, A3;
for j being Nat
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting
let j be
Nat;
for t being Element of (Free (S,Z)) st j in dom q & j <> i & t = q . j holds
t is z -omitting let q1 be
Element of
(Free (S,Z));
( j in dom q & j <> i & q1 = q . j implies q1 is z -omitting )
assume B4:
(
j in dom q &
j <> i &
q1 = q . j )
;
q1 is z -omitting
then B5:
k /. j = k . j
by A5, PARTFUN1:def 6;
k /. j is
z1 -omitting
by A2, B4, A5, Th72;
then
(
q1 = H1(
j) &
H1(
j)
= k . j )
by B4, A4, B5, Th23;
hence
q1 is
z -omitting
by c, B5, B4, A5, AA, Th54;
verum
end;
hence
(
C,
[z1,s1])
<- C9 is
context of
z
by AA, A7, Th53;
verum
end;
let C1 be z -omitting context of z1; C1 -sub C9 is context of z
S1[C1]
from MSAFREE5:sch 4(A2, A3);
hence
C1 -sub C9 is context of z
by A1, SUB; verum