(
x.A[(||A||-(x+1))]) 
m
n increasing(x.A[(||A||-(x+1))];m) & (
s:m. G([((x.A[(||A||-(x+1))])(s))]) = c)mn (increasing(f;m) & (s:m. G([(f(s))]) = c)) Prop List
n List)| ||s|| = 1 
& (x,y:||s||. x < y 
s[x] < s[y]) }||L||
||L||
List
||A||
x:||A||. A[x] < n & G([A[x]]) = c
x,y:||A||. x < y A[x] > A[y]
f:(mn). increasing(f;m) & (s:m. G([(f(s))]) = c)
x.A[(||A||-(x+1))]]
| 1 | (x.A[(||A||-(x+1))]) mn | 2 steps |
| 2 | increasing(x.A[(||A||-(x+1))];m) & (s:m. G([((x.A[(||A||-(x+1))])(s))]) = c) | 3 steps |
| 3 | 10. f: mn (increasing(f;m) & (s:m. G([(f(s))]) = c)) Prop | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |