Definition: forall
x.P[x] ==  ∀x:Dom. P[x]

Lemma: forall_wf
[A:Type]. ∀[B:A ─→ ℙ].  (∀a.B[a] ∈ ℙ)

Definition: forsome
x.P[x] ==  ∃x:Dom. P[x]

Lemma: forsome_wf
[A:Type]. ∀[B:A ─→ ℙ].  (∃a.B[a] ∈ ℙ)

Definition: language1
language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ==
  ∀[D:Type]. ∀[A:ℙ]. ∀[B,C:D ─→ ℙ]. ∀[P,Q,R:D ─→ D ─→ ℙ]. ∀[H:D ─→ D ─→ D ─→ ℙ].  fml[D;A;B;C;P;Q;R;H]

Lemma: language1_wf
[fml:D:Type ─→ ℙ ─→ (D ─→ ℙ) ─→ (D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ D ─→ ℙ) ─→ ℙ]
  (language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ∈ ℙ')

Definition: TC
TC(λx,y.F[x; y])(a,b) ==  TC(λx,y. F[x; y]) b

Lemma: TC_wf
[Dom:Type]. ∀[F:Dom ─→ Dom ─→ ℙ]. ∀[a,b:Dom].  (TC(λx,y.F[x;y])(a,b) ∈ ℙ)

Lemma: TC-ind
[Dom:Type]. ∀[B:Dom ─→ ℙ]. ∀[R:Dom ─→ Dom ─→ ℙ].
  ((∀x,y:Dom.  ((R y)  (B x)  (B y)))  (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (B x)  (B y))))

Lemma: TC-min
[Dom:Type]. ∀[R,Q:Dom ─→ Dom ─→ ℙ].
  ((∀x,y,z:Dom.  ((Q y)  (Q z)  (Q z)))
   (∀x,y:Dom.  ((R y)  (Q y)))
   (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (Q y))))

Lemma: TC-min-uniform
[Dom:Type]. ∀[R,Q:Dom ─→ Dom ─→ ℙ].
  ((∀[x,y,z:Dom].  ((Q y)  (Q z)  (Q z)))
   (∀x,y:Dom.  ((R y)  (Q y)))
   (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (Q y))))

Lemma: TC-trans
[Dom:Type]. ∀[R:Dom ─→ Dom ─→ ℙ]. ∀[x,y,z:Dom].  (TC(λa,b.R b)(x,y)  TC(λa,b.R b)(y,z)  TC(λa,b.R b)(x,z))

Lemma: TC-base
[Dom:Type]. ∀[R:Dom ─→ Dom ─→ ℙ].  ∀x,y:Dom.  ((R y)  TC(λa,b.R b)(x,y))

Lemma: TC-ind-ext
[Dom:Type]. ∀[B:Dom ─→ ℙ]. ∀[R:Dom ─→ Dom ─→ ℙ].
  ((∀x,y:Dom.  ((R y)  (B x)  (B y)))  (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (B x)  (B y))))

Lemma: fo-logic-test1
x.(B x)  (C x)  ∃x.B  ∃x.C x

Lemma: example2
x.(B x)  (C x)  ∃z.B  ∃y.C y

Lemma: fo-logic-xmiddle
x:Dom. ((((B x) ∨ ((B x)  A))  A)  A)

Lemma: fo-logic-test2
x:Dom. ((B x)  (B x))

Lemma: ancestral-logic-lemma1
x,y:Dom.  (TC(λa,b.R b)(x,y)  ((R y) ∨ (∃z:Dom. ((R z) ∧ TC(λa,b.R b)(z,y)))))

Lemma: ancestral-logic-induction
(∀x,y:Dom.  ((R y)  (B x)  (B y)))  (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (B x)  (B y)))

Lemma: ancestral-logic-induction-ext
(∀x,y:Dom.  ((R y)  (B x)  (B y)))  (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (B x)  (B y)))

Lemma: ancestral-logic-example1
(∀x,y:Dom.  ((P y)  (Q y)))  (∀x,y:Dom.  (TC(λa,b.P b)(x,y)  TC(λa,b.Q b)(x,y)))

Lemma: ancestral-logic-example1-ext
(∀x,y:Dom.  ((P y)  (Q y)))  (∀x,y:Dom.  (TC(λa,b.P b)(x,y)  TC(λa,b.Q b)(x,y)))

Lemma: ancestral-logic-example2
x,y:Dom.  (TC(λa,b.TC(λi,j.P j)(a,b))(x,y)  TC(λa,b.P b)(x,y))

Lemma: ancestral-logic-example2-ext
x,y:Dom.  (TC(λa,b.TC(λi,j.P j)(a,b))(x,y)  TC(λa,b.P b)(x,y))

Definition: DNSF
DNSF(isphi;K;n;v) ==  fix((λDNSF,isphi. if isphi then x.(DNSF ff x)) else λx.if x <then v.x else λz.Ax fi  fi ))\000C isphi



Home Index