Comment: core_2_intro
Introduces variety of general-purpose definitions and

Definition: ycomb
==  λf.((λx.(f (x x))) x.(f (x x))))

Definition: recind-ycomb
Y' ==  λf,x. letrec x(y) in x(x)

Definition: pi2
snd(t) ==  let x,y in y

Definition: pi1
fst(t) ==  let x,y in x

Definition: so_apply1
x[s] ==  s

Definition: so_apply2
x[s1;s2] ==  s1 s2

Definition: so_apply3
x[s1;s2;s3] ==  s1 s2 s3

Definition: so_apply4
x[s1;s2;s3;s4] ==  s1 s2 s3 s4

Definition: so_apply5
x[s1;s2;s3;s4;s5] ==  s1 s2 s3 s4 s5

Definition: so_apply6
x[a;b;c;d;e;f] ==  f

Definition: so_apply7
x[a;b;c;d;e;f;g] ==  g

Definition: so_apply8
x[a;b;c;d;e;f;g;h] ==  h

Definition: so_apply9
x[a;b;c;d;e;f;g;h;i] ==  i

Definition: so_apply10
x[a;b;c;d;e;f;g;h;i;j] ==  j

Definition: so_apply11
x[a;b;c;d;e;f;g;h;i;j;k] ==  k

Definition: so_apply12
x[a;b;c;d;e;f;g;h;i;j;k;l] ==  l

Definition: so_apply13
x[a;b;c;d;e;f;g;h;i;j;k;l;m] ==  m

Definition: so_apply14
x[a;b;c;d;e;f;g;h;i;j;k;l;m;n] ==  n

Definition: infix_ap
==  y

Definition: so_lambda1
λ2x.t[x] ==  λx.t[x]

Definition: so_lambda2
λ2y.t[x; y] ==  λx,y. t[x; y]

