dom c = X by Th6;
then reconsider c9 = c as Function of X,NAT by A1, FUNCT_2:4;
reconsider i0 = 0 as Element of INT by INT_1:def 1;
reconsider b = 0 as Nat ;
set Q = Funcs X,INT ;
set x = (c " ) . 0 ;
set S = ECIW-signature ;
set G = INT-ElemIns ;
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
reconsider q0 = X --> i0 as Element of Funcs X,INT by FUNCT_2:11;
A2: Terminals (DTConUA ECIW-signature ,INT-ElemIns ) = INT-ElemIns by FREEALG:3;
defpred S₁[ set , set ] means ex s being Element of Funcs X,INT st
( $1 `1 = s & ( ( $2 = s & ( for v being Element of Funcs (Funcs X,INT ),X
for e being Element of Funcs (Funcs X,INT ),INT holds not $1 `2 = root-tree [((c * v) ** c9,NAT ),(e ** c9,NAT )] ) ) or ex v being Element of Funcs (Funcs X,INT ),X ex e being Element of Funcs (Funcs X,INT ),INT st
( $1 `2 = root-tree [((c * v) ** c9,NAT ),(e ** c9,NAT )] & $2 = s +* (v . s),(e . s) ) ) );
A3: ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) = FreeGenSetNSG ECIW-signature ,INT-ElemIns by AOFA_000:70;
A4: for x being set st x in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] holds
ex y being set st
( y in Funcs X,INT & S₁[x,y] )

let x be set ; :: thesis:
assume x in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] ; :: thesis:
then consider s, I being set such that
A5: s in Funcs X,INT and
A6: I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) and
A7: x = [s,I] by ZFMISC_1:def 2;
A8: x `1 = s by A7, MCART_1:7;
reconsider s = s as Element of Funcs X,INT by A5;
A9: x `2 = I by A7, MCART_1:7;
consider a being Symbol of (DTConUA ECIW-signature ,INT-ElemIns ) such that
A10: I = root-tree a and
a in Terminals (DTConUA ECIW-signature ,INT-ElemIns ) by A3, A6;

suppose ex v being Element of Funcs (Funcs X,INT ),X ex e being Element of Funcs (Funcs X,INT ),INT st a = [((c * v) ** c9,NAT ),(e ** c9,NAT )] ; :: thesis:

then consider v being Element of Funcs (Funcs X,INT ),X, e being Element of Funcs (Funcs X,INT ),INT such that
A11: a = [((c * v) ** c9,NAT ),(e ** c9,NAT )] ;
take y = s +* (v . s),(e . s); :: thesis:
thus y in Funcs X,INT by FUNCT_2:11; :: thesis:
thus S₁[x,y] by A8, A9, A10, A11; :: thesis:

end;

suppose A12: for v being Element of Funcs (Funcs X,INT ),X
for e being Element of Funcs (Funcs X,INT ),INT holds not a = [((c * v) ** c9,NAT ),(e ** c9,NAT )] ; :: thesis:

take y = s; :: thesis:
thus y in Funcs X,INT ; :: thesis:
for v being Element of Funcs (Funcs X,INT ),X
for e being Element of Funcs (Funcs X,INT ),INT holds not x `2 = root-tree [((c * v) ** c9,NAT ),(e ** c9,NAT )] by A9, A10, A12, TREES_4:4;
hence S₁[x,y] by A8; :: thesis:

end;

end;

end;

consider g being Function such that
A13: ( dom g = [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] & rng g c= Funcs X,INT ) and
A14: for x being set st x in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] holds
S₁[x,g . x] from WELLORD2:sch 1(A4);
reconsider g = g as Function of [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):],(Funcs X,INT ) by A13, FUNCT_2:4;
consider f being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs X,INT ,T such that
A15: f | [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] = g and
for s being Element of Funcs X,INT
for C, I being Element of (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = q0 by AOFA_000:91;
take f ; :: thesis:
let s be Element of Funcs X,INT ; :: thesis:
let v be Element of Funcs (Funcs X,INT ),X; :: thesis:
let e be Element of Funcs (Funcs X,INT ),INT ; :: thesis:
reconsider vv = v as Function of (Funcs X,INT ),X ;
reconsider cv = c9 * vv as Element of Funcs (Funcs X,INT ),NAT by FUNCT_2:11;
set v0 = cv ** c9,NAT ;
set e0 = e ** c9,NAT ;
set I = root-tree [(cv ** c9,NAT ),(e ** c9,NAT )];
A16: [s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])] `2 = root-tree [(cv ** c9,NAT ),(e ** c9,NAT )] by MCART_1:7;
A17: [s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])] `1 = s by MCART_1:7;
[(cv ** c9,NAT ),(e ** c9,NAT )] in INT-ElemIns by ZFMISC_1:106;
then root-tree [(cv ** c9,NAT ),(e ** c9,NAT )] in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by A3, A2;
then A18: [s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])] in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] by ZFMISC_1:106;
then S₁[[s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])],g . [s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])]] by A14;
then consider v9 being Element of Funcs (Funcs X,INT ),X, e9 being Element of Funcs (Funcs X,INT ),INT such that
A19: [s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])] `2 = root-tree [((c * v9) ** c9,NAT ),(e9 ** c9,NAT )] and
A20: g . [s,(root-tree [(cv ** c9,NAT ),(e ** c9,NAT )])] = s +* (v9 . s),(e9 . s) by A16, A17;
A21: dom (c9 * v9) = Funcs X,INT by FUNCT_2:def 1;
A22: dom e = Funcs X,INT by FUNCT_2:def 1;
A23: dom v = Funcs X,INT by FUNCT_2:def 1;
A24: dom cv = Funcs X,INT by FUNCT_2:def 1;
A25: dom c9 = X by FUNCT_2:def 1;
A26: rng v c= X ;
A27: dom e9 = Funcs X,INT by FUNCT_2:def 1;
A28: dom v9 = Funcs X,INT by FUNCT_2:def 1;
A29: [(cv ** c9,NAT ),(e ** c9,NAT )] = [((c * v9) ** c9,NAT ),(e9 ** c9,NAT )] by A19, MCART_1:7, TREES_4:4;
then cv ** c9,NAT = (c * v9) ** c9,NAT by ZFMISC_1:33;
then A30: cv = c * v9 by A24, A21, Th5;
e ** c9,NAT = e9 ** c9,NAT by A29, ZFMISC_1:33;
then A31: e = e9 by A22, A27, Th5;
rng v9 c= X ;
then v = v9 by A26, A25, A28, A23, A30, FUNCT_1:49;
hence f . s,(root-tree [((c * v) ** c,NAT ),(e ** c,NAT )]) = s +* (v . s),(e . s) by A15, A18, A20, A31, FUNCT_1:72; :: thesis: