(17steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: trivial-arrows 2
1. k:
2. L: List
3. i: ||L||
4. L[i] < k
5. n:
6. k-1n
7. G: {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||
c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c)
By: ((InstConcl [i;x.x]) THEN (Reduce 0)) THENA (Try (Complete Auto))
Generated subgoals:

1 increasing(x.x;L[i]) & (s:L[i] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(x.x;s)) = i)5 steps
 
28. f: L[i]n
(increasing(f;L[i]) & (s:L[i] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = i)) Prop		1 step
 
38. c: ||L||
(f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c)) Prop		1 step

About:
listintnatural_numbersubtractless_thansetlambda
functionequalmemberpropimpliesandall
exists

(17steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc