Step
*
1
2
1
of Lemma
append_functionality_wrt_permutation
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
⊢ Inj(ℕ||as1|| + ||as2||;ℕ||as1|| + ||as2||;λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi )
BY
{ ((RepeatFor 2 ((D 0 THENA Auto)) THEN Reduce 0) THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))) }
1
.....truecase.....
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
15. a1 : ℕ||as1|| + ||as2||@i
16. a2 : ℕ||as1|| + ||as2||@i
17. a1 < ||as1||
18. a2 < ||as1||
⊢ ((f1 a1) = (f1 a2) ∈ ℕ||as1|| + ||as2||) ⇒ (a1 = a2 ∈ ℕ||as1|| + ||as2||)
2
.....falsecase.....
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
15. a1 : ℕ||as1|| + ||as2||@i
16. a2 : ℕ||as1|| + ||as2||@i
17. a1 < ||as1||
18. ||as1|| ≤ a2
⊢ ((f1 a1) = (||as1|| + (f (a2 - ||as1||))) ∈ ℕ||as1|| + ||as2||) ⇒ (a1 = a2 ∈ ℕ||as1|| + ||as2||)
3
.....truecase.....
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
15. a1 : ℕ||as1|| + ||as2||@i
16. a2 : ℕ||as1|| + ||as2||@i
17. ||as1|| ≤ a1
18. a2 < ||as1||
⊢ ((||as1|| + (f (a1 - ||as1||))) = (f1 a2) ∈ ℕ||as1|| + ||as2||) ⇒ (a1 = a2 ∈ ℕ||as1|| + ||as2||)
4
.....falsecase.....
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
15. a1 : ℕ||as1|| + ||as2||@i
16. a2 : ℕ||as1|| + ||as2||@i
17. ||as1|| ≤ a1
18. ||as1|| ≤ a2
⊢ ((||as1|| + (f (a1 - ||as1||))) = (||as1|| + (f (a2 - ||as1||))) ∈ ℕ||as1|| + ||as2||)
⇒ (a1 = a2 ∈ ℕ||as1|| + ||as2||)
Latex:
Latex:
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : \mBbbN{}||as1|| {}\mrightarrow{} \mBbbN{}||as1||@i
7. Inj(\mBbbN{}||as1||;\mBbbN{}||as1||;f1)
8. bs1 = (as1 o f1)
9. f : \mBbbN{}||as2|| {}\mrightarrow{} \mBbbN{}||as2||@i
10. Inj(\mBbbN{}||as2||;\mBbbN{}||as2||;f)
11. bs2 = (as2 o f)
12. ||as1|| = ||bs1||
13. ||as2|| = ||bs2||
14. \mlambda{}i.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi \mmember{} \mBbbN{}||as1|| + ||as2||
{}\mrightarrow{} \mBbbN{}||as1|| + ||as2||
\mvdash{} Inj(\mBbbN{}||as1|| + ||as2||;\mBbbN{}||as1|| + ||as2||;\mlambda{}i.if i <z ||as1||
then f1 i
else ||as1|| + (f (i - ||as1||))
fi )
By
Latex:
((RepeatFor 2 ((D 0 THENA Auto)) THEN Reduce 0) THEN RepeatFor 2 ((SplitOnConclITE THENA Auto)))
Home
Index