Definition: so_lambda3
                  z]) ==
  λx,y,z. t[x;

Definition: so_lambda4
                    w]) ==
  λx,y,z,w. t[x;

Definition: so_lambda5
                      v]) ==
  λx,y,z,w,v. t[x;

Definition: so_lambda6
                       w]) ==
  λx,y,z,u,v,w. t[x;

Definition: so_lambda7
                         q]) ==
  λx,y,z,u,v,w,q. t[x;

Definition: so_lambda8
                            p]) ==
  λx,y,z,u,v,w,q,p. t[x;

Definition: so_lambda9
                              r]) ==
  λx,y,z,u,v,w,q,p,r. t[x;

Definition: label
...$L... ==  t

Definition: guard
{T} ==  T

Definition: show
The term show(x) unfolds to x. It has special display form that makes it
easy to spot.  We make conversion ShowAddrC addr that folds `show` at the
given addr. That helps when working with conversions so that we can
easily see what term is at given address. ⋅

⇒⇒ ⇐⇐ ==  x

Definition: error
??? ==  "error"

Definition: prop
ℙ ==  Type

Definition: cand
c∧ ==  A × B

Definition: parameter
parm{i} ==  !null_abstraction

Comment: top_com
Top⌝ is the type that contains all terms

Definition: top
Top⌝ is the type that contains all terms⋅

Top ==  ⋂x:Void. Void

Lemma: top_wf
Top ∈ Type

Lemma: istype-top

Lemma: istype-void

Lemma: istype-int

Lemma: istype-atom

Definition: uall
This is "uniform" universal quantification.
Evidence for ⌜∀[x:A]. B[x]⌝ must be something that is member of ⌜B[x]⌝
whenever ⌜x ∈ A⌝Such evidence is independent of the choice of ⌜x ∈ A⌝. ⋅

[x:A]. B[x] ==  ⋂x:A. B[x]

Lemma: uall_wf
[A:Type]. ∀[B:A ⟶ ℙ].  (∀[x:A]. B[x] ∈ ℙ)

Lemma: isect_wf
[A:Type]. ∀[B:A ⟶ ℙ].  (⋂x:A. B[x] ∈ ℙ)

Lemma: base_wf
Base ∈ Type

Lemma: istype-base

Lemma: image-type_wf
[A:Type]. ∀[f:Base].  (Image(A,f) ∈ Type)

Definition: tunion_def
The union of family types B[x], x ∈ is obtained from the type 
x:A × B[x] of all pairs <a, b>a ∈ A, b ∈ B[a] by projection onto the
second component.  That means that b ∈ ⋃x:A.B[x]  if for some a ∈ A,
<a, b> ∈ x:A × B[x].⋅

x:A.B[x] ==  Image((x:A × B[x]),(λp.(snd(p))))

Lemma: tunion_wf
[A:Type]. ∀[B:A ⟶ Type].  (⋃x:A.B[x] ∈ Type)

Lemma: set_wf
[A:Type]. ∀[B:A ⟶ Type].  ({a:A| B[a]}  ∈ Type)

Lemma: set-elim
[A:Type]. ∀[B:A ⟶ Type].  ∀x:Image((a:A × B[a]),(λp.(fst(p)))). ((x ∈ A) ∧ (↓B[x]))

Lemma: equal-wf-base
[A:Type]. ∀[a,b:Base].  (a b ∈ A ∈ ℙ)

Lemma: trivial-equal
[A:Type]. ∀[a:A].  (a a ∈ A)

Definition: respects-equality
respects-equality(S;T) ==  ∀x,y:Base.  ((x y ∈ S)  (x ∈ T)  (x y ∈ T))

Lemma: respects-equality_wf
[S,T:Type].  (respects-equality(S;T) ∈ Type)

Lemma: base-respects-equality
[T:Type]. respects-equality(Base;T)

Lemma: respects-equality-trivial
[T:Type]. respects-equality(T;T)

Lemma: respects-equality-set-trivial
[T:Type]. ∀[P:T ⟶ ℙ].  respects-equality(T;{x:T| P[x]} )

Lemma: respects-equality-set-trivial2
[T:Type]. ∀[P:T ⟶ ℙ].  respects-equality({x:T| P[x]} ;T)

Lemma: respects-equality-set
[A,T:Type]. ∀[P:T ⟶ ℙ].  (respects-equality(A;T)  respects-equality(A;{x:T| P[x]} ))

Lemma: respects-equality-sets
[A,T:Type]. ∀[P:T ⟶ ℙ]. ∀[Q:A ⟶ ℙ].  (respects-equality(A;T)  respects-equality({x:A| Q[x]} ;{x:T| P[x]} ))

Lemma: equal-wf
[X,Y,A:Type].  (respects-equality(Y;A)  respects-equality(X;A)  (∀[a:X]. ∀[b:Y].  (a b ∈ A ∈ ℙ)))

Lemma: equal_wf
[A:Type]. ∀[a,b:A].  (a b ∈ A ∈ ℙ)

Lemma: equal-wf-T-base
[T:Type]. ∀[a:T]. ∀[b:Base].  (a b ∈ T ∈ ℙ)

Lemma: equal-wf-base-T
[T:Type]. ∀[a:Base]. ∀[b:T].  (a b ∈ T ∈ ℙ)

Lemma: change-equality-type
[A,B:Type].  (respects-equality(A;B)  (∀x,y:A.  ((x y ∈ A)  (x ∈ B)  (x y ∈ B))))

Definition: subtype_rel
A ⊆==  λx.x ∈ A ⟶ B

Lemma: subtype_rel_wf
[A,B:Type].  (A ⊆B ∈ Type)

Definition: istype
istype(T) ==  T ⊆T

Lemma: istype_wf
[T:Type]. (istype(T) ∈ Type)

Lemma: istype-universe
[T:Type]. istype(T)

Lemma: respects-equality_weakening
[T,S:Type].  ((S T ∈ Type)  respects-equality(S;T))

Lemma: respects-equality-function
[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].
  ((A' ⊆A)  (∀a:A'. respects-equality(B[a];B'[a]))  respects-equality(a:A ⟶ B[a];a:A' ⟶ B'[a]))

Lemma: false_wf
False ∈ ℙ

Lemma: istype-false

Lemma: void_wf
Void ∈ Type

Lemma: int-wf
ℤ ∈ Type

Comment: no apply_wf
The "true" _wf for apply would be
⌜∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A ⟶ B[x]]. ∀[a:A].  (f a ∈ B[a])⌝

an "approximation" is 
⌜∀[A,B:Type]. ∀[f:x:A ⟶ B]. ∀[a:A].  (f a ∈ B)⌝

Both of these are true, but if we add them to the library
then they would be used by type inference and by Auto

At present, they interfere too much with the working of other tactic.
So, until we understand the problems better, we do not add _wf lemma
for apply.⋅

Lemma: infix_ap_wf
[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[x:A]. ∀[y:B].  (x y ∈ C)

Lemma: lambda-wf
[A,B:Type]. ∀[f:A ⟶ B].  x.f[x] ∈ A ⟶ B)

Lemma: product-wf
[A:Type]. ∀[B:A ⟶ Type].  (a:A × B[a] ∈ Type)

Lemma: exists_wf
[A:Type]. ∀[B:A ⟶ ℙ].  (∃a:A. B[a] ∈ ℙ)

Lemma: and_wf
[A,B:ℙ].  (A ∧ B ∈ ℙ)

Lemma: cand_wf
[A,B:ℙ].  (A c∧ B ∈ ℙ)

Lemma: or_wf
[A,B:ℙ].  (A ∨ B ∈ ℙ)

Lemma: function-wf
[A:Type]. ∀[B:A ⟶ Type].  (a:A ⟶ B[a] ∈ Type)

Lemma: all_wf
[A:Type]. ∀[B:A ⟶ ℙ].  (∀a:A. B[a] ∈ ℙ)

Lemma: sq_exists_wf
[A:Type]. ∀[B:A ⟶ ℙ].  (∃a:A [B[a]] ∈ ℙ)

Lemma: set-wf
[A:Type]. ∀[P:A ⟶ ℙ].  ({a:A| P[a]}  ∈ Type)

Lemma: union-wf
[A,B:Type].  (A B ∈ Type)

Lemma: add-wf
[x,y:ℤ].  (x y ∈ ℤ)

Lemma: minus_wf
[x:ℤ]. (-x ∈ ℤ)

Lemma: multiply_wf
[x,y:ℤ].  (x y ∈ ℤ)

Lemma: subtract_wf
[x,y:ℤ].  (x y ∈ ℤ)

Lemma: uall_subtype
[F:Type ⟶ Type]. ∀[A:Type].  ((∀[A:Type]. F[A]) ⊆F[A])

Definition: uimplies
This is "uniform" implication.
Evidence for (a  b) is function from evidence for to evidence for b,
but evidence for (b supposing a) is something that is evidence for b
as long as is not empty (i.e. supposing that has evidence).

Thus, the evidence must be "uniform" because it does not depend on
the the evidence for a. ⋅

supposing ==  ⋂:a. b

Lemma: uimplies-wf
[A:ℙ]. ∀[B:⋂a:A. ℙ].  (B supposing A ∈ ℙ)

Lemma: implies-wf
[A:ℙ]. ∀[B:⋂a:A. ℙ].  (A  B ∈ ℙ)

Definition: rev_uimplies
rev_uimplies(P;Q) ==  supposing Q

Lemma: rev_uimplies_wf
[P,Q:ℙ].  (rev_uimplies(P;Q) ∈ ℙ)

Definition: uiff
uiff(P;Q) ==  supposing P ∧ supposing Q

Lemma: uiff_wf
[P,Q:ℙ].  (uiff(P;Q) ∈ ℙ)

Lemma: iff_weakening_uiff
[P,Q:ℙ].  (uiff(P;Q)  (P ⇐⇒ Q))

Lemma: iff_weakening_equal
[A,B:Type].  {A ⇐⇒ B} supposing B ∈ Type

Lemma: implies_weakening_uimplies
[P,Q:ℙ].  (Q supposing  {P  Q})

Lemma: rev_implies_weakening_rev_uimplies
[P,Q:ℙ].  (rev_uimplies(P;Q)  {P  Q})

Lemma: uiff_functionality_wrt_uiff
[P1,P2,Q1,Q2:ℙ].  ({P1 ⇐⇒ P2}  {Q1 ⇐⇒ Q2}  {uiff(P1;Q1) ⇐⇒ uiff(P2;Q2)})

Lemma: uiff_functionality_wrt_uiff2
[P1,P2,Q1,Q2:ℙ].  ({P1 ⇐⇒ P2}  {Q1 ⇐⇒ Q2}  {uiff(P1;Q1) ⇐⇒ uiff(P2;Q2)})

Lemma: uimplies_functionality_wrt_uimplies
[P1,P2,Q1,Q2:ℙ].  ({P1 supposing P2}  {Q2 supposing Q1}  {Q1 supposing P1  Q2 supposing P2})

Lemma: uimplies_functionality_wrt_uiff
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  {uiff(Q1;Q2)}  {uiff(Q1 supposing P1;Q2 supposing P2)})

Lemma: uimplies-iff-squash-implies
[P,Q:ℙ].  (Q supposing ⇐⇒ (↓P)  Q)

Lemma: and_functionality_wrt_uimplies
[P1,P2,Q1,Q2:ℙ].  ({P2 supposing P1}  {Q2 supposing Q1}  {P2 ∧ Q2 supposing P1 ∧ Q1})

Lemma: and_functionality_wrt_rev_uimplies
[P1,P2,Q1,Q2:ℙ].  ({rev_uimplies(P1;P2)}  {rev_uimplies(Q1;Q2)}  {rev_uimplies(P1 ∧ Q1;P2 ∧ Q2)})

Lemma: and_functionality_wrt_uiff
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  {uiff(Q1;Q2)}  {uiff(P1 ∧ Q1;P2 ∧ Q2)})

Lemma: not_functionality_wrt_uimplies
[P,Q:ℙ].  ({P supposing Q}  supposing ¬P})

