Comment: bool_1_summary
Definitions, theorems and tactics for the boolean 
type and boolean-related expressions.

Comment: bool_1_intro
Definitions, theorems, and tactics for boolean type
and standard boolean operators.

Theorems include standard logic ones, as well
as `assert' theorems for converting between boolean 
and prop-valued predicates.

This implementation of bool differs from that in Nuprl V3.
There, the booleans were defined as subtype of the integers.
Here, the use of the Unit Unit type enables evaluation
of boolean expressions, especially those involving 
ifthenelse, using Nuprl's direct computation rules. This
is of great help when these expressions are used in 
definitions of recursive functions, whose proof of 
well-formedness relies heavily on direct-computation-style


Comment: BOOL_DEFS

Definition: exposed-btrue
exposed-btrue ==  inl ⋅

Definition: exposed-bfalse
exposed-bfalse ==  inr ⋅ 

Lemma: bool_sq

Lemma: bool_sim_true
[b:𝔹]. tt supposing tt

Lemma: bool_sim_false
[b:𝔹]. ff supposing ff

Lemma: assert_witness
[b:𝔹]. ((↑b)  (Ax ∈ ↑b))

Lemma: comb_for_assert_wf
λb,z. (↑b) ∈ b:𝔹 ⟶ (↓True) ⟶ ℙ

Lemma: ifthenelse-wf
[b:𝔹]. ∀[A:Type]. ∀[p:⋂v:↑b. A]. ∀[q:⋂v:¬↑b. A].  (if then else fi  ∈ A)

Definition: band
p ∧b ==  if then else ff fi 

Definition: bor
p ∨b==  if then tt else fi 

Lemma: btrue_neq_bfalse
¬tt ff

Lemma: band_wf
[p,q:𝔹].  (p ∧b q ∈ 𝔹)

Lemma: bor_wf
[p,q:𝔹].  (p ∨bq ∈ 𝔹)

Lemma: band_ff
[u:𝔹]. (u ∧b ff ff)

Lemma: band_tt
[u:𝔹]. (u ∧b tt u)

Lemma: bor_ff_simp
[u:𝔹]. u ∨bff u

Lemma: bor_tt_simp
[u:𝔹]. u ∨btt tt

Lemma: band_ff_simp
[u:𝔹]. u ∧b ff ff

Lemma: band_tt_simp
[u:𝔹]. u ∧b tt u

Lemma: bnot_bnot
[p:Top]. b¬bp ∧b tt)

Lemma: bnot_bnot_elim
[p:𝔹]. ¬b¬bp

Lemma: band_assoc
[a,b,c:Top].  ((a ∧b b) ∧b a ∧b b ∧b c)

Lemma: band_commutes
[a,b:𝔹].  a ∧b b ∧b a

Lemma: bor_assoc
[a,b,c:Top].  ((a ∨bb) ∨ba ∨bb ∨bc)

Lemma: bor_band_distributive
[a,b,c:Top].  (a ∨b(b ∧b c) (a ∨bb) ∧b (a ∨bc))

Lemma: band_bor_distributive
[a,b,c:Top].  (a ∧b (b ∨bc) (a ∧b b) ∨b(a ∧b c))

Lemma: bor_band_absorption
[a,b:Top].  (a ∧b (a ∨bb) a ∧b tt)

Lemma: band_bor_absorption
[a,b:Top].  (a ∨b(a ∧b b) a ∧b tt)

Lemma: band_bnot
[a:Top]. (a ∧b ba) a ∧b ff)

Lemma: bor_bnot
[a:Top]. (a ∨bba) a ∨btt)

Lemma: bnot_thru_band
[p,q:Top].  b(p ∧b q) bp) ∨bbq))

Lemma: bnot_thru_bor
[p,q:Top].  b(p ∨bq) bp) ∧b bq))

Lemma: bnot_of_le_int
[i,j:ℤ].  ¬bi ≤j <i

Lemma: bnot_of_lt_int
[i,j:ℤ].  ¬bi <j ≤i

Definition: b2i
b2i(b) ==  if then else fi 

Lemma: b2i_wf
[b:𝔹]. (b2i(b) ∈ ℤ)

Lemma: comb_for_b2i_wf
λb,z. b2i(b) ∈ b:𝔹 ⟶ (↓True) ⟶ ℤ

Lemma: b2i_bounds
[b:𝔹]. ((0 ≤ b2i(b)) ∧ (b2i(b) ≤ 1))

Lemma: comb_for_bnot_wf
λb,z. bb) ∈ b:𝔹 ⟶ (↓True) ⟶ 𝔹

Lemma: comb_for_bor_wf
λp,q,z. (p ∨bq) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹

Lemma: comb_for_band_wf
λp,q,z. (p ∧b q) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹

Definition: eq_bool
=b ==  (p ∧b q) ∨b((¬bp) ∧b bq))

Lemma: eq_bool_wf
[p,q:𝔹].  (p =b q ∈ 𝔹)

Definition: bxor
p ⊕==  (p ∧b bq)) ∨b((¬bp) ∧b q)

Lemma: bxor_wf
[p,q:𝔹].  (p ⊕q ∈ 𝔹)

Definition: bimplies
b ==  bp) ∨bq

Lemma: bimplies_wf
[p:𝔹]. ∀[q:𝔹 supposing ↑p].  (p b q ∈ 𝔹)

Lemma: comb_for_bimplies_wf
λp,q,z. (p b q) ∈ p:𝔹 ⟶ q:𝔹 supposing ↑p ⟶ (↓True) ⟶ 𝔹

Definition: rev_bimplies
b ==  b p

Lemma: rev_bimplies_wf
[p,q:𝔹].  (p b q ∈ 𝔹)

Comment: bool_thms

Lemma: bool_ind
[P:𝔹 ⟶ ℙ]. (P[ff]  P[tt]  {∀b:𝔹P[b]})

Lemma: decidable__equal_bool
a,b:𝔹.  Dec(a b)

Lemma: bimplies_weakening
[u,v:𝔹].  ↑(u b v) supposing v

Lemma: bimplies_transitivity
[u,v,w:𝔹].  (↑(u b w)) supposing ((↑(v b w)) and (↑(u b v)))

Lemma: assert_functionality_wrt_bimplies
[u,v:𝔹].  {↑supposing ↑u} supposing ↑(u b v)

Lemma: assert_functionality_wrt_uiff
[u,v:𝔹].  {uiff(↑u;↑v)} supposing v

Comment: bool_tactics_1
=========================  TACTICS USED IN `ASSERT' =========================================

