Definition: seq-single
seq-single(t) == λi.if i=0 then t else ⊥
Lemma: seq-single_wf
∀[T:Type]. ∀[t:T]. (seq-single(t) ∈ ℕ1 ⟶ T)
Definition: seq-append
seq-append(n;m;s1;s2) == λi.if (i) < (n) then s1 i else if (i) < (n + m) then s2 (i - n) else ⊥
Lemma: seq-append_wf
∀[T:Type]. ∀[n,m:ℕ]. ∀[s1:ℕn ⟶ T]. ∀[s2:ℕm ⟶ T]. (seq-append(n;m;s1;s2) ∈ ℕn + m ⟶ T)
Definition: seq-add
s.x@n == λm.if m=n then x else (s m)
Lemma: seq-add_wf
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[x:T]. (s.x@n ∈ ℕn + 1 ⟶ T)
Definition: strictly-increasing-seq
strictly-increasing-seq(n;s) == ∀j:ℕn. ∀i:ℕj. s i < s j
Lemma: strictly-increasing-seq_wf
∀[n:ℕ]. ∀[s:ℕn ⟶ ℤ]. (strictly-increasing-seq(n;s) ∈ ℙ)
Lemma: decidable__strictly-increasing-seq
∀n:ℕ. ∀s:ℕn ⟶ ℤ. Dec(strictly-increasing-seq(n;s))
Lemma: implies-strictly-increasing-seq
∀[n:ℕ]. ∀[s:ℕn ⟶ ℤ]. ((∀i:ℕn - 1. s i < s (i + 1)) ⇒ strictly-increasing-seq(n;s))
Lemma: strictly-increasing-seq-add
∀[n:ℕ]. ∀[s:ℕn ⟶ ℤ].
∀x,y:ℕ. (x < y ⇒ strictly-increasing-seq(n + 1;s.x@n) ⇒ strictly-increasing-seq(n + 2;s.x@n.y@n + 1))
Lemma: strictly-increasing-seq-add2-implies
∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀x,y:ℕ.
(strictly-increasing-seq(n + 2;s.x@n.y@n + 1)
⇒ {x < y ∧ strictly-increasing-seq(n + 1;s.x@n) ∧ strictly-increasing-seq(n + 1;s.y@n)})
Definition: consistent-seq
R-consistent-seq(n) == {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))}
Lemma: consistent-seq_wf
∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[n:ℕ]. (R-consistent-seq(n) ∈ Type)
Lemma: seq-append_wf_consistent
∀T:Type. ∀R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ. ∀n:ℕ. ∀s:R-consistent-seq(n). ∀t:T.
((R n s t) ⇒ (seq-append(n;1;s;λi.t) ∈ R-consistent-seq(n + 1)))
Lemma: seq-add_wf_consistent
∀T:Type. ∀R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ. ∀n:ℕ. ∀s:R-consistent-seq(n). ∀t:T.
((R n s t) ⇒ (s.t@n ∈ R-consistent-seq(n + 1)))
Lemma: seq-append-assoc
∀[n,m,k:ℕ]. ∀[s1,s2,s3:Top].
(seq-append(n;m + k;s1;seq-append(m;k;s2;s3)) ~ seq-append(n + m;k;seq-append(n;m;s1;s2);s3))
Definition: seq-normalize
seq-normalize(n;s) == λm.if (m) < (n) then s m else ⊥
Lemma: seq-normalize_wf
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. (seq-normalize(n;s) ∈ ℕn ⟶ T)
Lemma: seq-normalize-equal
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. (seq-normalize(n;s) = s ∈ (ℕn ⟶ T))
Lemma: seq-normalize-normalize
∀[n,m:ℕ]. ∀[s:Top]. (seq-normalize(n;seq-normalize(m;s)) ~ seq-normalize(if (n) < (m) then n else m;s))
Lemma: seq-normalize-append
∀[n,m:ℕ]. ∀[s1,s2:Top]. (seq-normalize(n + m;seq-append(n;m;s1;s2)) ~ seq-append(n;m;s1;s2))
Lemma: seq-append-normalize
∀[n,m:ℕ]. ∀[s1,s2:Top]. (seq-append(n;m;s1;seq-normalize(m;s2)) ~ seq-append(n;m;s1;s2))
Lemma: seq-normalize0
seq-normalize(0;λm.⊥) ~ λm.eval x = m in
⊥
Definition: seq-adjoin
s++t == seq-append(n;1;s;λi.t)
Lemma: seq-adjoin_wf
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[t:T]. (s++t ∈ ℕn + 1 ⟶ T)
Lemma: seq-append1
∀[n:ℕ]. ∀[s,t:Top]. (seq-append(n;1;s;λi.t) ~ seq-normalize(n + 1;λm.if m=n then t else (s m)))
Lemma: seq-append1-assoc
∀[n,n1:ℕ]. ∀[s,s1,t:Top].
(λm.if m=n + n1 then t else (seq-append(n;n1;s;s1) m) ~ seq-append(n;n1 + 1;s;λm.if m=n1 then t else (s1 m)))
Lemma: seq-append0
∀[n:ℕ]. ∀[s,t:Top]. (seq-append(n;0;s;t) ~ seq-normalize(n;s))
Definition: bar_recursion
bar_recursion(d;
b;
i;
n;s) ==
fix((λbar_recursion,n,s. case d n s
of inl(r) =>
b n s r
| inr(r) =>
i n s (λt.(bar_recursion (n + 1) (λm.if m=n then t else (s m))))))
n
s
Lemma: bar_recursion_wf1
∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:ℕn ⟶ T. Dec(R[n;s])].
∀[b:∀n:ℕ. ∀s:ℕn ⟶ T. (R[n;s] ⇒ A[n;s])]. ∀[i:∀n:ℕ. ∀s:ℕn ⟶ T. ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])].
((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[m;alpha])) ⇒ (∀c:Top. (bar_recursion(d;b;i;0;c) ∈ A[0;c])))
Lemma: bar_recursion_wf
∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:ℕn ⟶ T. Dec(R[n;s])].
∀[b:∀n:ℕ. ∀s:ℕn ⟶ T. (R[n;s] ⇒ A[n;s])]. ∀[i:∀n:ℕ. ∀s:ℕn ⟶ T. ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])].
∀[n:ℕ]. ∀[s:ℕn ⟶ T].
((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[n + m;seq-append(n;m;s;alpha)]))
⇒ (bar_recursion(d;
b;
i;
n;seq-normalize(n;s)) ∈ A[n;seq-normalize(n;s)]))
Lemma: bar_recursion_wf_strong
∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[B:n:ℕ ⟶ {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))} ⟶ ℙ].
∀[A:n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:R-consistent-seq(n). Dec(B[n;s])]. ∀[b:∀n:ℕ. ∀s:R-consistent-seq(n).
(B[n;s] ⇒ A[n;s])].
∀[i:∀n:ℕ. ∀s:R-consistent-seq(n). ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) ⇒ A[n;s])].
((∀alpha:{f:ℕ ⟶ T| ∀x:ℕ. (R x f (f x))} . (↓∃m:ℕ. B[m;alpha])) ⇒ (∀x:Top. (bar_recursion(d;b;i;0;x) ∈ A[0;x])))
Lemma: bar_recursion_wf0
∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:ℕn ⟶ T. Dec(R[n;s])].
∀[b:∀n:ℕ. ∀s:ℕn ⟶ T. (R[n;s] ⇒ A[n;s])]. ∀[i:∀n:ℕ. ∀s:ℕn ⟶ T. ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])].
((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[m;alpha])) ⇒ (bar_recursion(d;b;i;0;λm.eval x = m in ⊥) ∈ A[0;λm.⊥]))
Lemma: bar_induction
∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].
((∀n:ℕ. ∀s:ℕn ⟶ T. Dec(R[n;s]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ T. (R[n;s] ⇒ A[n;s]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ T. ((∀t:T. A[n + 1;s++t]) ⇒ A[n;s]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ T. ((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[n + m;seq-append(n;m;s;alpha)])) ⇒ A[n;s])))
Lemma: basic_bar_induction
∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].
((∀n:ℕ. ∀s:ℕn ⟶ T. Dec(R[n;s]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ T. (R[n;s] ⇒ A[n;s]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ T. ((∀t:T. A[n + 1;s++t]) ⇒ A[n;s]))
⇒ (∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[m;alpha]))
⇒ (∀x:Top. A[0;x]))
Lemma: basic_strong_bar_induction
∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[B,A:n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ].
((∀n:ℕ. ∀s:R-consistent-seq(n). Dec(B[n;s]))
⇒ (∀n:ℕ. ∀s:R-consistent-seq(n). (B[n;s] ⇒ A[n;s]))
⇒ (∀n:ℕ. ∀s:R-consistent-seq(n). ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) ⇒ A[n;s]))
⇒ (∀alpha:{f:ℕ ⟶ T| ∀x:ℕ. (R x f (f x))} . (↓∃m:ℕ. B[m;alpha]))
⇒ (∀x:Top. A[0;x]))
Definition: bounded-type
Bounded(T) == ∀K:T ⟶ ℕ. (∃B:ℕ [(∀t:T. ((K t) ≤ B))])
Lemma: bounded-type_wf
∀[T:Type]. (Bounded(T) ∈ ℙ)
Definition: project-seq
project-seq(s) == λi.(snd((s i)))
Lemma: project-seq_wf
∀[T:ℕ ⟶ Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ (i:ℕ × T[i])]. project-seq(s) ∈ i:ℕn ⟶ T[i] supposing ∀i:ℕn. ((fst((s i))) = i ∈ ℤ)
Lemma: simple_more_general_fan_theorem
∀[T:ℕ ⟶ Type]
(∀i:ℕ. Bounded(T[i]))
⇒ (∀[X:n:ℕ ⟶ (i:ℕn ⟶ T[i]) ⟶ ℙ]
(∀n:ℕ. ∀s:i:ℕn ⟶ T[i]. Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:i:ℕ ⟶ T[i]. ∃n:ℕk. X[n;f])])
supposing ∀f:i:ℕ ⟶ T[i]. (↓∃n:ℕ. X[n;f]))
supposing ∀i:ℕ. T[i]
Definition: genFAN
genFAN(max;d) ==
bar_recursion(λn,s. eval x = n in
if int_seg_decide(λk.if fst((s k))=k then inr (λ_.Ax) else (inl (λ_.Ax));0;x)
then inl Ax
else case d n (λi.(snd((s i)))) of inl(z) => inl z | inr(_) => inr (λ_.Ax)
fi ;
λn,s,f. 1;
λn,s,f. ((max n (λt.(f <n, t>))) + 1);
0;λm.eval x = m in
⊥)
Lemma: simple_more_general_fan_theorem-ext
∀[T:ℕ ⟶ Type]
(∀i:ℕ. Bounded(T[i]))
⇒ (∀[X:n:ℕ ⟶ (i:ℕn ⟶ T[i]) ⟶ ℙ]
(∀n:ℕ. ∀s:i:ℕn ⟶ T[i]. Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:i:ℕ ⟶ T[i]. ∃n:ℕk. X[n;f])])
supposing ∀f:i:ℕ ⟶ T[i]. (↓∃n:ℕ. X[n;f]))
supposing ∀i:ℕ. T[i]
Lemma: genFAN_wf
∀[T:ℕ ⟶ Type]
∀[max:∀i:ℕ. Bounded(T[i])]. ∀[X:n:ℕ ⟶ (i:ℕn ⟶ T[i]) ⟶ ℙ].
∀[d:∀n:ℕ. ∀s:i:ℕn ⟶ T[i]. Dec(X[n;s])]. (genFAN(max;d) ∈ {k:ℕ| ∀f:i:ℕ ⟶ T[i]. ∃n:ℕk. X[n;f]} )
supposing ∀f:i:ℕ ⟶ T[i]. (↓∃n:ℕ. X[n;f])
supposing ∀i:ℕ. T[i]
Lemma: simple_general_fan_theorem
∀[T:Type]
(Bounded(T)
⇒ (∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]
(∀n:ℕ. ∀s:ℕn ⟶ T. Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ T. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ T. (↓∃n:ℕ. X[n;f])))
Lemma: simple_general_fan_theorem-ext
∀[T:Type]
(Bounded(T)
⇒ (∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]
(∀n:ℕ. ∀s:ℕn ⟶ T. Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ T. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ T. (↓∃n:ℕ. X[n;f])))
Definition: weakly-infinite
w∃∞p.S[p] == ∀p:ℕ. (¬¬(∃q:ℕ. (p < q ∧ S[q])))
Lemma: weakly-infinite_wf
∀[S:ℕ ⟶ ℙ]. (w∃∞x.S[x] ∈ ℙ)
Lemma: weakly-infinite-cases
∀[S:ℕ ⟶ ℙ]. (w∃∞x.S[x] ⇒ (∀[A:ℕ ⟶ ℙ]. ((∀n:ℕ. (A[n] ⇒ S[n])) ⇒ (¬¬(w∃∞n.A[n] ∨ w∃∞n.S[n] ∧ (¬A[n]))))))
Definition: TI
TI is the principle of "transfinite induction" for the
given relation R on type T.
Unfortunately, it is well-formed only when Q[t] is a proposition
on type T, so it can't be used to prove that some Q' is a proposition.⋅
TI(T;x,y.R[x; y];t.Q[t]) == (∀t:T. ((∀s:{s:T| R[t; s]} . Q[s]) ⇒ Q[t])) ⇒ (∀t:T. Q[t])
Lemma: TI_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. (TI(T;x,y.R[x;y];t.Q[t]) ∈ ℙ)
Definition: uniform-TI
uniform-TI(T;x,y.R[x; y];t.Q[t]) == (∀[t:T]. ((∀[s:{s:T| R[t; s]} ]. Q[s]) ⇒ Q[t])) ⇒ (∀[t:T]. Q[t])
Lemma: uniform-TI_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. (uniform-TI(T;x,y.R[x;y];t.Q[t]) ∈ ℙ)
Definition: weak-TI
weak-TI(T;x,y.R[x; y];t.Q[t]) == (∀t:T. ((∀s:T. (R[t; s] ⇒ Q[s])) ⇒ Q[t])) ⇒ (∀t:T. Q[t])
Lemma: weak-TI_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. (weak-TI(T;x,y.R[x;y];t.Q[t]) ∈ ℙ)
Lemma: TI-weak-TI
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. (TI(T;x,y.R[x;y];t.Q[t]) ⇒ weak-TI(T;x,y.R[x;y];t.Q[t]))
Definition: homogeneous
homogeneous(R;n;s) ==
strictly-increasing-seq(n;s) ∧ (∀m,i,j:ℕn. (m < i ⇒ m < j ⇒ (R (s m) (s i) ⇐⇒ R (s m) (s j))))
Lemma: homogeneous_wf
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. ∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. (homogeneous(R;n;s) ∈ ℙ)
Lemma: homogeneous-extension-implies
∀R:ℕ ⟶ ℕ ⟶ ℙ. ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ. (homogeneous(R;n + 1;s.m@n) ⇒ homogeneous(R;n;s))
Lemma: le2-homogeneous
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. ∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. ((n ≤ 2) ⇒ strictly-increasing-seq(n;s) ⇒ homogeneous(R;n;s))
Lemma: non-homogeneous-add
∀[R:ℕ ⟶ ℕ ⟶ ℙ]
∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀p,q:ℕ.
(p < q
⇒ homogeneous(R;n + 1;s.p@n)
⇒ homogeneous(R;n + 1;s.q@n)
⇒ (¬homogeneous(R;n + 2;s.p@n.q@n + 1))
⇒ {0 < n ∧ (¬(R (s (n - 1)) p ⇐⇒ R (s (n - 1)) q))})
Definition: weakly-safe-seq
weakly-safe-seq(R;n;s) == w∃∞q.homogeneous(R;n + 1;s.q@n)
Lemma: weakly-safe-seq_wf
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. ∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. (weakly-safe-seq(R;n;s) ∈ ℙ)
Lemma: weakly-safe-extension
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. ∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. (weakly-safe-seq(R;n;s) ⇒ (¬¬(∃p:ℕ. weakly-safe-seq(R;n + 1;s.p@n))))
Lemma: no-weakly-safe-extensions
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. ∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. ((∀p:ℕ. (¬weakly-safe-seq(R;n + 1;s.p@n))) ⇒ (¬weakly-safe-seq(R;n;s)))
Definition: almost-full
AFx,y:T.R[x; y] == ∀f:ℕ ⟶ T. (↓∃i,j:ℕ. (i < j ∧ R[f i; f j]))
Lemma: almost-full_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (AFx,y:T.R[x;y] ∈ ℙ)
Definition: AF-spread-law
AF-spread-law(x,y.R[x; y]) == λn,s,x. ((↑isl(x)) ⇒ (∀i:ℕn. ((↑isl(s i)) ∧ (¬R[outl(s i); outl(x)]))))
Lemma: AF-spread-law_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (AF-spread-law(x,y.R[x;y]) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ)
Definition: AFbar
AFbar() == λn,s. (0 < n ∧ (↑isr(s (n - 1))))
Lemma: AFbar_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (AFbar() ∈ n:ℕ ⟶ AF-spread-law(x,y.R[x;y])-consistent-seq(n) ⟶ ℙ)
Lemma: decidable__AFbar
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀n:ℕ. ∀s:AF-spread-law(x,y.R[x;y])-consistent-seq(n). Dec(AFbar() n s)
Lemma: at_AFbar
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀n:ℕ. ∀s:AF-spread-law(x,y.R[x;y])-consistent-seq(n).
((AFbar() n s) ⇒ (¬{a:T| AF-spread-law(x,y.R[x;y]) n s (inl a)} ))
Lemma: AF-path-barred
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(AFx,y:T.R[x;y] ⇒ (∀alpha:{f:ℕ ⟶ (T?)| ∀x:ℕ. (AF-spread-law(x,y.R[x;y]) x f (f x))} . (↓∃m:ℕ. (AFbar() m alpha))))
Lemma: AF-induction
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[Q:T ⟶ ℙ]. TI(T;x,y.¬R[x;y];t.Q[t])) supposing
(AFx,y:T.R[x;y] and
(∀x,y,z:T. ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))))
Lemma: AF-uniform-induction
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[Q:T ⟶ ℙ]. uniform-TI(T;x,y.¬R[x;y];t.Q[t])) supposing
(AFx,y:T.R[x;y] and
(∀x,y,z:T. ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))))
Lemma: AF-induction2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[Q:T ⟶ ℙ]. TI(T;x,y.R[x;y];t.Q[t])) supposing (AFx,y:T.¬R[x;y] and (∀x,y,z:T. (R[x;y] ⇒ R[y;z] ⇒ R[x;z])))
Lemma: AF-uniform-induction2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[Q:T ⟶ ℙ]. uniform-TI(T;x,y.R[x;y];t.Q[t])) supposing
(AFx,y:T.¬R[x;y] and
(∀x,y,z:T. (R[x;y] ⇒ R[y;z] ⇒ R[x;z])))
Lemma: AF-induction3
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[Q:T ⟶ ℙ]. TI(T;x,y.R[x;y];t.Q[t])) supposing
((∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T. (R[x;y] ⇒ (¬R'[x;y]))))) and
(∀x,y,z:T. (R[x;y] ⇒ R[y;z] ⇒ R[x;z])))
Lemma: AF-uniform-induction3
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[Q:T ⟶ ℙ]. uniform-TI(T;x,y.R[x;y];t.Q[t])) supposing
((∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T. (R[x;y] ⇒ (¬R'[x;y]))))) and
(∀x,y,z:T. (R[x;y] ⇒ R[y;z] ⇒ R[x;z])))
Definition: power-set
P(T) == I:Type × (I ⟶ T)
Lemma: power-set_wf
∀[T:𝕌']. (P(T) ∈ 𝕌')
Definition: set-member
(x ∈ s) == let I,f = s in ∃i:I. (x = (f i) ∈ T)
Lemma: set-member_wf
∀[T:Type]. ∀[s:P(T)]. ∀[x:T]. ((x ∈ s) ∈ ℙ)
Definition: power-set-lift
power-set-lift(T;R) == λA,B. ∀x:T. ((x ∈ A) ⇒ (∃y:T. ((y ∈ B) ∧ (R x y))))
Lemma: power-set-lift_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (power-set-lift(T;R) ∈ P(T) ⟶ P(T) ⟶ ℙ)
Lemma: power-set-lift-well-founded-implies
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
((∀x:T. (R x x))
⇒ (∀f:ℕ ⟶ P(T). (↓∃n:ℕ. ((power-set-lift(T;R) (f (n + 1)) (f n)) ⇒ (power-set-lift(T;R) (f n) (f (n + 1))))))
⇒ AFx,y:T.R[x;y])
Definition: cWO
cWO(T;x,y.R[x; y]) == ∀f:ℕ ⟶ T. (↓∃n:ℕ. (¬R[f n; f (n + 1)]))
Lemma: cWO_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (cWO(T;x,y.R[x;y]) ∈ ℙ)
Definition: tcWO
The relation x > y is transitive, and for any infinite sequence f
there exists i < j for which it is not the case that f(i) > f(j).
Thus there are no infinite descending sequences f(0) > f(1) > f(2) ...
This seems to be a weaker condition than the condition for a well-quasi-order.
If > is a total order, then ⌜¬(x > y) ⇐⇒ (x = y) ∨ (y > x)⌝.
In that case, letting ⌜x ≤ y⌝ be ⌜(x = y) ∨ (y > x)⌝, we have
that there exists i < j for which ⌜(f i) ≤ (f j)⌝, (and ⌜x ≤ y⌝ is transitive)
so, ⌜x ≤ y⌝ is a well-quasi-order.
But, if > is not a total order, then this definition does not rule out
and infinite antichain
(for which for all i<j, ⌜(¬((f i) > (f j))) ∧ (¬((f i) = (f j))) ∧ (¬((f j) > (f i)))⌝.
Nevertheless, we can prove, using strong bar induction, that there is an
induction principle for any tcWO relation
(i.e. transitive, constructively well-ordered relation).
We have the lemma tcWO-induction
(which can be used to prove by induction
things that are already known to be propositions)
and there is a tactic, woInduction R, that can be used to prove
by induction things that have a trivial witness. ⋅
tcWO(T;x,y.>[x; y]) == (∀x,y,z:T. (>[x; y] ⇒ >[y; z] ⇒ >[x; z])) ∧ (∀f:ℕ ⟶ T. (↓∃i,j:ℕ. (i < j ∧ (¬>[f i; f j]))))
Lemma: tcWO_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (tcWO(T;x,y.R[x;y]) ∈ ℙ)
Lemma: descending-chain-barred-implies-wellfounded
∀[T:Type]. ∀[<,B:T ⟶ T ⟶ ℙ].
((∀x,y,z:T. ((x < y) ⇒ (y < z) ⇒ (x < z)))
⇒ (∀x,y:T. Dec(x B y))
⇒ (∀x,y:T. ((x B y) ⇒ (¬(x < y))))
⇒ (∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i))))
⇒ WellFnd{i}(T;x,y.x < y))
Definition: no-descending-chain
no-descending-chain(T;<) == ∀f:ℕ ⟶ T. ∃j:ℕ. ∃i:ℕj. (¬((f j) < (f i)))
Lemma: no-descending-chain_wf
∀[T:Type]. ∀[<:T ⟶ T ⟶ ℙ]. (no-descending-chain(T;<) ∈ ℙ)
Lemma: no-descending-chain-implies-wellfounded
∀[T:Type]. ∀[<:T ⟶ T ⟶ ℙ].
((∀x,y,z:T. ((x < y) ⇒ (y < z) ⇒ (x < z)))
⇒ (∀x,y:T. Dec(x < y))
⇒ no-descending-chain(T;<)
⇒ WellFnd{i}(T;x,y.x < y))
Definition: cWO-rel
cWO-rel(R) == λn,s,x. ((0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))
Lemma: cWO-rel_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (cWO-rel(R) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ)
Definition: cWObar
cWObar() == λn,s. (0 < n ∧ (↑isr(s (n - 1))))
Lemma: cWObar_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (cWObar() ∈ n:ℕ ⟶ cWO-rel(R)-consistent-seq(n) ⟶ ℙ)
Lemma: decidable__cWObar
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀n:ℕ. ∀s:cWO-rel(R)-consistent-seq(n). Dec(cWObar() n s)
Lemma: at_cWObar
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀n:ℕ. ∀s:cWO-rel(R)-consistent-seq(n). ((cWObar() n s) ⇒ (¬{a:T| cWO-rel(R) n s (inl a)} ))
Lemma: cWO-rel-path-barred
∀[T:Type]
∀[R:T ⟶ T ⟶ ℙ]
(∀f:ℕ ⟶ T. (↓∃m:ℕ. ∃n:ℕm. (¬R[f n;f m])))
⇒ (∀alpha:{f:ℕ ⟶ (T?)| ∀x:ℕ. (cWO-rel(R) x f (f x))} . (↓∃m:ℕ. (cWObar() m alpha)))
supposing ∀a,b,c:T. (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
supposing T
Lemma: cWO-induction_1
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. TI(T;x,y.R[x;y];t.Q[t]) supposing cWO(T;x,y.R[x;y])
Lemma: cWO-induction_1-ext
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. TI(T;x,y.R[x;y];t.Q[t]) supposing cWO(T;x,y.R[x;y])
Lemma: tcWO-induction
∀[T:Type]. ∀[>:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. TI(T;x,y.>[x;y];t.Q[t]) supposing tcWO(T;x,y.>[x;y])
Lemma: tcWO-induction-ext
∀[T:Type]. ∀[>:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. TI(T;x,y.>[x;y];t.Q[t]) supposing tcWO(T;x,y.>[x;y])
Definition: Wqo
Wqo(T;x,y.R[x; y]) ==
(∀f:ℕ ⟶ T. (↓∃i,j:ℕ. (i < j ∧ R[f i; f j]))) ∧ (∀x:T. R[x; x]) ∧ (∀x,y,z:T. (R[x; y] ⇒ R[y; z] ⇒ R[x; z]))
Lemma: Wqo_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (Wqo(T;x,y.R[x;y]) ∈ ℙ)
Definition: wqo-less
wqo-less(T;x,y.R[x; y];bs;as) ==
∃a:T. let m,s' = bs in let n,s = as in (m = (n + 1) ∈ ℤ) ∧ (s' = s.s' n@n ∈ (ℕm ⟶ T)) ∧ (∀i:ℕn. (¬R[s i; s' n]))
Lemma: wqo-less_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[bs,as:n:ℕ × (ℕn ⟶ T)]. (wqo-less(T;x,y.R[x;y];bs;as) ∈ ℙ)
Definition: ccomb
C == λf,x,y. (f y x)
Lemma: ccomb_wf
∀[P,A,B:Type]. (C ∈ (A ⟶ B ⟶ P) ⟶ B ⟶ A ⟶ P)
Home
Index