---

Step * 1 1 2 1 of Lemma l_intersection-size


1. T : Type
2. eq : EqDecider(T)
3. a : T List
4. b : T List
5. c : T List
6. no_repeats(T;a)
7. no_repeats(T;b)
8. a ⊆ c
9. b ⊆ c
10. no_repeats(T;(a ⋂ b))
11. f : ℕ||a|| ⟶ ℕ||c||
12. ∀i:ℕ||a||. (a[i] = c[f i] ∈ T)
13. g : ℕ||b|| ⟶ ℕ||c||
14. ∀i:ℕ||b||. (b[i] = c[g i] ∈ T)
15. Inj({x:T| (x ∈ (a ⋂ b))} ;ℕ||(a ⋂ b)||;λx.index((a ⋂ b);x))
16. ∀j:ℕ||b||. ((b[j] ∈ a) ⇒ ((b[j] ∈ (a ⋂ b)) ∧ (index((a ⋂ b);b[j]) ∈ ℕ||(a ⋂ b)||)))
17. a1 : ℕ||a|| + ||b||
18. a2 : ℕ||a|| + ||b||
⊢ (if a1 <z ||a|| then f a1
if b[a1 - ||a||] ∈b a then ||c|| + index((a ⋂ b);b[a1 - ||a||])
else g (a1 - ||a||)
fi 
= if a2 <z ||a|| then f a2
  if b[a2 - ||a||] ∈b a then ||c|| + index((a ⋂ b);b[a2 - ||a||])
  else g (a2 - ||a||)
  fi 
∈ ℕ||c|| + ||(a ⋂ b)||)
⇒ (a1 = a2 ∈ ℕ||a|| + ||b||)
BY
{ TACTIC:(BoolCase ⌜a1 <z ||a||⌝⋅ THENA Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. a : T List
4. b : T List
5. c : T List
6. no_repeats(T;a)
7. no_repeats(T;b)
8. a ⊆ c
9. b ⊆ c
10. no_repeats(T;(a ⋂ b))
11. f : ℕ||a|| ⟶ ℕ||c||
12. ∀i:ℕ||a||. (a[i] = c[f i] ∈ T)
13. g : ℕ||b|| ⟶ ℕ||c||
14. ∀i:ℕ||b||. (b[i] = c[g i] ∈ T)
15. Inj({x:T| (x ∈ (a ⋂ b))} ;ℕ||(a ⋂ b)||;λx.index((a ⋂ b);x))
16. ∀j:ℕ||b||. ((b[j] ∈ a) ⇒ ((b[j] ∈ (a ⋂ b)) ∧ (index((a ⋂ b);b[j]) ∈ ℕ||(a ⋂ b)||)))
17. a1 : ℕ||a|| + ||b||
18. a2 : ℕ||a|| + ||b||
19. a1 < ||a||
⊢ ((f a1)
= if a2 <z ||a|| then f a2
  if b[a2 - ||a||] ∈b a then ||c|| + index((a ⋂ b);b[a2 - ||a||])
  else g (a2 - ||a||)
  fi 
∈ ℕ||c|| + ||(a ⋂ b)||)
⇒ (a1 = a2 ∈ ℕ||a|| + ||b||)

2
1. T : Type
2. eq : EqDecider(T)
3. a : T List
4. b : T List
5. c : T List
6. no_repeats(T;a)
7. no_repeats(T;b)
8. a ⊆ c
9. b ⊆ c
10. no_repeats(T;(a ⋂ b))
11. f : ℕ||a|| ⟶ ℕ||c||
12. ∀i:ℕ||a||. (a[i] = c[f i] ∈ T)
13. g : ℕ||b|| ⟶ ℕ||c||
14. ∀i:ℕ||b||. (b[i] = c[g i] ∈ T)
15. Inj({x:T| (x ∈ (a ⋂ b))} ;ℕ||(a ⋂ b)||;λx.index((a ⋂ b);x))
16. ∀j:ℕ||b||. ((b[j] ∈ a) ⇒ ((b[j] ∈ (a ⋂ b)) ∧ (index((a ⋂ b);b[j]) ∈ ℕ||(a ⋂ b)||)))
17. a1 : ℕ||a|| + ||b||
18. ¬a1 < ||a||
19. a2 : ℕ||a|| + ||b||
⊢ (if b[a1 - ||a||] ∈b a then ||c|| + index((a ⋂ b);b[a1 - ||a||]) else g (a1 - ||a||) fi 
= if a2 <z ||a|| then f a2
  if b[a2 - ||a||] ∈b a then ||c|| + index((a ⋂ b);b[a2 - ||a||])
  else g (a2 - ||a||)
  fi 
∈ ℕ||c|| + ||(a ⋂ b)||)
⇒ (a1 = a2 ∈ ℕ||a|| + ||b||)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  a  :  T  List
4.  b  :  T  List
5.  c  :  T  List
6.  no\_repeats(T;a)
7.  no\_repeats(T;b)
8.  a  \msubseteq{}  c
9.  b  \msubseteq{}  c
10.  no\_repeats(T;(a  \mcap{}  b))
11.  f  :  \mBbbN{}||a||  {}\mrightarrow{}  \mBbbN{}||c||
12.  \mforall{}i:\mBbbN{}||a||.  (a[i]  =  c[f  i])
13.  g  :  \mBbbN{}||b||  {}\mrightarrow{}  \mBbbN{}||c||
14.  \mforall{}i:\mBbbN{}||b||.  (b[i]  =  c[g  i])
15.  Inj(\{x:T|  (x  \mmember{}  (a  \mcap{}  b))\}  ;\mBbbN{}||(a  \mcap{}  b)||;\mlambda{}x.index((a  \mcap{}  b);x))
16.  \mforall{}j:\mBbbN{}||b||.  ((b[j]  \mmember{}  a)  {}\mRightarrow{}  ((b[j]  \mmember{}  (a  \mcap{}  b))  \mwedge{}  (index((a  \mcap{}  b);b[j])  \mmember{}  \mBbbN{}||(a  \mcap{}  b)||)))
17.  a1  :  \mBbbN{}||a||  +  ||b||
18.  a2  :  \mBbbN{}||a||  +  ||b||
\mvdash{}  (if  a1  <z  ||a||  then  f  a1
if  b[a1  -  ||a||]  \mmember{}\msubb{}  a  then  ||c||  +  index((a  \mcap{}  b);b[a1  -  ||a||])
else  g  (a1  -  ||a||)
fi 
=  if  a2  <z  ||a||  then  f  a2
    if  b[a2  -  ||a||]  \mmember{}\msubb{}  a  then  ||c||  +  index((a  \mcap{}  b);b[a2  -  ||a||])
    else  g  (a2  -  ||a||)
    fi  )
{}\mRightarrow{}  (a1  =  a2)


By

---

Latex:
TACTIC:(BoolCase  \mkleeneopen{}a1  <z  ||a||\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index