Lemma: iff_imp_equal_bool
[a,b:𝔹].  supposing ↑⇐⇒ ↑b

Lemma: equal_bool_if
[a,b:𝔹].  (a b) supposing ((¬((↑a) ∧ (¬↑b))) and ((¬↑a) ∧ (↑b))))

Lemma: assert_equal
[a,b:𝔹].  uiff((↑a) (↑b) ∈ Type;↑⇐⇒ ↑b)

Lemma: ifthenelse_functionality_wrt_uimplies
    (b1 b2
     {q2 supposing q1}
     {p2 supposing p1}
     {if b2 then p2 else q2 fi  supposing if b1 then p1 else q1 fi })

Lemma: ifthenelse_functionality_wrt_implies
  ∀[p1,q1,p2,q2:ℙ].  (b1 b2  {q1  q2}  {p1  p2}  {if b1 then p1 else q1 fi   if b2 then p2 else q2 fi })

Lemma: ifthenelse_functionality_wrt_iff
    (b1 b2  {q1 ⇐⇒ q2}  {p1 ⇐⇒ p2}  {if b1 then p1 else q1 fi  ⇐⇒ if b2 then p2 else q2 fi })

Lemma: ifthenelse_functionality_wrt_rev_implies
  ∀[p1,q1,p2,q2:ℙ].  (b1 b2  {q1  q2}  {p1  p2}  {if b1 then p1 else q1 fi   if b2 then p2 else q2 fi })

Lemma: ifthenelse_functionality_wrt_uimplies2
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q2 supposing q1}  {if b1 then else q1 fi   if b2 then else q2 fi })

Lemma: ifthenelse_functionality_wrt_implies2
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q1  q2}  {if b1 then else q1 fi   if b2 then else q2 fi })

