defpred S1[ Element of (Free (S,X))] means the_sort_of S is s -reachable ;
s is s -reachable
by REWRITE1:12;
then A1:
S1[x -term ]
by SORT;
A2:
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st p is x -context_including & S1[x -context_in p] holds
for C being context of x st C = o -term p holds
S1[C]
proof
let o be
OperSymbol of
S;
for p being Element of Args (o,(Free (S,X))) st p is x -context_including & S1[x -context_in p] holds
for C being context of x st C = o -term p holds
S1[C]let p be
Element of
Args (
o,
(Free (S,X)));
( p is x -context_including & S1[x -context_in p] implies for C being context of x st C = o -term p holds
S1[C] )
assume that A3:
p is
x -context_including
and A4:
S1[
x -context_in p]
;
for C being context of x st C = o -term p holds
S1[C]
let C be
context of
x;
( C = o -term p implies S1[C] )
assume AA:
C = o -term p
;
S1[C]
A6:
the_sort_of C = the_result_sort_of o
by AA, Th8;
A5:
(
x -context_pos_in p in dom p &
dom p = dom (the_arity_of o) &
x -context_in p = p . (x -context_pos_in p) )
by A3, Th71, MSUALG_6:2;
(
x -context_in p in the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. (x -context_pos_in p)) & the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. (x -context_pos_in p)) = the
Sorts of
(Free (S,X)) . ((the_arity_of o) . (x -context_pos_in p)) )
by A5, MSUALG_6:2, PARTFUN1:def 6;
then
(
the_sort_of (x -context_in p) = (the_arity_of o) /. (x -context_pos_in p) &
(the_arity_of o) /. (x -context_pos_in p) = (the_arity_of o) . (x -context_pos_in p) &
(the_arity_of o) . (x -context_pos_in p) in rng (the_arity_of o) &
x -context_pos_in p in NAT )
by A5, SORT, FUNCT_1:def 3, PARTFUN1:def 6;
then
[(the_sort_of (x -context_in p)),(the_result_sort_of o)] in TranslationRel S
by A5, MSUALG_6:def 3;
then
(
TranslationRel S reduces the_sort_of (x -context_in p),
the_result_sort_of o &
TranslationRel S reduces s,
the_sort_of (x -context_in p) )
by A4, REACH, REWRITE1:15;
hence
TranslationRel S reduces s,
the_sort_of C
by A6, REWRITE1:16;
MSAFREE5:def 33 verum
end;
S1[C]
from MSAFREE5:sch 4(A1, A2);
hence
the_sort_of C is s -reachable
; verum