---

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]) a 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 x y) ⇒ (B x) ⇒ (B y))) ⇒ (∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))))

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

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

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

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

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

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

Lemma: example2
∀x.(B x) ⇒ (C x) ⇒ ∃z.B z ⇒ ∃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 a b)(x,y) ⇒ ((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))))

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

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

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

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

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

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

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



Home Index