Lemma: ifthenelse_functionality_wrt_iff2
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q1 ⇐⇒ q2}  {if b1 then else q1 fi  ⇐⇒ if b2 then else q2 fi })

Lemma: ifthenelse_functionality_wrt_implies3
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q1  q2}  {if b1 then q1 else fi   if b2 then q2 else fi })

Lemma: ifthenelse_functionality_wrt_iff3
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q1 ⇐⇒ q2}  {if b1 then q1 else fi  ⇐⇒ if b2 then q2 else fi })

Lemma: ifthenelse_functionality_wrt_rev_implies2
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q1  q2}  {if b1 then else q1 fi   if b2 then else q2 fi })

Lemma: ifthenelse_functionality_wrt_rev_implies3
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q1  q2}  {if b1 then q1 else fi   if b2 then q2 else fi })

Lemma: ifthenelse_functionality_wrt_uimplies3
b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 b2  {q2 supposing q1}  {if b1 then q1 else fi   if b2 then q2 else fi })

Lemma: eq_atom-reflexive
[x:Atom]. =a tt

Lemma: neg_assert_of_eq_int
[x,y:ℤ].  uiff(¬↑(x =z y);x ≠ y)

Lemma: neg_assert_of_eq_atom
[x,y:Atom].  uiff(¬↑=a y;x ≠ y ∈ Atom )

Comment: assert_eqint_rw
The assert_eq_int_rw object is now redundant. However, it
is still referenced in at least the rational library.

Lemma: assert_of_eq_int_rw
[x,y:ℤ].  {uiff(↑(x =z y);x y ∈ ℤ)}

Lemma: assert_of_eq_bool
[p,q:𝔹].  uiff(↑=b q;p q)

Lemma: assert-bnot
[p:𝔹]. ((↑¬bp)  (¬↑p))

Lemma: assert_of_band
p:𝔹. ∀q:⋂:↑p. 𝔹.  uiff(↑(p ∧b q);(↑p) ∧ (↑q))

Lemma: assert_of_bor
p:𝔹. ∀[q:𝔹]. uiff(↑(p ∨bq);(↑p) ∨ (↑q))

Lemma: assert_of_bimplies
[p:𝔹]. ∀[q:𝔹 supposing ↑p].  uiff(↑(p b q);↑supposing ↑p)

Comment: bool_tactics

Lemma: ite_rw_false
[T:Type]. ∀[b:𝔹]. ∀[x,y:T].  if then else fi  y ∈ supposing ¬↑b

Lemma: ite_rw_true
[T:Type]. ∀[b:𝔹]. ∀[x,y:T].  if then else fi  x ∈ supposing ↑b

