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

proof

let x be set ; :: thesis: ( x in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):] implies ex y being set st
( y in Funcs X,INT & S₁[x,y] ) )
assume x in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):] ; :: thesis: ex y being set st
( y in Funcs X,INT & S₁[x,y] )
then consider s, I being set such that
A4: s in Funcs X,INT and
A5: I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X)) and
A6: x = [s,I] by ZFMISC_1:def 2;
reconsider s = s as Element of Funcs X,INT by A4;
consider a being Symbol of (DTConUA ECIW-signature ,(INT-ElemIns X)) such that
A7: I = root-tree a and
A8: a in Terminals (DTConUA ECIW-signature ,(INT-ElemIns X)) by A2, A5;
consider v, e being set such that
A9: v in Funcs (Funcs X,INT ),X and
A10: e in Funcs (Funcs X,INT ),INT and
A11: a = [v,e] by A1, A8, ZFMISC_1:def 2;
reconsider e = e as Element of Funcs (Funcs X,INT ),INT by A10;
reconsider v = v as Element of Funcs (Funcs X,INT ),X by A9;
take y = s +* (v . s),(e . s); :: thesis: ( y in Funcs X,INT & S₁[x,y] )
thus y in Funcs X,INT by FUNCT_2:11; :: thesis: S₁[x,y]
take s ; :: thesis: ex v being Element of Funcs (Funcs X,INT ),X ex e being Element of Funcs (Funcs X,INT ),INT st
( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) )
take v ; :: thesis: ex e being Element of Funcs (Funcs X,INT ),INT st
( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) )
take e ; :: thesis: ( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) )
thus ( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) ) by A6, A7, A11; :: thesis: verum

end;

consider g being Function such that
A12: ( dom g = [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):] & rng g c= Funcs X,INT ) and
A13: for x being set st x in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):] holds
S₁[x,g . x] from WELLORD2:sch 1(A3);
reconsider g = g as Function of [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):],(Funcs X,INT ) by A12, FUNCT_2:4;
consider f being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X), Funcs X,INT ,(Funcs X,INT ) \ x,0 such that
A14: f | [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):] = g and
for s being Element of Funcs X,INT
for C, I being Element of (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X)) 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: for s being Element of Funcs X,INT
for v being Element of Funcs (Funcs X,INT ),X
for e being Element of Funcs (Funcs X,INT ),INT holds f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
let s be Element of 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 f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
let v be Element of Funcs (Funcs X,INT ),X; :: thesis: for e being Element of Funcs (Funcs X,INT ),INT holds f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
let e be Element of Funcs (Funcs X,INT ),INT ; :: thesis: f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
set I = root-tree [v,e];
[v,e] in INT-ElemIns X by ZFMISC_1:106;
then root-tree [v,e] in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X)) by A2, A1;
then A15: [s,(root-tree [v,e])] in [:(Funcs X,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X))):] by ZFMISC_1:106;
then consider s9 being Element of Funcs X,INT , v9 being Element of Funcs (Funcs X,INT ),X, e9 being Element of Funcs (Funcs X,INT ),INT such that
A16: [s,(root-tree [v,e])] = [s9,(root-tree [v9,e9])] and
A17: g . [s,(root-tree [v,e])] = s9 +* (v9 . s9),(e9 . s9) by A13;
root-tree [v,e] = root-tree [v9,e9] by A16, ZFMISC_1:33;
then A18: [v,e] = [v9,e9] by TREES_4:4;
then A19: v = v9 by ZFMISC_1:33;
A20: e = e9 by A18, ZFMISC_1:33;
s = s9 by A16, ZFMISC_1:33;
hence f . s,(root-tree [v,e]) = s +* (v . s),(e . s) by A14, A15, A17, A19, A20, FUNCT_1:72; :: thesis: verum