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

set Q = Funcs (NAT,INT);

set T = (Funcs (NAT,INT)) \ (0,0);

set S = ECIW-signature ;

set G = INT-ElemIns ;

set A = FreeUnivAlgNSG (ECIW-signature,INT-ElemIns);

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

reconsider q0 = NAT --> i0 as Element of Funcs (NAT,INT) by FUNCT_2:8;

defpred S_{1}[ object , object ] means ex s being Element of Funcs (NAT,INT) ex v being Element of Funcs ((Funcs (NAT,INT)),NAT) ex e being Element of Funcs ((Funcs (NAT,INT)),INT) st

( $1 = [s,(root-tree [v,e])] & $2 = s +* ((v . s),(e . s)) );

A2: ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) = FreeGenSetNSG (ECIW-signature,INT-ElemIns) by AOFA_000:70;

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

ex y being object st

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

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

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

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

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

consider f being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) such that

A14: f | [:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] = g and

for s being Element of Funcs (NAT,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 (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds f . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))

let s be Element of Funcs (NAT,INT); :: thesis: for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds f . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))

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

let e be Element of Funcs ((Funcs (NAT,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 by ZFMISC_1:87;

then root-tree [v,e] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A2, A1;

then A15: [s,(root-tree [v,e])] in [:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] by ZFMISC_1:87;

then consider s9 being Element of Funcs (NAT,INT), v9 being Element of Funcs ((Funcs (NAT,INT)),NAT), e9 being Element of Funcs ((Funcs (NAT,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

set Q = Funcs (NAT,INT);

set T = (Funcs (NAT,INT)) \ (0,0);

set S = ECIW-signature ;

set G = INT-ElemIns ;

set A = FreeUnivAlgNSG (ECIW-signature,INT-ElemIns);

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

reconsider q0 = NAT --> i0 as Element of Funcs (NAT,INT) by FUNCT_2:8;

defpred S

( $1 = [s,(root-tree [v,e])] & $2 = s +* ((v . s),(e . s)) );

A2: ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) = FreeGenSetNSG (ECIW-signature,INT-ElemIns) by AOFA_000:70;

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

ex y being object st

( y in Funcs (NAT,INT) & S

proof

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

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

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

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

then consider s, I being object such that

A4: s in Funcs (NAT,INT) and

A5: I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) and

A6: x = [s,I] by ZFMISC_1:def 2;

reconsider s = s as Element of Funcs (NAT,INT) by A4;

consider a being Symbol of (DTConUA (ECIW-signature,INT-ElemIns)) such that

A7: I = root-tree a and

A8: a in Terminals (DTConUA (ECIW-signature,INT-ElemIns)) by A2, A5;

consider v, e being object such that

A9: v in Funcs ((Funcs (NAT,INT)),NAT) and

A10: e in Funcs ((Funcs (NAT,INT)),INT) and

A11: a = [v,e] by A1, A8, ZFMISC_1:def 2;

reconsider e = e as Element of Funcs ((Funcs (NAT,INT)),INT) by A10;

reconsider v = v as Element of Funcs ((Funcs (NAT,INT)),NAT) by A9;

take y = s +* ((v . s),(e . s)); :: thesis: ( y in Funcs (NAT,INT) & S_{1}[x,y] )

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

take s ; :: thesis: ex v being Element of Funcs ((Funcs (NAT,INT)),NAT) ex e being Element of Funcs ((Funcs (NAT,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 (NAT,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;( y in Funcs (NAT,INT) & S

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

( y in Funcs (NAT,INT) & S

then consider s, I being object such that

A4: s in Funcs (NAT,INT) and

A5: I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) and

A6: x = [s,I] by ZFMISC_1:def 2;

reconsider s = s as Element of Funcs (NAT,INT) by A4;

consider a being Symbol of (DTConUA (ECIW-signature,INT-ElemIns)) such that

A7: I = root-tree a and

A8: a in Terminals (DTConUA (ECIW-signature,INT-ElemIns)) by A2, A5;

consider v, e being object such that

A9: v in Funcs ((Funcs (NAT,INT)),NAT) and

A10: e in Funcs ((Funcs (NAT,INT)),INT) and

A11: a = [v,e] by A1, A8, ZFMISC_1:def 2;

reconsider e = e as Element of Funcs ((Funcs (NAT,INT)),INT) by A10;

reconsider v = v as Element of Funcs ((Funcs (NAT,INT)),NAT) by A9;

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

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

take s ; :: thesis: ex v being Element of Funcs ((Funcs (NAT,INT)),NAT) ex e being Element of Funcs ((Funcs (NAT,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 (NAT,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

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

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

S

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

consider f being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) such that

A14: f | [:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] = g and

for s being Element of Funcs (NAT,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 (NAT,INT)

for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds f . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))

let s be Element of Funcs (NAT,INT); :: thesis: for v being Element of Funcs ((Funcs (NAT,INT)),NAT)

for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds f . (s,(root-tree [v,e])) = s +* ((v . s),(e . s))

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

let e be Element of Funcs ((Funcs (NAT,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 by ZFMISC_1:87;

then root-tree [v,e] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A2, A1;

then A15: [s,(root-tree [v,e])] in [:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] by ZFMISC_1:87;

then consider s9 being Element of Funcs (NAT,INT), v9 being Element of Funcs ((Funcs (NAT,INT)),NAT), e9 being Element of Funcs ((Funcs (NAT,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