dom c = X
by Th6;

then reconsider c9 = c as Function of X,NAT by A1, FUNCT_2:2;

reconsider i0 = 0 as Element of INT by INT_1:def 1;

set Q = Funcs (X,INT);

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:8;

A2: Terminals (DTConUA (ECIW-signature,INT-ElemIns)) = INT-ElemIns by FREEALG:3;

defpred S_{1}[ object , object ] 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 object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] holds

ex y being object st

( y in Funcs (X,INT) & S_{1}[x,y] )

A13: ( dom g = [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] & rng g c= Funcs (X,INT) ) and

A14: for x being object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] holds

S_{1}[x,g . x]
from FUNCT_1:sch 6(A4);

reconsider g = g as Function of [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):],(Funcs (X,INT)) by A13, FUNCT_2:2;

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: 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 [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = 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 [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = 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 [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s))

let e be Element of Funcs ((Funcs (X,INT)),INT); :: thesis: f . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s))

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:8;

set v0 = cv ** (c9,NAT);

set e0 = e ** (c9,NAT);

set I = root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))];

[(cv ** (c9,NAT)),(e ** (c9,NAT))] in INT-ElemIns by ZFMISC_1:87;

then root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A3, A2;

then A16: [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] by ZFMISC_1:87;

then S_{1}[[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

A17: [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] `2 = root-tree [((c * v9) ** (c9,NAT)),(e9 ** (c9,NAT))] and

A18: g . [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] = s +* ((v9 . s),(e9 . s)) ;

A19: dom (c9 * v9) = Funcs (X,INT) by FUNCT_2:def 1;

A20: dom e = Funcs (X,INT) by FUNCT_2:def 1;

A21: dom v = Funcs (X,INT) by FUNCT_2:def 1;

A22: dom cv = Funcs (X,INT) by FUNCT_2:def 1;

A23: dom c9 = X by FUNCT_2:def 1;

A24: rng v c= X ;

A25: dom e9 = Funcs (X,INT) by FUNCT_2:def 1;

A26: dom v9 = Funcs (X,INT) by FUNCT_2:def 1;

A27: [(cv ** (c9,NAT)),(e ** (c9,NAT))] = [((c * v9) ** (c9,NAT)),(e9 ** (c9,NAT))] by A17, TREES_4:4;

then cv ** (c9,NAT) = (c * v9) ** (c9,NAT) by XTUPLE_0:1;

then A28: cv = c * v9 by A22, A19, Th5;

e ** (c9,NAT) = e9 ** (c9,NAT) by A27, XTUPLE_0:1;

then A29: e = e9 by A20, A25, Th5;

rng v9 c= X ;

then v = v9 by A24, A23, A26, A21, A28, FUNCT_1:27;

hence f . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) by A15, A16, A18, A29, FUNCT_1:49; :: thesis: verum

then reconsider c9 = c as Function of X,NAT by A1, FUNCT_2:2;

reconsider i0 = 0 as Element of INT by INT_1:def 1;

set Q = Funcs (X,INT);

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:8;

A2: Terminals (DTConUA (ECIW-signature,INT-ElemIns)) = INT-ElemIns by FREEALG:3;

defpred S

( $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 object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] holds

ex y being object st

( y in Funcs (X,INT) & S

proof

consider g being Function such that
let x be object ; :: thesis: ( x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] implies ex y being object st

( y in Funcs (X,INT) & S_{1}[x,y] ) )

assume x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] ; :: thesis: ex y being object st

( y in Funcs (X,INT) & S_{1}[x,y] )

then consider s, I being object 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;

reconsider s = s as Element of Funcs (X,INT) by A5;

A9: x `2 = I by A7;

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;

end;( y in Funcs (X,INT) & S

assume x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] ; :: thesis: ex y being object st

( y in Funcs (X,INT) & S

then consider s, I being object 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;

reconsider s = s as Element of Funcs (X,INT) by A5;

A9: x `2 = I by A7;

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;

per cases
( 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))] or 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))] ) ;

end;

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

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: ex y being object st

( y in Funcs (X,INT) & S_{1}[x,y] )

( y in Funcs (X,INT) & S

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: ( y in Funcs (X,INT) & S_{1}[x,y] )

thus y in Funcs (X,INT) by FUNCT_2:8; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A8, A9, A10, A11; :: thesis: verum

end;A11: a = [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] ;

take y = s +* ((v . s),(e . s)); :: thesis: ( y in Funcs (X,INT) & S

thus y in Funcs (X,INT) by FUNCT_2:8; :: thesis: S

thus S

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: ex y being object st

( y in Funcs (X,INT) & S_{1}[x,y] )

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

( y in Funcs (X,INT) & S

take y = s; :: thesis: ( y in Funcs (X,INT) & S_{1}[x,y] )

thus y in Funcs (X,INT) ; :: thesis: S_{1}[x,y]

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_{1}[x,y]
by A8; :: thesis: verum

end;thus y in Funcs (X,INT) ; :: thesis: S

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

A13: ( dom g = [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] & rng g c= Funcs (X,INT) ) and

A14: for x being object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] holds

S

reconsider g = g as Function of [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):],(Funcs (X,INT)) by A13, FUNCT_2:2;

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: 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 [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = 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 [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = 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 [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s))

let e be Element of Funcs ((Funcs (X,INT)),INT); :: thesis: f . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s))

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:8;

set v0 = cv ** (c9,NAT);

set e0 = e ** (c9,NAT);

set I = root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))];

[(cv ** (c9,NAT)),(e ** (c9,NAT))] in INT-ElemIns by ZFMISC_1:87;

then root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A3, A2;

then A16: [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] by ZFMISC_1:87;

then S

then consider v9 being Element of Funcs ((Funcs (X,INT)),X), e9 being Element of Funcs ((Funcs (X,INT)),INT) such that

A17: [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] `2 = root-tree [((c * v9) ** (c9,NAT)),(e9 ** (c9,NAT))] and

A18: g . [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] = s +* ((v9 . s),(e9 . s)) ;

A19: dom (c9 * v9) = Funcs (X,INT) by FUNCT_2:def 1;

A20: dom e = Funcs (X,INT) by FUNCT_2:def 1;

A21: dom v = Funcs (X,INT) by FUNCT_2:def 1;

A22: dom cv = Funcs (X,INT) by FUNCT_2:def 1;

A23: dom c9 = X by FUNCT_2:def 1;

A24: rng v c= X ;

A25: dom e9 = Funcs (X,INT) by FUNCT_2:def 1;

A26: dom v9 = Funcs (X,INT) by FUNCT_2:def 1;

A27: [(cv ** (c9,NAT)),(e ** (c9,NAT))] = [((c * v9) ** (c9,NAT)),(e9 ** (c9,NAT))] by A17, TREES_4:4;

then cv ** (c9,NAT) = (c * v9) ** (c9,NAT) by XTUPLE_0:1;

then A28: cv = c * v9 by A22, A19, Th5;

e ** (c9,NAT) = e9 ** (c9,NAT) by A27, XTUPLE_0:1;

then A29: e = e9 by A20, A25, Th5;

rng v9 c= X ;

then v = v9 by A24, A23, A26, A21, A28, FUNCT_1:27;

hence f . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) by A15, A16, A18, A29, FUNCT_1:49; :: thesis: verum