defpred S1[ Element of NAT , Instruction-Location of S] means $1 in card (NIC (pi M,$2),$2);
reconsider n = FirstLoc M as Element of NAT by AMI_1:def 4;
defpred S2[ set , set ] means ex l being Instruction-Location of S st
( l = $2 & $1 in card (NIC (pi M,l),l) );
defpred S3[ set , Element of NAT , set ] means ex l being Instruction-Location of S st
( l = $1 & ( $2 in dom (LocSeq (NIC (pi M,l),l)) implies $3 = (LocSeq (NIC (pi M,l),l)) . $2 ) & ( not $2 in dom (LocSeq (NIC (pi M,l),l)) implies $3 = il. S,0 ) );
set D = NAT ;
A1: for x, y being Element of NAT ex z being Element of NAT st S3[x,y,z]
proof
let x, y be Element of NAT ; :: thesis: ex z being Element of NAT st S3[x,y,z]
reconsider x = x as Instruction-Location of S by AMI_1:def 4;
set z = (LocSeq (NIC (pi M,x),x)) . y;
per cases ( y in dom (LocSeq (NIC (pi M,x),x)) or not y in dom (LocSeq (NIC (pi M,x),x)) ) ;
suppose A2: y in dom (LocSeq (NIC (pi M,x),x)) ; :: thesis: ex z being Element of NAT st S3[x,y,z]
take (LocSeq (NIC (pi M,x),x)) . y ; :: thesis: ( (LocSeq (NIC (pi M,x),x)) . y is Element of NAT & S3[x,y,(LocSeq (NIC (pi M,x),x)) . y] )
A3: rng (LocSeq (NIC (pi M,x),x)) c= NAT by RELAT_1:def 19;
(LocSeq (NIC (pi M,x),x)) . y in rng (LocSeq (NIC (pi M,x),x)) by A2, FUNCT_1:def 5;
hence ( (LocSeq (NIC (pi M,x),x)) . y is Element of NAT & S3[x,y,(LocSeq (NIC (pi M,x),x)) . y] ) by A2, A3; :: thesis: verum
end;
suppose A4: not y in dom (LocSeq (NIC (pi M,x),x)) ; :: thesis: ex z being Element of NAT st S3[x,y,z]
reconsider il = il. S,0 as Element of NAT by AMI_1:def 4;
take il ; :: thesis: S3[x,y,il]
thus S3[x,y,il] by A4; :: thesis: verum
end;
end;
end;
consider f being Function of [:NAT ,NAT :], NAT such that
A5: for l, n being Element of NAT holds S3[l,n,f . l,n] from BINOP_1:sch 3(A1);
 A6: for d, k1, k2 being Element of NAT st k1 <= k2 & S2[k2,d] holds
S2[k1,d]
proof
let d be Element of NAT ; :: thesis: for k1, k2 being Element of NAT st k1 <= k2 & S2[k2,d] holds
S2[k1,d]
let k1, k2 be Element of NAT ; :: thesis: ( k1 <= k2 & S2[k2,d] implies S2[k1,d] )
assume that
A7: k1 <= k2 and
A8: S2[k2,d] ; :: thesis: S2[k1,d]
reconsider d = d as Instruction-Location of S by AMI_1:def 4;
take d ; :: thesis: ( d = d & k1 in card (NIC (pi M,d),d) )
k1 c= k2 by A7, NAT_1:40;
hence ( d = d & k1 in card (NIC (pi M,d),d) ) by A8, ORDINAL1:22; :: thesis: verum
end;
consider T being DecoratedTree of NAT such that
A9: T . {} = n and
A10: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : S2[k,T . t] } & ( for n being Element of NAT st S2[n,T . t] holds
T . (t ^ <*n*>) = f . (T . t),n ) ) from TREES_2:sch 10(A6);
 reconsider T = T as IL-DecoratedTree of S by AMI_1:def 37;
take T ; :: thesis: ( T . {} = FirstLoc M & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T . t)),(T . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T . t)),(T . t)) holds
T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m ) ) ) )
{} in dom T by TREES_1:47;
hence T . {} = FirstLoc M by A9, AMI_1:def 38; :: thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T . t)),(T . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T . t)),(T . t)) holds
T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m ) )
let t be Element of dom T; :: thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(T . t)),(T . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(T . t)),(T . t)) holds
T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m ) )
A11: T . t = T . t by AMI_1:def 38;
deffunc H1( Element of NAT ) -> FinSequence of NAT = t ^ <*$1*>;
set X = { H1(k) where k is Element of NAT : ex l being Instruction-Location of S st
( l = T . t & S1[k,l] ) } ;
set Y = { H1(k) where k is Element of NAT : S1[k,T . t] } ;
{ H1(k) where k is Element of NAT : ex l being Instruction-Location of S st
( l = T . t & S1[k,l] ) } = { H1(k) where k is Element of NAT : S1[k,T . t] } from AMI_1:sch 2();
 hence A12: succ t = { H1(k) where k is Element of NAT : S1[k,T . t] } by A10, A11; :: thesis: for m being Element of NAT st m in card (NIC (pi M,(T . t)),(T . t)) holds
T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m
reconsider n = T . t as Element of NAT by ORDINAL1:def 13;
let m be Element of NAT ; :: thesis: ( m in card (NIC (pi M,(T . t)),(T . t)) implies T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m )
consider l being Instruction-Location of S such that
A13: l = n and
A14: ( m in dom (LocSeq (NIC (pi M,l),l)) implies f . n,m = (LocSeq (NIC (pi M,l),l)) . m ) and
( not m in dom (LocSeq (NIC (pi M,l),l)) implies f . n,m = il. S,0 ) by A5;
assume A15: m in card (NIC (pi M,(T . t)),(T . t)) ; :: thesis: T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m
then t ^ <*m*> in { H1(k) where k is Element of NAT : S1[k,l] } by A13;
then T . (t ^ <*m*>) = T . (t ^ <*m*>) by A12, A13, AMI_1:def 38;
hence T . (t ^ <*m*>) = (LocSeq (NIC (pi M,(T . t)),(T . t))) . m by A10, A11, A15, A13, A14, Def4; :: thesis: verum