Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2021 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Mathlib.Tactic.Basic
import Std.Tactic.Simpa
import Mathlib.Data.Array.Basic

structure 
UFModel: {n : โ„•} โ†’ (parent : Fin n โ†’ Fin n) โ†’ (rank : โ„• โ†’ โ„•) โ†’ (โˆ€ (i : Fin n), โ†‘(parent i) โ‰  โ†‘i โ†’ rank โ†‘i < rank โ†‘(parent i)) โ†’ UFModel n
UFModel
(
n: ?m.2
n
) where
parent: {n : โ„•} โ†’ UFModel n โ†’ Fin n โ†’ Fin n
parent
:
Fin: โ„• โ†’ Type
Fin
n: ?m.2
n
โ†’
Fin: โ„• โ†’ Type
Fin
n: ?m.2
n
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
:
Nat: Type
Nat
โ†’
Nat: Type
Nat
rank_lt: โˆ€ {n : โ„•} (self : UFModel n) (i : Fin n), โ†‘(UFModel.parent self i) โ‰  โ†‘i โ†’ UFModel.rank self โ†‘i < UFModel.rank self โ†‘(UFModel.parent self i)
rank_lt
: โˆ€
i: ?m.16
i
, (
parent: Fin n โ†’ Fin n
parent
i: ?m.16
i
).
1: {n : โ„•} โ†’ Fin n โ†’ โ„•
1
โ‰ 
i: ?m.16
i
โ†’
rank: โ„• โ†’ โ„•
rank
i: ?m.16
i
<
rank: โ„• โ†’ โ„•
rank
(
parent: Fin n โ†’ Fin n
parent
i: ?m.16
i
) namespace UFModel def
empty: UFModel 0
empty
:
UFModel: โ„• โ†’ Type
UFModel
0: ?m.629
0
where parent
i: ?m.643
i
:=
i: ?m.643
i
.
elim0: {ฮฑ : Sort ?u.645} โ†’ Fin 0 โ†’ ฮฑ
elim0
rank
_: ?m.653
_
:=
0: ?m.656
0
rank_lt
i: ?m.660
i
:=
i: ?m.660
i
.
elim0: โˆ€ {ฮฑ : Sort ?u.662}, Fin 0 โ†’ ฮฑ
elim0
def
push: {n : โ„•} โ†’ UFModel n โ†’ (k : โ„•) โ†’ n โ‰ค k โ†’ UFModel k
push
{
n: ?m.770
n
} (
m: UFModel n
m
:
UFModel: โ„• โ†’ Type
UFModel
n: ?m.770
n
) (k) (
le: n โ‰ค k
le
:
n: ?m.770
n
โ‰ค
k: ?m.775
k
) :
UFModel: โ„• โ†’ Type
UFModel
k: ?m.775
k
where parent
i: ?m.794
i
:= if
h: ?m.2016
h
:
i: ?m.794
i
< n then let โŸจa,
h': a < n
h'
โŸฉ :=
m: UFModel n
m
.
parent: {n : โ„•} โ†’ UFModel n โ†’ Fin n โ†’ Fin n
parent
โŸจ
i: ?m.794
i
,
h: ?m.1857
h
โŸฉ โŸจa,
lt_of_lt_of_le: โˆ€ {ฮฑ : Type ?u.1888} [inst : Preorder ฮฑ] {a b c : ฮฑ}, a < b โ†’ b โ‰ค c โ†’ a < c
lt_of_lt_of_le
h': a < n
h'
le: n โ‰ค k
le
โŸฉ else
i: ?m.794
i
rank
i: ?m.2025
i
:= if
i: ?m.2025
i
< n then
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
i: ?m.2025
i
else
0: ?m.2051
0
rank_lt
i: ?m.2063
i
:=

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i) โ‰  โ†‘i โ†’ (fun i => if i < n then rank m i else 0) โ†‘i < (fun i => if i < n then rank m i else 0) โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i)
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


ยฌโ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) = โ†‘i โ†’ (if โ†‘i < n then rank m โ†‘i else 0) < if โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) < n then rank m โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


ยฌโ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) = โ†‘i โ†’ (if โ†‘i < n then rank m โ†‘i else 0) < if โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) < n then rank m โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i) โ‰  โ†‘i โ†’ (fun i => if i < n then rank m i else 0) โ†‘i < (fun i => if i < n then rank m i else 0) โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i)
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

hโœ: โ†‘i < n


inl
ยฌโ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } = โ†‘i โ†’ rank m โ†‘i < if โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } < n then rank m โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

hโœ: ยฌโ†‘i < n


