defpred S1[ Element of (Free (S,X))] means ($1,[x,s]) <- (x -term) = $1;
A1: S1[x -term ] ;
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; :: thesis: 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))); :: thesis: ( 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
A2: p is x -context_including and
A3: S1[x -context_in p] ; :: thesis: for C being context of x st C = o -term p holds
S1[C]
set t = x -term ;
deffunc H1( Nat) -> set = ((p /. $1),[x,s]) <- (x -term);
now :: thesis: for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
p . i = (d1,[x,s]) <- (x -term)
let i be Nat; :: thesis: for d1 being DecoratedTree st i in dom p & d1 = p . i holds
p . b2 = (b3,[x,s]) <- (x -term)
let d1 be DecoratedTree; :: thesis: ( i in dom p & d1 = p . i implies p . b1 = (b2,[x,s]) <- (x -term) )
assume B1: ( i in dom p & d1 = p . i ) ; :: thesis: p . b1 = (b2,[x,s]) <- (x -term)
then B2: p /. i = d1 by PARTFUN1:def 6;
per cases ( x -context_pos_in p = i or x -context_pos_in p <> i ) ;
suppose x -context_pos_in p = i ; :: thesis: p . b1 = (b2,[x,s]) <- (x -term)
then x -context_in p = p . i by A2, Th71;
hence p . i = (d1,[x,s]) <- (x -term) by A3, B1; :: thesis: verum
end;
suppose x -context_pos_in p <> i ; :: thesis: p . b1 = (b2,[x,s]) <- (x -term)
hence p . i = (d1,[x,s]) <- (x -term) by B1, B2, A2, Th72, Th23; :: thesis: verum
end;
end;
end;
hence for C being context of x st C = o -term p holds
S1[C] by A2, ThL8; :: thesis: verum
end;
AA: S1[C] from MSAFREE5:sch 4(A1, A2);
the_sort_of (x -term) = s by SORT;
hence C -sub (x -term) = C by AA, SUB; :: thesis: verum