Lemma: fun_thru_ite
[S,T:Type]. ∀[f:S ⟶ T]. ∀[b:𝔹]. ∀[p,q:S].  ((f if then else fi if then else fi  ∈ T)

Comment: old_bool_1_stuff
Obselete tactics and theorems that are maybe used in
old proofs.

Lemma: eq_int_eq_false
[i,j:ℤ].  (i =z j) ff supposing i ≠ j

Lemma: eq_int_eq_true
[i,j:ℤ].  (i =z j) tt supposing j ∈ ℤ

Lemma: eq_int_eq_false_elim
[i,j:ℤ].  i ≠ supposing (i =z j) ff

Lemma: eq_int_eq_true_elim
[i,j:ℤ].  j ∈ ℤ supposing (i =z j) tt

Lemma: eq_int_cases_test
[A:Type]. ∀x,y:A.  ∀[P:A ⟶ ℙ]. ∀i,j:ℤ.  ((P if (i =z j) then else fi  (P if (i =z j) then else fi ))

Lemma: comb_for_lt_int_wf
λi,j,z. i <j ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ 𝔹

Lemma: assert-pushdown-test
C:𝔹. ↑((C ∧b C) ∨bC) supposing ↑(C ∧b C)

Lemma: subtype_rel_b-union
[A1,B1,A2,B2:Type].  (A1 ⋃ B1) ⊆(A2 ⋃ B2) supposing (A1 ⊆A2) ∧ (B1 ⊆B2)

Lemma: subtype_rel_b-union-left
[A,B:Type].  (A ⊆(A ⋃ B))

Lemma: subtype_rel_b-union-right
[A,B:Type].  (B ⊆(A ⋃ B))

Lemma: subtype_rel_union_left
[A,B:Type].  (A ⊆(A ⋃ B))

Lemma: subtype_rel_union_right
[A,B:Type].  (B ⊆(A ⋃ B))

Lemma: subtype_rel_b-union_iff
[A,B,C:Type].  uiff((B ⋃ C) ⊆A;(B ⊆A) ∧ (C ⊆A))

Definition: isect2
T1 ⋂ T2 ==  ⋂b:𝔹if then T1 else T2 fi 

Lemma: isect2_wf
[T1,T2:Type].  (T1 ⋂ T2 ∈ Type)

Lemma: isect2_decomp
[t1,t2:Type]. ∀[x:t1 ⋂ t2].  ((x ∈ t1) ∧ (x ∈ t2))

Lemma: subtype_rel_isect2
[A,B,C:Type].  uiff(A ⊆B ⋂ C;(A ⊆B) ∧ (A ⊆C))

Lemma: isect2_subtype_rel
[A,B:Type].  (A ⋂ B ⊆A)

Lemma: isect2_subtype_rel2
[A,B:Type].  (A ⋂ B ⊆B)

Lemma: isect2_subtype_rel3
[A,B,C:Type].  A ⋂ B ⊆supposing (A ⊆C) ∨ (B ⊆C)

Lemma: isect_prod_lemma
[A,B,C:Type].  (A × B ⋂ A × C ⊆(A × B ⋂ C))

Definition: b-isect
b-isect(T1;T2) ==  ⋂b:⇃(𝔹). if then T1 else T2 fi 

Definition: pair-blex
pair-blex(eq;Ra;Rb) ==  λx,y. ((Ra (fst(x)) (fst(y))) ∨b((eq (fst(x)) (fst(y))) ∧b (Rb (snd(x)) (snd(y)))))

Lemma: pair-blex_wf
[A,B:Type]. ∀[eq,Ra:A ⟶ A ⟶ 𝔹]. ∀[Rb:B ⟶ B ⟶ 𝔹].  (pair-blex(eq;Ra;Rb) ∈ (A × B) ⟶ (A × B) ⟶ 𝔹)

Definition: dcdr-to-bool
[d]b ==  case of inl(x) => inl ⋅ inr(x) => inr ⋅ 

Lemma: dcdr-to-bool_wf
[P:ℙ]. ∀[d:Dec(P)].  ([d]b ∈ 𝔹)

Lemma: dcdr-to-bool-equivalence
[P:ℙ]. ∀d:Dec(P). (↑[d]b ⇐⇒ P)

Lemma: ite-bool-1
[b:𝔹]. ∀[x:Top].  (if then else tt fi  bb) ∨bx)

Lemma: ite-bool-2
[b:𝔹]. ∀[x:Top].  (if then else ff fi  b ∧b x)

Lemma: ite-bool-3
[b:𝔹]. ∀[x:Top].  (if then tt else fi  b ∨bx)

Lemma: ite-bool-4
[b:𝔹]. ∀[x:Top].  (if then ff else fi  bb) ∧b x)

Lemma: bor-bfalse
[b:𝔹]. (b ∨bff b)

Lemma: bor-btrue
[b:𝔹]. (b ∨btt tt)

Lemma: band-btrue
[b:𝔹]. (b ∧b tt b)

Lemma: band-bfalse
[b:𝔹]. (b ∧b ff ff)

Lemma: band-simplify
[b:𝔹]. ∀[f:Top].  (b ∧b f[b] b ∧b f[tt])

Lemma: band-idempotent
[b:𝔹]. (b ∧b b)

Lemma: bor-simplify
[b:𝔹]. ∀[f:Top].  (b ∨bf[b] b ∨bf[ff])

Lemma: bor-assoc
[b:𝔹]. ∀[c,d:Top].  (b ∨bc ∨b(b ∨bc) ∨bd)

Lemma: bor-inl
[a,b:Top].  ((inl a) ∨btt)

Lemma: bor-inr
[a,b:Top].  ((inr ) ∨bb)