inr
ยฌโ†‘i = โ†‘i โ†’ 0 < 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


ยฌโ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) = โ†‘i โ†’ (if โ†‘i < n then rank m โ†‘i else 0) < if โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) < n then rank m โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

hโœ: โ†‘i < n


inl
ยฌโ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } = โ†‘i โ†’ rank m โ†‘i < if โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } < n then rank m โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

hโœ: ยฌโ†‘i < n


inr
ยฌโ†‘i = โ†‘i โ†’ 0 < 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


ยฌโ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) = โ†‘i โ†’ (if โ†‘i < n then rank m โ†‘i else 0) < if โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) < n then rank m โ†‘(if h : โ†‘i < n then { val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else i) else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: ยฌโ†‘i < n


inr
ยฌโ†‘i = โ†‘i โ†’ 0 < 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i) โ‰  โ†‘i โ†’ (fun i => if i < n then rank m i else 0) โ†‘i < (fun i => if i < n then rank m i else 0) โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i)
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: โ†‘i < n


inl
ยฌโ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } = โ†‘i โ†’ rank m โ†‘i < if โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } < n then rank m โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: โ†‘i < n


inl
ยฌโ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } = โ†‘i โ†’ rank m โ†‘i < if โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } < n then rank m โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: ยฌโ†‘i < n


inr
ยฌโ†‘i = โ†‘i โ†’ 0 < 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: โ†‘i < n


inl
ยฌโ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) })
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: โ†‘i < n


inl
ยฌโ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) })
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: โ†‘i < n


inl
ยฌโ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } = โ†‘i โ†’ rank m โ†‘i < if โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } < n then rank m โ†‘{ val := โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }), isLt := (_ : โ†‘(m.1 { val := โ†‘i, isLt := (_ : โ†‘i < n) }) < k) } else 0

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k


โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i) โ‰  โ†‘i โ†’ (fun i => if i < n then rank m i else 0) โ†‘i < (fun i => if i < n then rank m i else 0) โ†‘((fun i => if h : โ†‘i < n then match parent m { val := โ†‘i, isLt := h } with | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) } else i) i)
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: ยฌโ†‘i < n


inr
ยฌโ†‘i = โ†‘i โ†’ 0 < 0
n: โ„•

m: UFModel n

k: โ„•

le: n โ‰ค k

i: Fin k

h: ยฌโ†‘i < n


inr
ยฌโ†‘i = โ†‘i โ†’ 0 < 0

Goals accomplished! ๐Ÿ™
def
setParent: {n : โ„•} โ†’ (m : UFModel n) โ†’ (x y : Fin n) โ†’ rank m โ†‘x < rank m โ†‘y โ†’ UFModel n
setParent
{
n: ?m.5711
n
} (
m: UFModel n
m
:
UFModel: โ„• โ†’ Type
UFModel
n: ?m.5711
n
) (
x: Fin n
x
y: Fin n
y
:
Fin: โ„• โ†’ Type
Fin
n: ?m.5711
n
) (
h: rank m โ†‘x < rank m โ†‘y
h
:
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
x: Fin n
x
<
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
y: Fin n
y
) :
UFModel: โ„• โ†’ Type
UFModel
n: ?m.5711
n
where parent
i: ?m.5925
i
:= if
x: Fin n
x
.
1: {n : โ„•} โ†’ Fin n โ†’ โ„•
1
=
i: ?m.5925
i
then
y: Fin n
y
else
m: UFModel n
m
.
parent: {n : โ„•} โ†’ UFModel n โ†’ Fin n โ†’ Fin n
parent
i: ?m.5925
i
rank :=
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
rank_lt
i: ?m.6116
i
:=

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ rank m โ†‘i < rank m โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ rank m โ†‘i < rank m โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

hโœ: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

hโœ: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

hโœ: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

hโœ: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ rank m โ†‘i < rank m โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘x โ†’ rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘x โ†’ rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘x โ†’ rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘y

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ rank m โ†‘i < rank m โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

h: rank m โ†‘x < rank m โ†‘y

i: Fin n

h': ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < rank m โ†‘(parent m i)