Lemma: not_functionality_wrt_uiff
[P,Q:ℙ].  ({uiff(P;Q)}  {uiff(¬P;¬Q)})

Lemma: uall_functionality_wrt_iff
[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀[x:S]. (P[x] ⇐⇒ Q[x]))  {∀[x:S]. P[x] ⇐⇒ ∀[y:T]. Q[y]} supposing T ∈ Type

Lemma: uimplies_antisymmetry
[P,Q:ℙ].  (Q supposing  supposing  uiff(P;Q))

Lemma: uimplies_transitivity
[P,Q,R:ℙ].  (Q supposing  supposing  {R supposing P})

Lemma: uiff_transitivity
[P,Q,R:ℙ].  (uiff(P;Q)  uiff(Q;R)  uiff(P;R))

Lemma: uiff_transitivity2
[P,Q,R:ℙ].  (uiff(P;Q)  (Q R ∈ ℙ uiff(P;R))

Lemma: uiff_transitivity3
[P,Q,R:ℙ].  ((P Q ∈ ℙ uiff(Q;R)  uiff(P;R))

Wf theorems for definitions introduced
in core_1 theory.  

Lemma: true_wf
True ∈ ℙ

Lemma: istype-true

Lemma: squash_wf
[A:ℙ]. (↓A ∈ ℙ)

Lemma: squash-test
[P:ℙ]. (P  (↓P))

Lemma: guard_wf
[T:Type]. ({T} ∈ Type)

Lemma: unit_wf
Unit ∈ Type

Lemma: not_wf
[A:ℙ]. A ∈ ℙ)

Lemma: member-not
[A:ℙ]. ∀[z:Top].  λx.z ∈ ¬supposing ¬A

Lemma: comb_for_not_wf
λA,z. A) ∈ A:ℙ ⟶ (↓True) ⟶ ℙ

Lemma: rev_implies_wf
[A,B:ℙ].  (A  B ∈ ℙ)

Lemma: comb_for_rev_implies_wf
λA,B,z. (A  B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ

Lemma: iff_wf
[A,B:ℙ].  (A ⇐⇒ B ∈ ℙ)

Lemma: comb_for_iff_wf
λA,B,z. (A ⇐⇒ B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ

Lemma: nequal_wf
[A:Type]. ∀[x,y:A].  (x ≠ y ∈ A  ∈ ℙ)

Lemma: member_wf
[A:Type]. ∀[a:A].  (a ∈ A ∈ Type)

Comment: COMBS_acom
Common Combinators

Definition: icomb
==  λx.x

Lemma: icomb_wf
[A:Type]. (I ∈ A ⟶ A)

Definition: kcomb
==  λx,y. x

Lemma: kcomb_wf
[A,B:Type].  (K ∈ A ⟶ B ⟶ A)

Definition: scomb
==  λx,y,z. (x (y z))

Lemma: scomb_wf
[A,B,C:Type].  (S ∈ (A ⟶ B ⟶ C) ⟶ (A ⟶ B) ⟶ A ⟶ C)

Comment: PRODUCT_DEFS_acom
Projection functions for pairs

Lemma: pi2_wf
[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (snd(p) ∈ B[fst(p)])

Lemma: pi1_wf
[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (fst(p) ∈ A)

Lemma: pair_eta_rw
[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (<fst(p), snd(p)> p ∈ (a:A × B[a]))

Lemma: respects-equality-product
[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].
   (∀a:Base. ((a ∈ A)  (a ∈ A')  respects-equality(B[a];B'[a])))
   respects-equality(a:A × B[a];a:A' × B'[a]))

Definition: spread3
let x,y,z in 
  z] ==
  let x,zz 
  in let y,z zz 
     in t[x;

Definition: spread4
let w,x,y,z 
in t[w;
     z]   ==
  let w,zz1 
  in let x,zz2 zz1 
     in let y,z zz2 
        in t[w;

Definition: spread5
let a,b,c,d,e in v[a;
                       e] ==
  let a,zz1 
  in let b,zz2 zz1 
     in let c,zz3 zz2 
        in let d,e zz3 
           in v[a;

Definition: spread6
let a,b,c,d,e,f in 
 f] ==
  let a,zz1 
  in let b,zz2 zz1 
     in let c,zz3 zz2 
        in let d,zz4 zz3 
           in let e,f zz4 
              in v[a;

Definition: spread7
let a,b,c,d,e,f,g in 
  g] ==
  let a,zz1 
  in let b,zz2 zz1 
     in let c,zz3 zz2 
        in let d,zz4 zz3 
           in let e,zz5 zz4 
              in let f,g zz5 
                 in v[a;

Lemma: all_functionality_wrt_uimplies
[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].
  (∀x:T. {Q[x] supposing P[x]})  {∀x:T. Q[x] supposing ∀x:S. P[x]} supposing T ∈ Type

Lemma: all_functionality_wrt_uiff
[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].
  (∀x:T. {uiff(P[x];Q[x])})  {uiff(∀x:S. P[x];∀x:T. Q[x])} supposing T ∈ Type

Comment: UNIT_DEFS_acom
Inhabitant of Unit type

Definition: it
⋅ ==  Ax

Definition: exposed-it
exposed-it ==  Ax

Lemma: it_wf
⋅ ∈ Unit

Lemma: unit_triviality
[a:Unit]. (a = ⋅ ∈ Unit)

Predicates for constructive properties of propositions, and
lemmas characterizing how these predicates are inherited.

Worthwhile sometime redoing thms for soft abstractions
in terms of the underlying hard abstractions primitives.

Definition: decidable
Dec(P) ==  P ∨ P)

Lemma: decidable_wf
[A:ℙ]. (Dec(A) ∈ ℙ)

Lemma: decidable__or
[P,Q:ℙ].  (Dec(P)  Dec(Q)  Dec(P ∨ Q))

Lemma: decidable__and
[P,Q:ℙ].  (Dec(P)  (P  Dec(Q))  Dec(P ∧ Q))

Lemma: decidable__and2
[P:ℙ]. ∀[Q:⋂:P. ℙ].  (Dec(P)  (P  Dec(Q))  Dec(P ∧ Q))

Lemma: decidable__implies
[P:ℙ]. ∀[Q:⋂p:P. ℙ].  (Dec(P)  (P  Dec(Q))  Dec(P  Q))

Lemma: decidable__false

Lemma: decidable__true

Lemma: decidable__not
[P:ℙ]. (Dec(P)  Dec(¬P))

Lemma: decidable__iff
[P,Q:ℙ].  (Dec(P)  Dec(Q)  Dec(P ⇐⇒ Q))

Lemma: atom_subtype_base
Atom ⊆Base

Lemma: decidable__atom_equal
a,b:Atom.  Dec(a b ∈ Atom)

Lemma: iff_preserves_decidability
[A,B:ℙ].  (Dec(A)  (A ⇐⇒ B)  Dec(B))

Definition: stable
Stable{P} ==  supposing ¬¬P

Lemma: stable_wf
[A:ℙ]. (Stable{A} ∈ ℙ)

Lemma: stable__not
[P:ℙ]. Stable{¬P}

Lemma: stable__false

Lemma: stable__and
[P,Q:ℙ].  (Stable{P}  Stable{Q}  Stable{P ∧ Q})

Lemma: stable__all
[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Stable{P[x]})  Stable{∀x:T. P[x]})

Lemma: stable__implies
[P,Q:ℙ].  (Stable{P}  Stable{Q  P})

Lemma: stable__function_equal
[A,B:Type]. ∀[f,g:A ⟶ B].  Stable{f g ∈ (A ⟶ B)} supposing ∀x:A. Stable{(f x) (g x) ∈ B}

Lemma: stable__from_decidable
[P:ℙ]. (Dec(P)  Stable{P})

Definition: sq_stable
SqStable(P) ==  (↓P)  P

Lemma: sq_stable_wf
[A:ℙ]. (SqStable(A) ∈ ℙ)

Lemma: sq_stable_functionality
[A,B:ℙ].  ((A ⇐⇒ B)  (SqStable(A) ⇐⇒ SqStable(B)))

Lemma: sq_stable__and
[P:ℙ]. ∀[Q:⋂p:P. ℙ].  (SqStable(P)  (P  SqStable(Q))  SqStable(P ∧ Q))

Lemma: sq_stable__implies
[P,Q:ℙ].  (SqStable(Q)  SqStable(P  Q))

Lemma: sq_stable__uimplies
[P,Q:ℙ].  (SqStable(Q)  SqStable(Q supposing P))

Lemma: sq_stable__iff
[P,Q:ℙ].  (SqStable(P)  SqStable(Q)  SqStable(P ⇐⇒ Q))

Lemma: sq_stable__uiff
[P,Q:ℙ].  (SqStable(P)  SqStable(Q)  SqStable(uiff(P;Q)))

Lemma: sq_stable__all
[A:Type]. ∀[P:A ⟶ ℙ].  ((∀x:A. SqStable(P[x]))  SqStable(∀x:A. P[x]))

Lemma: sq_stable__uall
[A:Type]. ∀[P:A ⟶ ℙ].  ((∀[x:A]. SqStable(P[x]))  SqStable(∀[x:A]. P[x]))

Lemma: sq_stable__equal
[A:Type]. ∀[x,y:A].  SqStable(x y ∈ A)

Lemma: sq_stable__squash
[P:ℙ]. SqStable(↓P)

Lemma: sq_stable__from_stable
[P:ℙ]. (Stable{P}  SqStable(P))

Lemma: sq_stable__not
[P:ℙ]. SqStable(¬P)

Lemma: sq_stable_from_decidable
[P:ℙ]. (Dec(P)  SqStable(P))

Lemma: sq_stable__respects-equality
[A,B:Type].  SqStable(respects-equality(A;B))

Lemma: uiff_weakening
[P:ℙ]. (SqStable(P)  {uiff(P;P)})

Definition: xmiddle
XM ==  ∀P:ℙDec(P)

Lemma: xmiddle_wf
XM ∈ ℙ'

Definition: weak-xmiddle
WeakXM ==  ∀P:ℙ(↓Dec(P))

Lemma: weak-xmiddle_wf
WeakXM ∈ ℙ'

Lemma: xmiddle-implies-stable
XM  (∀P:ℙStable{P})

Lemma: sq_stable_iff_stable
XM  (∀P:ℙ(SqStable(P) ⇐⇒ Stable{P}))

Lemma: squash_elim
[P:ℙ]. (SqStable(P)  (↓⇐⇒ P))

Lemma: sq_stable_iff_uimplies
[P:ℙ]. (SqStable(P) ⇐⇒ supposing P)

Comment: LOGIC_THMS_tcom
Theorems of inituitionistic propositional and 
predicate logic. 

Lemma: dneg_elim
[A:ℙ]. (Dec(A)  supposing ¬¬A)

Lemma: dneg_elim_a
[A:ℙ]. (Dec(A)  (¬¬⇐⇒ A))

Lemma: iff_symmetry
[A,B:ℙ].  (A ⇐⇒ ⇐⇒ ⇐⇒ A)

Lemma: and_assoc
[A,B,C:ℙ].  (A ∧ B ∧ ⇐⇒ (A ∧ B) ∧ C)

Lemma: and_comm
[A,B:ℙ].  (A ∧ ⇐⇒ B ∧ A)

Lemma: or_assoc
[A,B,C:ℙ].  (A ∨ B ∨ ⇐⇒ (A ∨ B) ∨ C)

Lemma: or_comm
[A,B:ℙ].  (A ∨ ⇐⇒ B ∨ A)

Lemma: not_over_or
[A,B:ℙ].  uiff(¬(A ∨ B);(¬A) ∧ B))

Lemma: not_over_or_a
[A,B:ℙ].  uiff(¬(A ∨ B);{(¬A) ∧ B)})

Lemma: not_over_and_b
[A,B:ℙ].  ¬(A ∧ B) supposing A) ∨ B)

Lemma: not_over_and
[A,B:ℙ].  (Dec(A)  (A ∧ B) ⇐⇒ A) ∨ B)))

Lemma: not_over_not
[A:ℙ]. (Dec(A)  (¬¬⇐⇒ A))

Lemma: not_over_implies
[A,B:ℙ].  (A  B) ⇐⇒ (¬¬A) ∧ B))

Lemma: and_false_l
[A:Top]. (False ∧ ⇐⇒ False)

Lemma: and_false_r
[A:ℙ]. (A ∧ False ⇐⇒ False)

Lemma: and_true_l
[A:ℙ]. (True ∧ ⇐⇒ A)

Lemma: and_true_r
[A:ℙ]. (A ∧ True ⇐⇒ A)

Lemma: or_false_l
[A:ℙ]. (False ∨ ⇐⇒ A)

Lemma: or_false_r
[A:ℙ]. (A ∨ False ⇐⇒ A)

Lemma: or_true_l
[A:ℙ]. (True ∨ ⇐⇒ True)

Lemma: or_true_r
[A:ℙ]. (A ∨ True ⇐⇒ True)

Lemma: exists_over_and_r
[T:Type]. ∀[A:ℙ]. ∀[B:T ⟶ ℙ].  (∃x:T. (A ∧ B[x]) ⇐⇒ A ∧ (∃x:T. B[x]))

Lemma: not_over_exists
[T:Type]. ∀[Q:T ⟶ ℙ].  uiff(¬(∃x:T. Q[x]);∀x:T. Q[x]))

Lemma: not_over_exists_uniform
[T:Type]. ∀[Q:T ⟶ ℙ].  uiff(¬(∃x:T. Q[x]);∀[x:T]. Q[x]))

Lemma: triple-neg
[A:ℙ]. uiff(¬¬¬A;¬A)

Lemma: non-uniform-triple-neg
A:ℙ(¬¬¬⇐⇒ ¬A)

Lemma: minimal-triple-neg
[E:Type]. ∀[A:ℙ].  (((A  E)  E)  ⇐⇒  E)

Lemma: triple-neg-ext
[A:ℙ]. uiff(¬¬¬A;¬A)

Lemma: non-uniform-triple-neg-ext
A:ℙ(¬¬¬⇐⇒ ¬A)

Lemma: minimal-triple-neg-ext
[E:Type]. ∀[A:ℙ].  (((A  E)  E)  ⇐⇒  E)

Comment: EQUALITY_THMS_tcom
Equality Theorems

Lemma: equal_symmetry
[T:Type]. ∀[x,y:T].  uiff(x y ∈ T;y x ∈ T)

Lemma support for rewriting.

Lemma: iff_transitivity
[P,Q,R:ℙ].  ((P ⇐⇒ Q)  (Q ⇐⇒ R)  (P ⇐⇒ R))

Lemma: implies_transitivity
[P,Q,R:ℙ].  ((P  Q)  (Q  R)  {P  R})

Lemma: and_functionality_wrt_iff
[P1,P2,Q1,Q2:ℙ].  ((P1 ⇐⇒ P2)  (Q1 ⇐⇒ Q2)  (P1 ∧ Q1 ⇐⇒ P2 ∧ Q2))

Lemma: and_functionality_wrt_implies
[P1,P2,Q1,Q2:ℙ].  ({P1  P2}  {Q1  Q2}  {(P1 ∧ Q1)  (P2 ∧ Q2)})

Lemma: and_functionality_wrt_uiff2
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  (Q1 Q2 ∈ ℙ {P1 ∧ Q1 ⇐⇒ P2 ∧ Q2})

Lemma: and_functionality_wrt_uiff3
[P1,P2,Q1,Q2:ℙ].  ((P1 P2 ∈ ℙ {uiff(Q1;Q2)}  {P1 ∧ Q1 ⇐⇒ P2 ∧ Q2})

Lemma: implies_functionality_wrt_iff
[P1,P2,Q1,Q2:ℙ].  ({P1 ⇐⇒ P2}  {Q1 ⇐⇒ Q2}  {P1  Q1 ⇐⇒ P2  Q2})

Lemma: implies_functionality_wrt_implies
[P1,P2,Q1,Q2:ℙ].  ({P1  P2}  {Q1  Q2}  {(P1  Q1)  P2  Q2})

Lemma: decidable_functionality
[P,Q:ℙ].  ((P ⇐⇒ Q)  (Dec(P) ⇐⇒ Dec(Q)))

Lemma: iff_functionality_wrt_iff
[P1,P2,Q1,Q2:ℙ].  ((P1 ⇐⇒ P2)  (Q1 ⇐⇒ Q2)  (P1 ⇐⇒ Q1 ⇐⇒ P2 ⇐⇒ Q2))

Lemma: all_functionality_wrt_iff
[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀x:S. (P[x] ⇐⇒ Q[x]))  (∀x:S. P[x] ⇐⇒ ∀y:T. Q[y]) supposing T ∈ Type

Lemma: all_functionality_wrt_implies
[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀z:S. {P[z]  Q[z]})  {(∀x:S. P[x])  (∀y:T. Q[y])} supposing T ∈ Type

Lemma: exists_functionality_wrt_iff
[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀x:S. (P[x] ⇐⇒ Q[x]))  (∃x:S. P[x] ⇐⇒ ∃y:T. Q[y]) supposing T ∈ Type

Lemma: exists_functionality_wrt_implies
[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀x:S. {P[x]  Q[x]})  {(∃x:S. P[x])  (∃y:T. Q[y])} supposing T ∈ Type

Lemma: not_functionality_wrt_iff
[P,Q:ℙ].  ⇐⇒ ¬Q} supposing ⇐⇒ Q

Lemma: not_functionality_wrt_implies
[P,Q:ℙ].  {(¬P)  Q)} supposing {P  Q}

Lemma: or_functionality_wrt_iff
[P1,P2,Q1,Q2:ℙ].  ({P1 ⇐⇒ P2}  {Q1 ⇐⇒ Q2}  {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})

Lemma: or_functionality_wrt_uiff
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  {uiff(Q1;Q2)}  {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})

Lemma: or_functionality_wrt_uiff2
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  (Q1 Q2 ∈ ℙ {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})

Lemma: or_functionality_wrt_uiff3
[P1,P2,Q1,Q2:ℙ].  ((P1 P2 ∈ ℙ {uiff(Q1;Q2)}  {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})

Lemma: union_functionality_wrt_iff
[P1,P2,Q1,Q2:ℙ].  ({P1 ⇐⇒ P2}  {Q1 ⇐⇒ Q2}  {P1 Q1 ⇐⇒ P2 Q2})

Lemma: union_functionality_wrt_uiff
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  {uiff(Q1;Q2)}  {P1 Q1 ⇐⇒ P2 Q2})

Lemma: union_functionality_wrt_uiff2
[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)}  (Q1 Q2 ∈ ℙ {P1 Q1 ⇐⇒ P2 Q2})

Lemma: union_functionality_wrt_uiff3
[P1,P2,Q1,Q2:ℙ].  ((P1 P2 ∈ ℙ {uiff(Q1;Q2)}  {P1 Q1 ⇐⇒ P2 Q2})

Lemma: and-iff
[A:ℙ]. ∀[B,C:⋂a:A. ℙ].  ((A  (B ⇐⇒ C))  {A ∧ ⇐⇒ A ∧ C})

Definition: sq_or
a ↓∨ ==  ↓a ∨ b

Lemma: sq_or_wf
[a,b:ℙ].  (a ↓∨ b ∈ ℙ)

Lemma: sq_stable__sq_or
[a,b:ℙ].  SqStable(a ↓∨ b)

Lemma: sq_or_simp
[a:ℙ]. ({uiff(a ↓∨ False;↓a)} ∧ {uiff(False ↓∨ a;↓a)} ∧ {uiff(a ↓∨ True;True)} ∧ {uiff(True ↓∨ a;True)})

Lemma: sq_or_sq_or
[a,b,c:ℙ].  ({uiff(a ↓∨ b ↓∨ c;a ↓∨ (b ∨ c))} ∧ {uiff((b ↓∨ c) ↓∨ a;(b ∨ c) ↓∨ a)})

Lemma: sq_or_functionality_wrt_iff
[P1,P2,Q1,Q2:ℙ].  ({P1 ⇐⇒ P2}  {Q1 ⇐⇒ Q2}  {P1 ↓∨ Q1 ⇐⇒ P2 ↓∨ Q2})

Lemma: squash_squash
[a:ℙ]. uiff(↓↓a;↓a)

Lemma: squash_true

Lemma: squash_false

Lemma: sq_or_squash
[a,b:ℙ].  uiff((↓a) ↓∨ (↓b);a ↓∨ b)

Lemma: squash_sq_or
[a,b:ℙ].  uiff(↓a ↓∨ b;a ↓∨ b)

Lemma: sq_or_squash2
[a,b:ℙ].  uiff((↓a) ↓∨ b;a ↓∨ b)

Lemma: sq_or_squash3
[a,b:ℙ].  uiff(a ↓∨ (↓b);a ↓∨ b)

Lemma: squash_and
[a,b:ℙ].  uiff(↓a ∧ b;(↓a) ∧ (↓b))

Lemma: squash_not
[p:ℙ]. uiff(↓¬p;¬p)

Lemma: not_squash
[p:ℙ]. uiff(¬↓p;¬p)

Lemma: squash_equal
[T:Type]. ∀[x,y:T].  uiff(↓y ∈ T;x y ∈ T)

Lemma: uimplies_functionality_wrt_uiff2
[P,Q1,Q2:ℙ].  ({uiff(Q1;Q2)}  {uiff(Q1 supposing P;Q2 supposing P)})

Lemma: uimplies_functionality_wrt_uiff3
[P,Q1,Q2:ℙ].  (Dec(P)  {uiff(Q1;Q2)}  {uiff(P supposing Q1;P supposing Q2)})

Lemma: or_functionality_wrt_implies
[P1,P2,Q1,Q2:ℙ].  ({P1  P2}  {Q1  Q2}  {(P1 ∨ Q1)  (P2 ∨ Q2)})

Lemma: squash_functionality_wrt_implies
[P,Q:ℙ].  ({P  Q}  {(↓P)  (↓Q)})

Lemma: squash_functionality_wrt_iff
[P,Q:ℙ].  ({P ⇐⇒ Q}  {↓⇐⇒ ↓Q})

Lemma: squash_functionality_wrt_uiff
[P,Q:ℙ].  ({P ⇐⇒ Q}  {uiff(↓P;↓Q)})

Lemma: implies_antisymmetry
[P,Q:ℙ].  ((P  Q)  (Q  P)  (P ⇐⇒ Q))


Lemma: gen_hyp_tp
[A:Type]. ∀[e:A]. ∀[H:A ⟶ 𝕌{j}]. ∀[z:H e].  {{{False  True}}}

Comment: MISC_DEFS_com
Miscellaneous General Definitions

Definition: let
let in b[x] ==  x.b[x]) a

Lemma: let_wf
[A,B:Type]. ∀[f:A ⟶ B]. ∀[x:A].  (let in f[v] ∈ B)

Comment: type_inj_acom
type_inj is intended chiefly for injecting into quotient
types. For convenience, typing lemmas should be proven
for each application. e.g. 

... ∀x:T. [x]{a,b:T//Eab}

general typing lemma for type_inj(x;T) cannot
be proven, because it's antecedent would involve the subtype
predicate which isn't typeable.

Definition: type_inj
[x]{T} ==  x

Comment: choicef_com
Hilbert choice operator. Set up for use in theorems where
assume_xm abstraction is used outermost. 

Select the correctly instantiated display form by entering the 
editor alias "eps". This display form contains variable that
is bound by assume_xm.

Sequent display routine needs fixing, so that pretty choicef 
display form is used when XM becomes explicit hypothesis. 

Definition: choicef
x:T. P[x] ==  case xm {y:T| P[y]}  of inl(z) => inr(w) => "???"

Lemma: choicef_wf
[xm:XM]. ∀[T:Type]. ∀[P:T ⟶ ℙ].  ∈x:T. P[x] ∈ supposing ∃a:T. P[a]

Lemma: fun_thru_spread
[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C,D:Type]. ∀[f:C ⟶ D]. ∀[b:x:A ⟶ B[x] ⟶ C].
  ((f let x,y in b[x;y]) let x,y in b[x;y] ∈ D)

Lemma: spread_to_pi12
[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C:Type]. ∀[b:x:A ⟶ B[x] ⟶ C].
  (let x,y in b[x;y] b[fst(p);snd(p)] ∈ C)

Definition: singleton
{a:T} ==  {x:T| a ∈ T} 

Lemma: singleton_wf
[T:Type]. ∀[a:T].  ({a:T} ∈ Type)

Lemma: singleton_properties
[T:Type]. ∀[a:T]. ∀[x:{a:T}].  (x a ∈ T)

Definition: unique_set
{!x:T P[x]} ==  {x:T| P[x] ∧ (∀y:T. (P[y]  (y x ∈ T)))} 

Lemma: unique_set_wf
[T:Type]. ∀[P:T ⟶ ℙ].  ({!x:T P[x]} ∈ Type)

Definition: uni_sat
!x:T. Q[x] ==  Q[a] ∧ (∀a':T. (Q[a']  (a' a ∈ T)))

Lemma: uni_sat_wf
[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ].  (a !x:T. Q[x] ∈ ℙ)

Lemma: uni_sat_imp_in_uni_set
[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ].  ((a !x:T. Q[x])  (a ∈ {!x:T Q[x]}))

Lemma: sq_stable__uni_sat
[T:Type]. ∀a:T. ∀[Q:T ⟶ ℙ]. ((∀x:T. SqStable(Q[x]))  SqStable(a !x:T. Q[x]))

Lemma: comb_for_pi1_wf
λA,B,p,z. (fst(p)) ∈ A:Type ⟶ B:(A ⟶ Type) ⟶ p:(a:A × B[a]) ⟶ (↓True) ⟶ A

Lemma: image-type_wf
[A:Type]. ∀[f:Base].  (Image(A,f) ∈ Type)

Lemma: int_eq_wf
[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ].  (if x=y then else b ∈ T)

Lemma: atom_eq_wf
[T:Type]. ∀[a,b:T]. ∀[x,y:Atom].  (if x=y then else fi  ∈ T)

Lemma: not-0-eq-1
¬(0 1 ∈ ℤ)

Definition: baseof
baseof(T) ==  ⋂x:Unit?. case of inl(z) => inr(z) => Base

Lemma: baseof_wf
[T:Type]. (baseof(T) ∈ Type)

Lemma: equal-top
[x,y:Top].  (x y ∈ Top)

Lemma: equal-unit
[x,y:Unit].  (x y ∈ Unit)

Lemma: decidable__squash
[p:ℙ]. (Dec(p)  Dec(↓p))

Lemma: squash_thru_implies_dec
[P,Q:ℙ].  uiff(↓ Q;P  (↓Q)) supposing Dec(P)

Lemma: equality-test
[A,B,C:Type].  ((A B ∈ Type)  (C B ∈ Type)  (∀[x,y,z:A].  ((x y ∈ A)  (z y ∈ A)  (x z ∈ C))))

Lemma: equality-test2
  ((A B ∈ Type)
   (C B ∈ Type)
   (∀[f:A ⟶ A]. ∀[x,y,z,u,w:A].  ((x (f y) ∈ A)  (z (f y) ∈ A)  (w u ∈ C)  (w z ∈ C)  (u x ∈ C))))

Lemma: or-to-and-by-cases
[X:ℙ]. (Dec(X)  (∀[P,Q:ℙ].  ((P  X)  (Q  X))  {P ∨ ⇐⇒ (X  P) ∧ ((¬X)  Q)})))

Definition: exists!
!x:T. P[x] ==  ∃x:T. (P[x] ∧ (∀y:T. (P[y]  (y x ∈ T))))

Lemma: exists!_wf
[T:Type]. ∀[P:T ⟶ ℙ].  (∃!x:T. P[x] ∈ ℙ)

Lemma: less-member
[T:Type]. ∀[n,m:ℤ]. ∀[a,b:T].  (if (n) < (m)  then a  else b ∈ T)

Definition: less_than'
At one time, ⌜a < b⌝ was primitive type, and the equality rule for it
said that ⌜a < b⌝ was type if ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝.
An elimination rule said that if ⌜t ∈ a < b⌝ then ⌜Ax⌝.
All of these properties are easily derivable if we simply define
a < b⌝ using the primitive `less` comparison operator
  ⌜if (a) < (b)  then True  else False⌝
However, from the fact that ⌜if (a) < (b)  then True  else False⌝ 
is proposition (even when we know that it is true proposition)
it does not follow that ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝ because, for example
from  a:⇃({...3}), b:⇃({4...}) we can prove that
if (a) < (b)  then True  else False ∈ ℙ⌝.
Therefore, we call ⌜if (a) < (b)  then True  else False⌝ ⌜less_than'(a;b)⌝
and reserve ⌜a < b⌝ for the proposition that includes ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝⋅

less_than'(a;b) ==  if (a) < (b)  then True  else False

Lemma: less_than'_wf
[a,b:ℤ].  (less_than'(a;b) ∈ ℙ)

Definition: less_than
At one time, ⌜a < b⌝ was primitive type but the properties we need all
follow from the definition of ⌜less_than'(a;b)⌝ except for the
property that from ⌜a < b⌝ we can derive ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝.
So we simply add those to the definition.. 

a < ==  ↓less_than'(a;b) ∧ (a ∈ ℤ) ∧ (b ∈ ℤ)

Lemma: less_than_wf
[a,b:ℤ].  (a < b ∈ ℙ)

Lemma: istype-less_than
[a,b:ℤ].  istype(a < b)

Lemma: less_wf
[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ].  (if (x) < (y)  then a  else b ∈ T)

Lemma: int_subtype_base
ℤ ⊆Base

Lemma: unit_subtype_base
Unit ⊆Base

Lemma: decidable__equal_set
[T:Type]. ((∀x,y:T.  Dec(x y ∈ T))  (∀[P:T ⟶ Type]. ∀x,y:{x:T| P[x]} .  Dec(x y ∈ {x:T| P[x]} )))

Lemma: decidable__equal_unit
x,y:Unit.  Dec(x y ∈ Unit)

Lemma: test-compute-all
(1 3) 12

Lemma: minimal-example1
[A,B,X:ℙ].  ((((A  B)  X)  X)  ((A  X)  X)  (B  X)  X)

Lemma: minimal-example1-ext
[A,B,X:ℙ].  ((((A  B)  X)  X)  ((A  X)  X)  (B  X)  X)

Lemma: not-not-p-or-not-p
P,A:ℙ.  (((P ∨ (P  A))  A)  A)

Lemma: not-not-p-or-not-p-example
P:ℙ(¬¬(P ∨ P)))

Lemma: not-not-p-or-not-p-prgram
P,A:ℙ.  (((P ∨ (P  A))  A)  A)

Lemma: curry-lemma
A,B,C:ℙ.  (((A ∧ B)  C)    C)

Lemma: curry-lemma-program
A,B,C:ℙ.  (((A ∧ B)  C)    C)

Lemma: minimal-not-not-xmiddle
[P,A:ℙ].  (((P ∨ (P  A))  A)  A)

Lemma: not-not-1-xmiddle
[P:ℙ]. (¬¬(P ∨ P)))

Lemma: minimal-not-not-implies
[P,A:ℙ].  (((((P  A)  A)  (P ∨ A))  A)  A)

Lemma: minimal-not-not-implies-program
[P,A:ℙ].  (((((P  A)  A)  (P ∨ A))  A)  A)

Lemma: minimal-not-not-implies-from-program
[P,A:ℙ].  (((((P  A)  A)  (P ∨ A))  A)  A)

Lemma: example
[P,A:ℙ].  (((P ∨ (P  A))  A)  A)

Lemma: minimal-not-not-xmiddle-program
[P,A:ℙ].  (((P ∨ (P  A))  A)  A)

Lemma: minimal-not-not-xmiddle-from-program
[P,A:ℙ].  (((P ∨ (P  A))  A)  A)

Home Index