Lemma: band-inl
[a,b:Top].  ((inl a) ∧b b)

Lemma: band-inr
[a,b:Top].  ((inr ) ∧b ff)

Lemma: testxxx_lemma
b:Top. (tt ∨btt)

Lemma: ifthenelse-inl
[a,b,c:Top].  (if inl then else fi  b)

Lemma: ifthenelse-inr
[a,b,c:Top].  (if inr a  then else fi  c)

Lemma: bnot-inl
[a:Top]. b(inl a) ff)

Lemma: bnot-inr
[a:Top]. b(inr tt)

Lemma: free-from-atom-bool
[a:Atom1]. ∀[n:𝔹].  a#n:𝔹

Lemma: free-from-atom-bool-subtype
[a:Atom1]. ∀[T:Type].  ∀[n:T]. a#n:T supposing T ⊆r 𝔹

Lemma: has-value-bor
[a,b:Base].  (a)↓ supposing (a ∨bb)↓

Lemma: has-value-bor-type
[a,b:Base].  a ∈ Top Top supposing (a ∨bb)↓

Lemma: has-value-band
[a,b:Base].  (a)↓ supposing (a ∧b b)↓

Lemma: has-value-band-type
[a,b:Base].  a ∈ Top Top supposing (a ∧b b)↓

Lemma: has-value-ifthenelse
[a,b,c:Base].  (a)↓ supposing (if then else fi )↓

Lemma: has-value-ifthenelse-type
[a,b,c:Base].  a ∈ Top Top supposing (if then else fi )↓

Lemma: has-value-bnot
[a:Base]. (a)↓ supposing ba)↓

Lemma: has-value-bnot-type
[a:Base]. a ∈ Top Top supposing ba)↓

Lemma: band-is-inl
[a,b:Top Top]. ∀[c:Top].  (a inl outl(a)) ∧ (b inl outl(b)) supposing (a ∧b b) (inl c) ∈ (Top Top)

Lemma: band-is-inl-base
  ∀[c:Top]. (a inl outl(a)) ∧ (b inl outl(b)) supposing (a ∧b b) (inl c) ∈ (Top Top) 
  supposing a ∧b b ∈ Top Top

Lemma: band-sqequal-inl
[a,b,c:Base].  {(a inl outl(a)) ∧ (b inl outl(b))} supposing a ∧b inl c

