let n, m be Integer; :: thesis: ( n >= 0 implies for sm, sn, pn being FinSequence of INT
for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) )
assume A1: n >= 0 ; :: thesis: for sm, sn, pn being FinSequence of INT
for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) )
then reconsider n2 = n as Element of NAT by INT_1:3;
let sm, sn, pn be FinSequence of INT ; :: thesis: for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) )
let i be Integer; :: thesis:
assume that
A2: len sm = n + 1 and
A3: ( len sn = n + 1 & len pn = n + 1 ) and
A4: ( not n < m implies ( sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) ; :: thesis:
( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) )

1 <= n2 + 1 by NAT_1:12;
then A5: 1 in Seg (len sm) by A2, FINSEQ_1:1;
assume A6: not n < m ; :: thesis:
then reconsider i2 = i as Element of NAT by A4, INT_1:3;
A7: 1 <= i2 + 1 by NAT_1:12;
A8: i2 <= n2 + 1 by A4, A6, NAT_1:13;
A9: for k being Integer st 1 <= k & k n )

let k be Integer; :: thesis:
assume that
A10: 1 <= k and
A11: k < i ; :: thesis:
reconsider k2 = k as Element of NAT by A10, INT_1:3;
A12: 1 <= k2 + 1 by NAT_1:12;
A13: k2 < n2 + 1 by A8, A11, XXREAL_0:2;
then k2 + 1 <= n2 + 1 by NAT_1:13;
then A14: k2 + 1 in Seg (n2 + 1) by A12, FINSEQ_1:1;
k in Seg (n2 + 1) by A10, A13, FINSEQ_1:1;
hence ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) by A2, A4, A6, A10, A11, A14, FINSEQ_1:def 3; :: thesis:

end;

A15: for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) )

proof

let j be Integer; :: thesis:
assume that
A16: 1 <= j and
A17: j <= i ; :: thesis:
j - 1 >= 0 by A16, XREAL_1:48;
then (i + 1) + 0 <= (i + 1) + (j - 1) by XREAL_1:7;
then A18: (i + 1) - (j - 1) <= ((i + 1) + (j - 1)) - (j - 1) by XREAL_1:9;
i - j < (i - j) + 1 by XREAL_1:29;
then 0 < (i - j) + 1 by A17, XREAL_1:48;
then reconsider ij = (i - j) + 1 as Element of NAT by INT_1:3;
0 <= i - j by A17, XREAL_1:48;
then A19: ( 0 + 1 <= ((i - j) + 1) + 1 & 0 + 1 <= ij ) by XREAL_1:7;
A20: i + 1 <= n2 + 1 by A4, A6, XREAL_1:7;
(i + 1) + 0 <= (i + 1) + j by A16, XREAL_1:7;
then (i + 1) - j <= ((i + 1) + j) - j by XREAL_1:9;
then A21: (i + 1) - j <= n2 + 1 by A20, XXREAL_0:2;
i + 1 <= n2 + 1 by A4, A6, XREAL_1:7;
then (i + 1) - (j - 1) <= n2 + 1 by A18, XXREAL_0:2;
hence ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) by A2, A3, A4, A6, A16, A17, A19, A21, Th7; :: thesis:

end;

i2 + 1 <= n2 + 1 by A4, A6, XREAL_1:7;
then A22: i2 + 1 in Seg (n2 + 1) by A7, FINSEQ_1:1;
i2 in Seg (n2 + 1) by A4, A6, A8, FINSEQ_1:1;
hence ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) by A2, A3, A4, A6, A5, A15, A22, A9, FINSEQ_1:def 3; :: thesis:

end;

hence ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) by A1, A2, A3, Def1; :: thesis: