set NH = OSNat_Hom (ParsedTermsOSA X),(LCongruence X);
set A = OSFreeGen s,X;
set R = LCongruence X;
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set NHs = OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s;
set D = DTConOSA X;
A1:
(OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s = OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s
by OSALG_4:def 24;
defpred S1[ set , set ] means for t being Symbol of (DTConOSA X) st $1 = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) holds
$2 = root-tree t;
A2:
for x being set st x in OSFreeGen s,X holds
ex a being set st
( a in PTVars s,X & S1[x,a] )
proof
let x be
set ;
:: thesis: ( x in OSFreeGen s,X implies ex a being set st
( a in PTVars s,X & S1[x,a] ) )
assume
x in OSFreeGen s,
X
;
:: thesis: ex a being set st
( a in PTVars s,X & S1[x,a] )
then
x in { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }
by Th31;
then consider t being
Symbol of
(DTConOSA X) such that A3:
(
x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) &
t in Terminals (DTConOSA X) &
t `2 = s )
;
consider s1 being
Element of
S,
a being
set such that A4:
(
a in X . s1 &
t = [a,s1] )
by A3, Th4;
A5:
s = s1
by A3, A4, MCART_1:7;
take
root-tree t
;
:: thesis: ( root-tree t in PTVars s,X & S1[x, root-tree t] )
thus
root-tree t in PTVars s,
X
by A4, A5, Def24;
:: thesis: S1[x, root-tree t]
reconsider rt =
root-tree t as
Element of the
Sorts of
(ParsedTermsOSA X) . s by A4, A5, Th10;
reconsider tt =
root-tree t as
Element of
TS (DTConOSA X) by A4, Th10;
A6:
OSClass (LCongruence X),
tt = OSClass (LCongruence X),
rt
by Def28;
A7:
OSClass (LCongruence X),
tt <> {}
by Th33;
A8:
x = (OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s) . (root-tree t)
by A3, OSALG_4:def 24;
A9:
(OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s) . rt = OSClass (LCongruence X),
rt
by OSALG_4:def 23;
A10:
x <> {}
by A6, A7, A8, OSALG_4:def 23;
let t1 be
Symbol of
(DTConOSA X);
:: thesis: ( x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t1) implies root-tree t = root-tree t1 )
assume A11:
x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t1)
;
:: thesis: root-tree t = root-tree t1
then A12:
x = (OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s) . (root-tree t1)
by OSALG_4:def 24;
root-tree t1 in dom (OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s)
by A1, A10, A11, FUNCT_1:def 4;
then reconsider rt1 =
root-tree t1 as
Element of the
Sorts of
(ParsedTermsOSA X) . s ;
reconsider tt2 =
rt1 as
Element of
TS (DTConOSA X) by Th16;
A13:
OSClass (LCongruence X),
rt1 = OSClass (LCongruence X),
rt
by A8, A9, A12, OSALG_4:def 23;
OSClass (LCongruence X),
tt2 = OSClass (LCongruence X),
rt1
by Def28;
then
tt2 in OSClass (LCongruence X),
tt
by A6, A13, Th35;
hence
root-tree t = root-tree t1
by A4, Th37;
:: thesis: verum
end;
consider f being Function such that
A14:
( dom f = OSFreeGen s,X & rng f c= PTVars s,X & ( for x being set st x in OSFreeGen s,X holds
S1[x,f . x] ) )
from WELLORD2:sch 1(A2);
reconsider f = f as Function of (OSFreeGen s,X),(PTVars s,X) by A14, FUNCT_2:4;
take
f
; :: thesis: for t being Symbol of (DTConOSA X) st ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X holds
f . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t
let t be Symbol of (DTConOSA X); :: thesis: ( ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X implies f . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t )
assume
((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X
; :: thesis: f . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t
hence
f . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t
by A14; :: thesis: verum