Lemma: simple_fan_theorem
[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s]))  (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹(↓∃n:ℕX[n;f])

Lemma: simple_fan_theorem-ext
[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s]))  (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹(↓∃n:ℕX[n;f])

Definition: b-exists
(∃i<n.P[i])_b ==  primrec(n;ff;λi,x. (P[i] ∨bx))

Lemma: b-exists_wf
[n:ℕ]. ∀[P:ℕn ⟶ 𝔹].  ((∃i<n.P[i])_b ∈ 𝔹)

Lemma: assert-b-exists
n:ℕ. ∀P:ℕn ⟶ 𝔹.  (↑(∃i<n.P[i])_b ⇐⇒ ∃i:ℕn. (↑P[i]))

Lemma: b-exists-bfalse
[n:ℕ]. ((∃x<n.ff)_b ff)

Definition: bdd-all
bdd-all(n;i.P[i]) ==  primrec(n;tt;λi,x. (P[i] ∧b x))

Lemma: bdd-all_wf
[n:ℕ]. ∀[P:ℕn ⟶ 𝔹].  (bdd-all(n;i.P[i]) ∈ 𝔹)

Lemma: bdd-all-btrue
[n:ℕ]. (bdd-all(n; tt)

Lemma: assert-bdd-all
n:ℕ. ∀P:ℕn ⟶ 𝔹.  (↑bdd-all(n;i.P[i]) ⇐⇒ ∀i:ℕn. (↑P[i]))

Lemma: not-assert-bdd-all
n:ℕ. ∀P:ℕn ⟶ 𝔹.  (¬↑bdd-all(n;i.P[i]) ⇐⇒ ∃i:ℕn. (¬↑P[i]))

Lemma: bdd_all_zero_lemma
P:Top. (bdd-all(0;x.P[x]) tt)

Lemma: ifthenelse-simplify0
[b:𝔹]. ∀[x,y:Top].  (if then x[b] else y[b] fi  if then x[tt] else y[ff] fi )

Lemma: ifthenelse-simplify1
[b,c:𝔹]. ∀[x,y:Top].  (if then if then else fi  else fi  if b ∧b then else fi )

Lemma: ifthenelse-simplify2
[b,c:𝔹]. ∀[x,y:Top].  (if then if then else fi  if b ∨bthen else fi )

Lemma: ifthenelse-simplify3
[b:𝔹]. (if then tt else ff fi  b)

Lemma: ifthenelse-prop
b:𝔹. ∀p,q:ℙ'.  (if then else fi  ⇐⇒ ((↑b) ∧ p) ∨ ((¬↑b) ∧ q))

Lemma: ifthenelse-false-left
b:𝔹. ∀[q:ℙ]. (if then False else fi  ⇐⇒ (¬↑b) ∧ q)

Lemma: ifthenelse-false-right
b:𝔹. ∀[q:ℙ]. (if then else False fi  ⇐⇒ (↑b) ∧ q)

Lemma: apply-ifthenelse
[T,U:Type]. ∀[f:T ⟶ U]. ∀[b:𝔹]. ∀[x,y:T].  (f[if then else fi if then f[x] else f[y] fi )

Lemma: apply-ifthenelse2
[T1,U1,T2,U2:Type]. ∀[x:T1]. ∀[y:T2]. ∀[b:𝔹]. ∀[f:if then T1 ⟶ U1 else T2 ⟶ U2 fi ].
  (f[if then else fi if then f[x] else f[y] fi )

Lemma: apply-ifthenelse-pi1
[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  (fst(if then else fi if then fst(x) else fst(y) fi )

Lemma: apply-ifthenelse-pi1-eq
[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((fst(if then else fi )) if then fst(x) else fst(y) fi  ∈ if then T1 else T2 fi )

Lemma: apply-ifthenelse-pi2
[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  (snd(if then else fi if then snd(x) else snd(y) fi )

Lemma: apply-ifthenelse-pi2-eq
[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((snd(if then else fi )) if then snd(x) else snd(y) fi  ∈ if then U1 else U2 fi )

Definition: imax
imax(a;b) ==  eval in eval in   if a ≤then else fi 

Lemma: imax_wf
[a,b:ℤ].  (imax(a;b) ∈ ℤ)

Lemma: imax_unfold
[a,b:ℤ].  (imax(a;b) if a ≤then else fi  ∈ ℤ)

Lemma: imax_nat
[a:ℤ]. ∀[b:ℕ].  (imax(a;b) ∈ ℕ)

Lemma: simple_fan_theorem'
[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s]))  (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹(↓∃n:ℕX[n;f])

Definition: FAN
FAN(d) ==  bar_recursion(d;λn,s,f. 1;λn,s,f. (imax(f tt;f ff) 1);0;λm.eval in ⊥)

Lemma: simple_fan_theorem'-ext
[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s]))  (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹(↓∃n:ℕX[n;f])

Lemma: FAN_wf
[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  ∀[d:∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])]. (FAN(d) ∈ {k:ℕ| ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]} supposing ∀f:ℕ ⟶ 𝔹(↓∃n:ℕX[n;f])

Lemma: less-as-ifthenelse
[r,s,x,y:Top].  (if (r) < (s)  then x  else if r <then else fi )

Lemma: int_eq-as-ifthenelse
[r,s,x,y:Top].  (if r=s then else if (r =z s) then else fi )

Lemma: ifthenelse-as-bor
[b:𝔹]. ∀[x:Top].  (if then tt else fi  b ∨bx)

Lemma: ifthenelse-as-bor
[b:𝔹]. ∀[x:Top].  (if then tt else fi  b ∨bx)

Lemma: ifthenelse-as-bor-bnot
[b:𝔹]. ∀[x:Top].  (if then else tt fi  bb) ∨bx)

Lemma: ifthenelse-as-band
[b:𝔹]. ∀[x:Top].  (if then else ff fi  b ∧b x)

Lemma: ifthenelse-as-band-bnot
[b:𝔹]. ∀[x:Top].  (if then ff else fi  bb) ∧b x)

Home Index