reconsider i0 = 0 as Element of INT by INT_1:def 1;
set Q = Funcs (X,INT);
set T = (Funcs (X,INT)) \ (x,0);
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:8;
defpred S₁[ object , object ] 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 object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)))):] holds
ex y being object st
( y in Funcs (X,INT) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)))):] implies ex y being object 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 object st
( y in Funcs (X,INT) & S₁[x,y] )
then consider s, I being object 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 object 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:8; :: 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 object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)))):] holds
S₁[x,g . x] from FUNCT_1:sch 6(A3);
reconsider g = g as Function of [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)))):],(Funcs (X,INT)) by A12, FUNCT_2:2;
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:87;
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:87;
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, XTUPLE_0:1;
then A18: [v,e] = [v9,e9] by TREES_4:4;
then A19: v = v9 by XTUPLE_0:1;
A20: e = e9 by A18, XTUPLE_0:1;
s = s9 by A16, XTUPLE_0:1;
hence f . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) by A14, A15, A17, A19, A20, FUNCT_1:49; :: thesis: verum