PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of nsubn 2 1 2 1 1 2 1 1 2 1 1 2 2 3 3 1 1 1
1. n: {1+1...}
2. E:((n-1)(n-1)Prop). (EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) (m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))
3. E: nnProp
4. EquivRel x,y:n. x E y
5. x,y:n. Dec(x E y)
6. EquivRel x,y:(n-1). x E y
7. m: (n-1+1)
8. f: m(i,j:(n-1)//(i E j))
9. g: (i,j:(n-1)//(i E j))m
10. InvFuns(m; i,j:(n-1)//(i E j); f; g)
11. x:m. f(x) i,j:n//(i E j)
12. a:n. a E a
13. a,b:n. (a E b) (b E a)
14. a,b,c:n. (a E b) (b E c) (a E c)
15. x,y:i,j:n//(i E j). Dec(x = y)
16. Eb: (i,j:n//(i E j))(i,j:n//(i E j))
17. x,y:i,j:n//(i E j). (x Eb y) x = y
18. (k:(n-1). k E (n-1))
19. n-1 i,j:n//(i E j)
20. f1: (m+1)(i,j:n//(i E j))
21. f1 = (x.if x=m n-1 else f(x) fi)
22. g1: (i,j:n//(i E j))(m+1)
23. g1 = (x.if x Eb (n-1) m else g(x) fi)
24. x: (m+1)

if if x=m n-1 else f(x) fi Eb (n-1) m else g(if x=m n-1 else f(x) fi) fi = x (m+1)
By: ((SplitOnNthConclITE 2) THEN SplitOnConclITE) THENA Try (Complete Auto)
Generated subgoals:

125. x = m
26. (n-1) Eb (n-1)
m = x (m+1)
225. x = m
26. ((n-1) Eb (n-1))
g(n-1) = x (m+1)
325. x = m
((f(x)) Eb (n-1))
425. x = m
26. (f(x)) Eb (n-1)
m = x (m+1)
525. x = m
26. ((f(x)) Eb (n-1))
g(f(x)) = x (m+1)

About:
equalnatural_numberaddifthenelsesubtractapply
allfunctionpropimpliesandexists
quotientmemberboolassertlambda