Goals accomplished! ๐Ÿ™
def
setParentBump: {n : โ„•} โ†’ (m : UFModel n) โ†’ (x y : Fin n) โ†’ rank m โ†‘x โ‰ค rank m โ†‘y โ†’ โ†‘(parent m y) = โ†‘y โ†’ UFModel n
setParentBump
{
n: ?m.7367
n
} (
m: UFModel n
m
:
UFModel: โ„• โ†’ Type
UFModel
n: ?m.7367
n
) (
x: Fin n
x
y: Fin n
y
:
Fin: โ„• โ†’ Type
Fin
n: ?m.7367
n
) (
H: rank m โ†‘x โ‰ค rank m โ†‘y
H
:
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
x: Fin n
x
โ‰ค
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
y: Fin n
y
) (
hroot: โ†‘(parent m y) = โ†‘y
hroot
: (
m: UFModel n
m
.
parent: {n : โ„•} โ†’ UFModel n โ†’ Fin n โ†’ Fin n
parent
y: Fin n
y
).
1: {n : โ„•} โ†’ Fin n โ†’ โ„•
1
=
y: Fin n
y
) :
UFModel: โ„• โ†’ Type
UFModel
n: ?m.7367
n
where parent
i: ?m.7672
i
:= if
x: Fin n
x
.
1: {n : โ„•} โ†’ Fin n โ†’ โ„•
1
=
i: ?m.7672
i
then
y: Fin n
y
else
m: UFModel n
m
.
parent: {n : โ„•} โ†’ UFModel n โ†’ Fin n โ†’ Fin n
parent
i: ?m.7672
i
rank
i: ?m.7860
i
:= if
y: Fin n
y
.
1: {n : โ„•} โ†’ Fin n โ†’ โ„•
1
=
i: ?m.7860
i
โˆง
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
x: Fin n
x
=
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
y: Fin n
y
then
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
y: Fin n
y
+
1: ?m.8057
1
else
m: UFModel n
m
.
rank: {n : โ„•} โ†’ UFModel n โ†’ โ„• โ†’ โ„•
rank
i: ?m.7860
i
rank_lt
i: ?m.8113
i
:=

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘i < (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(if โ†‘x = โ†‘i then y else parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(if โ†‘x = โ†‘i then y else parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘i < (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘y โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(if โ†‘x = โ†‘i then y else parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘y โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


ยฌโ†‘(if โ†‘x = โ†‘i then y else parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(if โ†‘x = โ†‘i then y else parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(if โ†‘x = โ†‘i then y else parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘y โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโœ: โ†‘x = โ†‘i


inl
ยฌโ†‘y = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘y โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโœ: โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y


inl.inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘y + 1 < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโœ: ยฌ(โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y)


inl.inr
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโœ: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y


inr.inl
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘y + 1 < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโœ: ยฌ(โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y


inl.inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘y + 1 < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y


inl.inl
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘y + 1 < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโ‚‚: ยฌ(โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y)


inl.inr
ยฌโ†‘y = โ†‘i โ†’ rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i


inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ (if โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘i) < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y


inr.inl
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘y + 1 < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: ยฌ(โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y)

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘y + 1 < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: ยฌ(โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr
ยฌโ†‘(parent m i) = โ†‘i โ†’ rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y

h: ยฌโ†‘y = โ†‘i


inl.inl
rank m โ†‘y + 1 < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘i = rank m โ†‘y

h: ยฌโ†‘y = โ†‘i


inl.inl
rank m โ†‘y + 1 < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘i < (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘x < if rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘x < if rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโœ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘x < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโœ: ยฌrank m โ†‘x = rank m โ†‘y


inl.inr.inr
rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘x < if rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโœ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘x < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโœ: ยฌrank m โ†‘x = rank m โ†‘y


inl.inr.inr
rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘x < if rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: ยฌrank m โ†‘x = rank m โ†‘y


inl.inr.inr
rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘x < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘x < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: ยฌrank m โ†‘x = rank m โ†‘y


inl.inr.inr
rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘x < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘y < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘y < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘y < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: rank m โ†‘x = rank m โ†‘y


inl.inr.inl
rank m โ†‘x < rank m โ†‘y + 1

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True


inl.inr
rank m โ†‘i < if rank m โ†‘i = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: ยฌrank m โ†‘x = rank m โ†‘y


inl.inr.inr
rank m โ†‘x < rank m โ†‘y
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: โ†‘x = โ†‘i

h: ยฌโ†‘y = โ†‘i

hโ‚‚: True

hโ‚ƒ: ยฌrank m โ†‘x = rank m โ†‘y


inl.inr.inr
rank m โ†‘x < rank m โ†‘y

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘i < (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i

this: y = i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i

this: y = i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

hโ‚: ยฌโ†‘x = โ†‘y

hโ‚‚: โ†‘y = โ†‘y โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m y) = โ†‘y


inr.inl
rank m โ†‘y + 1 < if โ†‘y = โ†‘(parent m y) then rank m โ†‘y + 1 else rank m โ†‘(parent m y)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โˆง rank m โ†‘x = rank m โ†‘y

h: ยฌโ†‘(parent m i) = โ†‘i


inr.inl
rank m โ†‘i + 1 < if โ†‘i = โ†‘(parent m i) then rank m โ†‘i + 1 else rank m โ†‘(parent m i)

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n


โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i) โ‰  โ†‘i โ†’ (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘i < (fun i => if โ†‘y = i โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m i) โ†‘((fun i => if โ†‘x = โ†‘i then y else parent m i) i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโœ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโœ: ยฌ(โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr.inr
rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโœ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโœ: ยฌ(โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr.inr
rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: ยฌ(โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr.inr
rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘(parent m i) + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘(parent m i) + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘(parent m i) + 1
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y


inr.inr.inl
rank m โ†‘i < rank m โ†‘y + 1

Goals accomplished! ๐Ÿ™
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y


inr.inr
rank m โ†‘i < if โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y then rank m โ†‘y + 1 else rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: ยฌ(โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr.inr
rank m โ†‘i < rank m โ†‘(parent m i)
n: โ„•

m: UFModel n

x, y: Fin n

H: rank m โ†‘x โ‰ค rank m โ†‘y

hroot: โ†‘(parent m y) = โ†‘y

i: Fin n

hโ‚: ยฌโ†‘x = โ†‘i

h: ยฌโ†‘(parent m i) = โ†‘i

hโ‚‚: โ†‘y = โ†‘i โ†’ ยฌrank m โ†‘x = rank m โ†‘y

this: rank m โ†‘i < rank m โ†‘(parent m i)

hโ‚ƒ: ยฌ(โ†‘y = โ†‘(parent m i) โˆง rank m โ†‘x = rank m โ†‘y)


inr.inr.inr
rank m โ†‘i < rank m โ†‘(parent m i)

Goals accomplished! ๐Ÿ™
end UFModel structure
UFNode: {ฮฑ : Type u_1} โ†’ โ„• โ†’ ฮฑ โ†’ โ„• โ†’ UFNode ฮฑ
UFNode
(
ฮฑ: Type ?u.14762
ฮฑ
:
Type _: Type (?u.14762+1)
Type _
) where
parent: {ฮฑ : Type u_1} โ†’ UFNode ฮฑ โ†’ โ„•
parent
:
Nat: Type
Nat
value: {ฮฑ : Type u_1} โ†’ UFNode ฮฑ โ†’ ฮฑ
value
:
ฮฑ: Type ?u.14762
ฮฑ
rank: {ฮฑ : Type u_1} โ†’ UFNode ฮฑ โ†’ โ„•
rank
:
Nat: Type
Nat
inductive
UFModel.Agrees: {ฮฑ : Type u_1} โ†’ {ฮฒ : Sort u_2} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
UFModel.Agrees
(
arr: Array ฮฑ
arr
:
Array: Type ?u.15274 โ†’ Type ?u.15274
Array
ฮฑ: ?m.15271
ฮฑ
) (
f: ฮฑ โ†’ ฮฒ
f
:
ฮฑ: ?m.15271
ฮฑ
โ†’
ฮฒ: ?m.15280
ฮฒ
) : โˆ€ {
n: ?m.15291
n
}, (
Fin: โ„• โ†’ Type
Fin
n: ?m.15291
n
โ†’
ฮฒ: ?m.15280
ฮฒ
) โ†’
Prop: Type
Prop
|
mk: โˆ€ {ฮฑ : Type u_1} {ฮฒ : Sort u_2} {arr : Array ฮฑ} {f : ฮฑ โ†’ ฮฒ}, Agrees arr f fun i => f (Array.get arr i)
mk
:
Agrees: {ฮฑ : Type ?u.15283} โ†’ {ฮฒ : Sort ?u.15287} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
arr: Array ฮฑ
arr
f: ฮฑ โ†’ ฮฒ
f
fun
i: ?m.15314
i
โ†ฆ
f: ฮฑ โ†’ ฮฒ
f
(
arr: Array ฮฑ
arr
.
get: {ฮฑ : Type ?u.15316} โ†’ (a : Array ฮฑ) โ†’ Fin (Array.size a) โ†’ ฮฑ
get
i: ?m.15314
i
) namespace UFModel.Agrees theorem
mk': โˆ€ {ฮฑ : Type u_1} {ฮฒ : Sort u_2} {arr : Array ฮฑ} {f : ฮฑ โ†’ ฮฒ} {n : โ„•} {g : Fin n โ†’ ฮฒ}, n = Array.size arr โ†’ (โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }) โ†’ Agrees arr f g
mk'
{
arr: Array ฮฑ
arr
:
Array: Type ?u.15374 โ†’ Type ?u.15374
Array
ฮฑ: ?m.15371
ฮฑ
} {
f: ฮฑ โ†’ ฮฒ
f
:
ฮฑ: ?m.15371
ฮฑ
โ†’
ฮฒ: ?m.15380
ฮฒ
} {n} {
g: Fin n โ†’ ฮฒ
g
:
Fin: โ„• โ†’ Type
Fin
n: ?m.15390
n
โ†’
ฮฒ: ?m.15380
ฮฒ
} (
e: n = Array.size arr
e
:
n: ?m.15390
n
=
arr: Array ฮฑ
arr
.
size: {ฮฑ : Type ?u.15398} โ†’ Array ฮฑ โ†’ โ„•
size
) (
H: โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }
H
: โˆ€
i: ?m.15407
i
hโ‚: ?m.15410
hโ‚
hโ‚‚: ?m.15413
hโ‚‚
,
f: ฮฑ โ†’ ฮฒ
f
(
arr: Array ฮฑ
arr
.
get: {ฮฑ : Type ?u.15417} โ†’ (a : Array ฮฑ) โ†’ Fin (Array.size a) โ†’ ฮฑ
get
โŸจ
i: ?m.15407
i
,
hโ‚: ?m.15410
hโ‚
โŸฉ) =
g: Fin n โ†’ ฮฒ
g
โŸจ
i: ?m.15407
i
,
hโ‚‚: ?m.15413
hโ‚‚
โŸฉ) :
Agrees: {ฮฑ : Type ?u.15435} โ†’ {ฮฒ : Sort ?u.15434} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
arr: Array ฮฑ
arr
f: ฮฑ โ†’ ฮฒ
f
g: Fin n โ†’ ฮฒ
g
:=

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

n: โ„•

g: Fin n โ†’ ฮฒ

e: n = Array.size arr

H: โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


Agrees arr f g
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

g: Fin (Array.size arr) โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


refl
Agrees arr f g
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

n: โ„•

g: Fin n โ†’ ฮฒ

e: n = Array.size arr

H: โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


Agrees arr f g
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

g: Fin (Array.size arr) โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


refl
Agrees arr f g

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

g: Fin (Array.size arr) โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


(fun i => f (Array.get arr i)) = g
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

g: Fin (Array.size arr) โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }

i: โ„•

h: i < Array.size arr


h
f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h }
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

g: Fin (Array.size arr) โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }

i: โ„•

h: i < Array.size arr


h
f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h }
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

g: Fin (Array.size arr) โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


(fun i => f (Array.get arr i)) = g

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

n: โ„•

g: Fin n โ†’ ฮฒ

e: n = Array.size arr

H: โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


Agrees arr f g
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = (fun i => f (Array.get arr i)) { val := i, isLt := hโ‚‚ }


refl.refl
Agrees arr f fun i => f (Array.get arr i)
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

H: โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = (fun i => f (Array.get arr i)) { val := i, isLt := hโ‚‚ }


refl.refl
Agrees arr f fun i => f (Array.get arr i)
ฮฑ: Type u_1

ฮฒ: Sort u_2

arr: Array ฮฑ

f: ฮฑ โ†’ ฮฒ

n: โ„•

g: Fin n โ†’ ฮฒ

e: n = Array.size arr

H: โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }


Agrees arr f g

Goals accomplished! ๐Ÿ™
theorem
size_eq: โˆ€ {ฮฑ : Type u_1} {n : โ„•} {ฮฒ : Sort u_2} {f : ฮฑ โ†’ ฮฒ} {arr : Array ฮฑ} {m : Fin n โ†’ ฮฒ}, Agrees arr f m โ†’ n = Array.size arr
size_eq
{
arr: Array ฮฑ
arr
:
Array: Type ?u.15905 โ†’ Type ?u.15905
Array
ฮฑ: ?m.15868
ฮฑ
} {
m: Fin n โ†’ ฮฒ
m
:
Fin: โ„• โ†’ Type
Fin
n: ?m.15876
n
โ†’
ฮฒ: ?m.15885
ฮฒ
} (
H: Agrees arr f m
H
:
Agrees: {ฮฑ : Type ?u.15913} โ†’ {ฮฒ : Sort ?u.15912} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
arr: Array ฮฑ
arr
f: ?m.15902
f
m: Fin n โ†’ ฮฒ
m
) :
n: ?m.15876
n
=
arr: Array ฮฑ
arr
.
size: {ฮฑ : Type ?u.15929} โ†’ Array ฮฑ โ†’ โ„•
size
:=

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

n: โ„•

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

m: Fin n โ†’ ฮฒ

H: Agrees arr f m


ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ


mk
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ


mk
ฮฑ: Type u_1

n: โ„•

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

m: Fin n โ†’ ฮฒ

H: Agrees arr f m



Goals accomplished! ๐Ÿ™
theorem
get_eq: โˆ€ {ฮฑ : Type u_1} {ฮฒ : Sort u_2} {f : ฮฑ โ†’ ฮฒ} {arr : Array ฮฑ} {n : โ„•} {m : Fin n โ†’ ฮฒ}, Agrees arr f m โ†’ โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = m { val := i, isLt := hโ‚‚ }
get_eq
{
arr: Array ฮฑ
arr
:
Array: Type ?u.16159 โ†’ Type ?u.16159
Array
ฮฑ: ?m.16124
ฮฑ
} {n} {
m: Fin n โ†’ ฮฒ
m
:
Fin: โ„• โ†’ Type
Fin
n: ?m.16162
n
โ†’
ฮฒ: ?m.16136
ฮฒ
} (
H: Agrees arr f m
H
:
Agrees: {ฮฑ : Type ?u.16170} โ†’ {ฮฒ : Sort ?u.16169} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
arr: Array ฮฑ
arr
f: ?m.16156
f
m: Fin n โ†’ ฮฒ
m
) : โˆ€
i: ?m.16186
i
hโ‚: ?m.16189
hโ‚
hโ‚‚: ?m.16192
hโ‚‚
,
f: ?m.16156
f
(
arr: Array ฮฑ
arr
.
get: {ฮฑ : Type ?u.16196} โ†’ (a : Array ฮฑ) โ†’ Fin (Array.size a) โ†’ ฮฑ
get
โŸจ
i: ?m.16186
i
,
hโ‚: ?m.16189
hโ‚
โŸฉ) =
m: Fin n โ†’ ฮฒ
m
โŸจ
i: ?m.16186
i
,
hโ‚‚: ?m.16192
hโ‚‚
โŸฉ :=

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m


โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = m { val := i, isLt := hโ‚‚ }
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ


mk
โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = (fun i => f (Array.get arr i)) { val := i, isLt := hโ‚‚ }
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ


mk
โˆ€ (i : โ„•) (hโ‚ hโ‚‚ : i < Array.size arr), f (Array.get arr { val := i, isLt := hโ‚ }) = (fun i => f (Array.get arr i)) { val := i, isLt := hโ‚‚ }
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m


โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = m { val := i, isLt := hโ‚‚ }

Goals accomplished! ๐Ÿ™
theorem
get_eq': โˆ€ {ฮฑ : Type u_1} {ฮฒ : Sort u_2} {f : ฮฑ โ†’ ฮฒ} {arr : Array ฮฑ} {m : Fin (Array.size arr) โ†’ ฮฒ}, Agrees arr f m โ†’ โˆ€ (i : Fin (Array.size arr)), f (Array.get arr i) = m i
get_eq'
{
arr: Array ฮฑ
arr
:
Array: Type ?u.16468 โ†’ Type ?u.16468
Array
ฮฑ: ?m.16451
ฮฑ
} {
m: Fin (Array.size arr) โ†’ ฮฒ
m
:
Fin: โ„• โ†’ Type
Fin
arr: Array ฮฑ
arr
.
size: {ฮฑ : Type ?u.16493} โ†’ Array ฮฑ โ†’ โ„•
size
โ†’
ฮฒ: ?m.16465
ฮฒ
} (
H: Agrees arr f m
H
:
Agrees: {ฮฑ : Type ?u.16502} โ†’ {ฮฒ : Sort ?u.16501} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
arr: Array ฮฑ
arr
f: ?m.16486
f
m: Fin (Array.size arr) โ†’ ฮฒ
m
) (
i: ?m.16516
i
) :
f: ?m.16486
f
(
arr: Array ฮฑ
arr
.
get: {ฮฑ : Type ?u.16520} โ†’ (a : Array ฮฑ) โ†’ Fin (Array.size a) โ†’ ฮฑ
get
i: ?m.16516
i
) =
m: Fin (Array.size arr) โ†’ ฮฒ
m
i: ?m.16516
i
:=
H: Agrees arr f m
H
.
get_eq: โˆ€ {ฮฑ : Type ?u.16534} {ฮฒ : Sort ?u.16535} {f : ฮฑ โ†’ ฮฒ} {arr : Array ฮฑ} {n : โ„•} {m : Fin n โ†’ ฮฒ}, Agrees arr f m โ†’ โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = m { val := i, isLt := hโ‚‚ }
get_eq
.. theorem
empty: โˆ€ {ฮฑ : Type u_1} {ฮฒ : Sort u_2} {f : ฮฑ โ†’ ฮฒ} {g : Fin 0 โ†’ ฮฒ}, Agrees #[] f g
empty
{
f: ฮฑ โ†’ ฮฒ
f
:
ฮฑ: ?m.16586
ฮฑ
โ†’
ฮฒ: ?m.16592
ฮฒ
} {
g: Fin 0 โ†’ ฮฒ
g
:
Fin: โ„• โ†’ Type
Fin
0: ?m.16601
0
โ†’
ฮฒ: ?m.16592
ฮฒ
} :
Agrees: {ฮฑ : Type ?u.16615} โ†’ {ฮฒ : Sort ?u.16614} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
#[]: Array ?m.16619
#[]
f: ฮฑ โ†’ ฮฒ
f
g: Fin 0 โ†’ ฮฒ
g
:=
mk': โˆ€ {ฮฑ : Type ?u.16639} {ฮฒ : Sort ?u.16640} {arr : Array ฮฑ} {f : ฮฑ โ†’ ฮฒ} {n : โ„•} {g : Fin n โ†’ ฮฒ}, n = Array.size arr โ†’ (โˆ€ (i : โ„•) (hโ‚ : i < Array.size arr) (hโ‚‚ : i < n), f (Array.get arr { val := i, isLt := hโ‚ }) = g { val := i, isLt := hโ‚‚ }) โ†’ Agrees arr f g
mk'
rfl: โˆ€ {ฮฑ : Sort ?u.16658} {a : ฮฑ}, a = a
rfl
ฮป.: โˆ€ (a : โ„•) (a_1 : a < Array.size #[]) (a_2 : a < 0), f (Array.get #[] { val := a, isLt := a_1 }) = g { val := a, isLt := a_2 }
ฮป.
theorem
push: โˆ€ {ฮฑ : Type u_1} {ฮฒ : Sort u_2} {f : ฮฑ โ†’ ฮฒ} {arr : Array ฮฑ} {n : โ„•} {m : Fin n โ†’ ฮฒ}, Agrees arr f m โ†’ โˆ€ (k : โ„•), k = n + 1 โ†’ โˆ€ (x : ฮฑ) (m' : Fin k โ†’ ฮฒ), (โˆ€ (i : Fin k) (h : โ†‘i < n), m' i = m { val := โ†‘i, isLt := h }) โ†’ (โˆ€ (h : n < k), f x = m' { val := n, isLt := h }) โ†’ Agrees (Array.push arr x) f m'
push
{
arr: Array ฮฑ
arr
:
Array: Type ?u.16963 โ†’ Type ?u.16963
Array
ฮฑ: ?m.16928
ฮฑ
} {n} {
m: Fin n โ†’ ฮฒ
m
:
Fin: โ„• โ†’ Type
Fin
n: ?m.16966
n
โ†’
ฮฒ: ?m.16940
ฮฒ
} (
H: Agrees arr f m
H
:
Agrees: {ฮฑ : Type ?u.16974} โ†’ {ฮฒ : Sort ?u.16973} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
arr: Array ฮฑ
arr
f: ?m.16960
f
m: Fin n โ†’ ฮฒ
m
) (k) (
hk: k = n + 1
hk
:
k: ?m.16989
k
=
n: ?m.16966
n
+
1: ?m.16997
1
) (
x: ฮฑ
x
) (
m': Fin k โ†’ ฮฒ
m'
:
Fin: โ„• โ†’ Type
Fin
k: ?m.16989
k
โ†’
ฮฒ: ?m.16940
ฮฒ
) (
hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < n), m' i = m { val := โ†‘i, isLt := h }
hmโ‚
: โˆ€ (
i: Fin k
i
:
Fin: โ„• โ†’ Type
Fin
k: ?m.16989
k
) (
h: โ†‘i < n
h
:
i: Fin k
i
<
n: ?m.16966
n
),
m': Fin k โ†’ ฮฒ
m'
i: Fin k
i
=
m: Fin n โ†’ ฮฒ
m
โŸจ
i: Fin k
i
,
h: โ†‘i < n
h
โŸฉ) (
hmโ‚‚: โˆ€ (h : n < k), f x = m' { val := n, isLt := h }
hmโ‚‚
: โˆ€ (
h: n < k
h
:
n: ?m.16966
n
<
k: ?m.16989
k
),
f: ?m.16960
f
x: ?m.17060
x
=
m': Fin k โ†’ ฮฒ
m'
โŸจ
n: ?m.16966
n
,
h: n < k
h
โŸฉ) :
Agrees: {ฮฑ : Type ?u.18140} โ†’ {ฮฒ : Sort ?u.18139} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ ฮฒ) โ†’ {n : โ„•} โ†’ (Fin n โ†’ ฮฒ) โ†’ Prop
Agrees
(
arr: Array ฮฑ
arr
.
push: {ฮฑ : Type ?u.18143} โ†’ Array ฮฑ โ†’ ฮฑ โ†’ Array ฮฑ
push
x: ?m.17060
x
)
f: ?m.16960
f
m': Fin k โ†’ ฮฒ
m'
:=

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m

k: โ„•

hk: k = n + 1

x: ฮฑ

m': Fin k โ†’ ฮฒ

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < n), m' i = m { val := โ†‘i, isLt := h }

hmโ‚‚: โˆ€ (h : n < k), f x = m' { val := n, isLt := h }


Agrees (Array.push arr x) f m'
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

k: โ„•

x: ฮฑ

m': Fin k โ†’ ฮฒ

hk: k = Array.size arr + 1

hmโ‚‚: โˆ€ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := โ†‘i, isLt := h }


mk
Agrees (Array.push arr x) f m'
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m

k: โ„•

hk: k = n + 1

x: ฮฑ

m': Fin k โ†’ ฮฒ

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < n), m' i = m { val := โ†‘i, isLt := h }

hmโ‚‚: โˆ€ (h : n < k), f x = m' { val := n, isLt := h }


Agrees (Array.push arr x) f m'
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

k: โ„•

x: ฮฑ

m': Fin k โ†’ ฮฒ

hk: k = Array.size arr + 1

hmโ‚‚: โˆ€ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := โ†‘i, isLt := h }


mk
Agrees (Array.push arr x) f m'

Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

k: โ„•

x: ฮฑ

m': Fin k โ†’ ฮฒ

hk: k = Array.size arr + 1

hmโ‚‚: โˆ€ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := โ†‘i, isLt := h }



Goals accomplished! ๐Ÿ™
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m

k: โ„•

hk: k = n + 1

x: ฮฑ

m': Fin k โ†’ ฮฒ

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < n), m' i = m { val := โ†‘i, isLt := h }

hmโ‚‚: โˆ€ (h : n < k), f x = m' { val := n, isLt := h }


Agrees (Array.push arr x) f m'
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

k: โ„•

x: ฮฑ

m': Fin k โ†’ ฮฒ

hk: k = Array.size arr + 1

hmโ‚‚: โˆ€ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := โ†‘i, isLt := h }

this: k = Array.size (Array.push arr x)

i: โ„•

hโ‚: i < Array.size (Array.push arr x)

hโ‚‚: i < k


mk
f (Array.get (Array.push arr x) { val := i, isLt := hโ‚ }) = m' { val := i, isLt := hโ‚‚ }
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m

k: โ„•

hk: k = n + 1

x: ฮฑ

m': Fin k โ†’ ฮฒ

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < n), m' i = m { val := โ†‘i, isLt := h }

hmโ‚‚: โˆ€ (h : n < k), f x = m' { val := n, isLt := h }


Agrees (Array.push arr x) f m'
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

k: โ„•

x: ฮฑ

m': Fin k โ†’ ฮฒ

hk: k = Array.size arr + 1

hmโ‚‚: โˆ€ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := โ†‘i, isLt := h }

this: k = Array.size (Array.push arr x)

i: โ„•

hโ‚: i < Array.size (Array.push arr x)

hโ‚‚: i < k


mk
f (if h : i < Array.size arr then arr[i] else x) = m' { val := i, isLt := hโ‚‚ }
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

k: โ„•

x: ฮฑ

m': Fin k โ†’ ฮฒ

hk: k = Array.size arr + 1

hmโ‚‚: โˆ€ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hmโ‚: โˆ€ (i : Fin k) (h : โ†‘i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := โ†‘i, isLt := h }

this: k = Array.size (Array.push arr x)

i: โ„•

hโ‚: i < Array.size (Array.push arr x)

hโ‚‚: i < k


mk
f (if h : i < Array.size arr then arr[i] else x) = m' { val := i, isLt := hโ‚‚ }
ฮฑ: Type u_1

ฮฒ: Sort u_2

f: ฮฑ โ†’ ฮฒ

arr: Array ฮฑ

n: โ„•

m: Fin n โ†’ ฮฒ

H: Agrees arr f m

k: โ„•

hk: k = n + 1

x: ฮฑ

m': Fin k โ†’ ฮฒ

hmโ‚: โˆ€ (i : Fin <