---

Definition: atomn def
Atom$n ==  PRIMITIVE

Definition: atomeqn def
if a=$n b then x else y ==  PRIMITIVE

Definition: token1 def
'$x'1 ==  PRIMITIVE

Definition: token2 def
'$x'2 ==  PRIMITIVE

Lemma: atom1_subtype_base
Atom1 ⊆r Base

Lemma: atom2_subtype_base
Atom2 ⊆r Base

Lemma: atom1_sq
SQType(Atom1)

Lemma: atom2_sq
SQType(Atom2)

Definition: eq_atomn
eq_atom$n(x;y) ==  if x=$n y then tt else ff

Lemma: eq_atom_wf1
∀[x,y:Atom1].  (x =a1 y ∈ 𝔹)

Lemma: eq_atom_wf2
∀[x,y:Atom2].  (x =a2 y ∈ 𝔹)

Lemma: decidable__atom_equal_1
∀a,b:Atom1.  Dec(a = b ∈ Atom1)

Lemma: decidable__atom_equal_2
∀a,b:Atom2.  Dec(a = b ∈ Atom2)

Lemma: assert_of_eq_atom1
∀[x,y:Atom1].  uiff(↑x =a1 y;x = y ∈ Atom1)

Lemma: eq_atom1_self
∀[x:Atom1]. (x =a1 x ~ tt)

Lemma: assert_of_eq_atom2
∀[x,y:Atom2].  uiff(↑x =a2 y;x = y ∈ Atom2)

Lemma: eq_atom2_self
∀[x:Atom2]. (x =a2 x ~ tt)

Lemma: neg_assert_of_eq_atom1
∀[x,y:Atom1].  uiff(¬↑x =a1 y;x ≠ y ∈ Atom1 )

Lemma: atom-test1
'xxx'1 =a1 'yyy'1 = ff

Definition: free-from-atom
The type ⌜a#x:T⌝ is inhabited (by ⌜Ax⌝) 
iff there exists a token "a" and a term y such that a = "a" in Atom{$n} and x = y in T 
such that token "a" does not occur in y.

Thus a#x:T is true iff a is an atom and there is some member of the equivalence class of x in T
that is free from a.

To see that this defines a type, we note that if a1 = a2 in Atom{n}, then there is a unique token "a" such that
"a" = a1 = a2 in Atom{n}, and if T1 = T2 in Universe{i} and x1 = x2 in T1,
then any y such that x1 = y in T1 and "a" does not occur in y also satisfies
x2 = y in T2 and "a" does not occur in y.

Thus we justify the rule for equality: freeFromAtomEquality .

One base case is ⌜a#a:Atom$n⌝ where a ∈ Atom$n. This is not inhabited because every term y = a in Atom$n 
must mention the token "a" = a  (otherwise we could permute ("a","b") and get y = "b" and hence "b"="a").
Since ⌜a#a:Atom$n⌝ is not a type unless ⌜a ∈ Atom$n⌝, if we have ⌜a#a:Atom$n⌝ as a hypothesis in a sequent
then a ∈ Atom$n, then since a#a:Atom$n is not inhabited, the sequent is trivially true.
We thus have the "absurdity rule"" freeFromAtomAbsurdity .

Another base case is that if ⌜atom-free{$n:n}(T; x)⌝ then ⌜Ax ∈ a#x:T⌝. This is because atom-free{$n:n}(T; x)
 is, by definition,
∀a,b:Atom$n.  (swap-atoms{$n:n}(a; b; x) = x)
, so we may choose b to be "fresh" w.r.t. x (i.e. an atom not occuring in x)
and take y = swap-atoms{$n:n}(a; b; x) = x, then whatever token "a" the atom a evaluates to, will not occur in 
swap-atoms{$n:n}(a; b; x).
So, we have the first triviality rule: freeFromAtomTriviality .

The last base case is when x is an atom the is not equal to a. freeFromAtomBase .

Finally, if ⌜a#x:A⌝ and ⌜a#f:u:A ⟶ B[u]⌝ then 
then for some token "a", "a" = a in Aton{n}, and there are x' = x in A and
f' = f in u:A ⟶ B[u] such that "a" does not occur in f' or x'.
Then (f' x') = (f x) in B[x], and "a" does not occur in f' x'. Therefore, ⌜a#f x:B[x]⌝.
So we have shown that the application rule freeFromAtomApplication is true.

Note that the contrapositive of the application rule in the form
⌜(¬a#f x:B[x]) ⇒ ((¬a#f:u:A ⟶ B[u]) ∨ (¬a#x:A))⌝ will not be constructively true.
We define ⌜inheres{n:n}(T; x; a)⌝ to be the negation, ⌜¬a#x:A⌝, and we read it as "a is inherent in x:T".
It says that it is not possible to find a representative of x in T which avoids "a", i.e. that
every member of the equivalence class of x in T must mention the atom a.
Now, if f x must mention a, there can't be representatives f' and x' of f and x which don't mention a,
so at least one of f or x has no such representative. But since the number of possible representatives is
infinite, we can't in general decide which of them has this property.
So we don't have ⌜inheres{n:n}(B[x]; f x; a) ⇒ (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝ in general. 

We tried to define inherence as ⌜inheres{$n:n}(T; x; a) ==  ∃g:T ⟶ 𝔹. (↑matters{$n:n}(a; g; x))⌝ where 
⌜matters{$n:n}(a; g; x)⌝ (read as "matters"(a,g,x))
was a boolean (provided ⌜atom-free{n:n}(Type; T)⌝) defined by (nu b. ⌜¬bg x =b g swap-atoms{n:n}(a; b; x)⌝).
Here, nu b. X[b] means choose a fresh atom b not occring in X and evaluate X[b] to normal form (a boolean in our case)
and evalute to that normal form if it does not mention the fresh b and diverge otherwise.

From this definition we could prove (for types that were atom-free) the strong application inherence property
⌜inheres{n:n}(B[x]; f x; a) ⇒ (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝
 from a purported property of "matters" called
"conservation of matters". Unfortunately, the "conservation of matters" property is not true, as shown by the following
counter-example.
Let g <x,y> = ⌜¬b(x =a y ∧b (¬bx =a "a"))⌝,
let f = ⌜λx.<"a", x>⌝,
let x = "a".
Then g (f x) = g <"a","a"> = ⌜tt⌝.
Any tokens "b", "c" different from "a" do not occur in "a",g,f, or x, and
g (f swap-atoms{$n:n}(a; b; x)) = g <"a","b"> = ⌜tt⌝
g (swap-atoms{$n:n}(a; b; f) x) = g <"b","a"> = ⌜tt⌝
g (swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; c; x)) = g <"b","c"> = ⌜tt⌝, but
g (swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; b; x) ) = g <"b","b"> = ⌜ff⌝.
This example show that it is possible that 
⌜(↑matters{$n:n}(a; g; f x))
 ∧ (¬↑matters{$n:n}(a; λX.(g (f X)); x))
 ∧ (¬↑matters{$n:n}(a; λF.(g (F x)); f))
 ∧ (¬↑matters{$n:n}(a; λF.matters{$n:n}(a; λX.(g (F X)); x); f))⌝
whereas "conservation of matters" purported to show that
⌜(↑matters{$n:n}(a; g; f x)) ⇒ (((↑matters{$n:n}(a; λX.(g (f X)); ...)) ∨ ...) ∨ ...)⌝...

a#x:T ==  PRIMITIVE

Comment: free-from-atom doc
The type ⌜a#x:T⌝ is inhabited (by ⌜Ax⌝) 
iff there exists a token "a" and a term y such that a = "a" in Atom{$n} and x = y in T 
such that token "a" does not occur in y.

Thus a#x:T is true iff a is an atom and there is some member of the equivalence class of x in T
that is free from a.

To see that this defines a type, we note that if a1 = a2 in Atom{n}, then there is a unique token "a" such that
"a" = a1 = a2 in Atom{n}, and if T1 = T2 in Universe{i} and x1 = x2 in T1,
then any y such that x1 = y in T1 and "a" does not occur in y also satisfies
x2 = y in T2 and "a" does not occur in y.

Thus we justify the rule for equality: freeFromAtomEquality .

One base case is ⌜a#a:Atom$n⌝ where a ∈ Atom$n. This is not inhabited because every term y = a in Atom$n 
must mention the token "a" = a  (otherwise we could permute ("a","b") and get y = "b" and hence "b"="a").
Since ⌜a#a:Atom$n⌝ is not a type unless ⌜a ∈ Atom$n⌝, if we have ⌜a#a:Atom$n⌝ as a hypothesis in a sequent
then a ∈ Atom$n, then since a#a:Atom$n is not inhabited, the sequent is trivially true.
We thus have the "absurdity rule"" freeFromAtomAbsurdity .

Another base case is that if ⌜atom-free{$n:n}(T; x)⌝ then ⌜Ax ∈ a#x:T⌝. This is because atom-free{$n:n}(T; x)
 is, by definition,
∀a,b:Atom$n.  (swap-atoms{$n:n}(a; b; x) = x)
, so we may choose b to be "fresh" w.r.t. x (i.e. an atom not occuring in x)
and take y = swap-atoms{$n:n}(a; b; x) = x, then whatever token "a" the atom a evaluates to, will not occur in 
swap-atoms{$n:n}(a; b; x).
So, we have the first triviality rule: freeFromAtomTriviality .

The last base case is when x is an atom the is not equal to a. freeFromAtomBase .

Finally, if ⌜a#x:A⌝ and ⌜a#f:u:A ⟶ B[u]⌝ then 
then for some token "a", "a" = a in Aton{n}, and there are x' = x in A and
f' = f in u:A ⟶ B[u] such that "a" does not occur in f' or x'.
Then (f' x') = (f x) in B[x], and "a" does not occur in f' x'. Therefore, ⌜a#f x:B[x]⌝.
So we have shown that the application rule freeFromAtomApplication is true.

Note that the contrapositive of the application rule in the form
⌜(¬a#f x:B[x]) ⇒ ((¬a#f:u:A ⟶ B[u]) ∨ (¬a#x:A))⌝ will not be constructively true.
We define ⌜inheres{n:n}(T; x; a)⌝ to be the negation, ⌜¬a#x:A⌝, and we read it as "a is inherent in x:T".
It says that it is not possible to find a representative of x in T which avoids "a", i.e. that
every member of the equivalence class of x in T must mention the atom a.
Now, if f x must mention a, there can't be representatives f' and x' of f and x which don't mention a,
so at least one of f or x has no such representative. But since the number of possible representatives is
infinite, we can't in general decide which of them has this property.
So we don't have ⌜inheres{n:n}(B[x]; f x; a) ⇒ (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝ in general. 

We tried to define inherence as ⌜inheres{$n:n}(T; x; a) ==  ∃g:T ⟶ 𝔹. (↑matters{$n:n}(a; g; x))⌝ where 
⌜matters{$n:n}(a; g; x)⌝ (read as "matters"(a,g,x))
was a boolean (provided ⌜atom-free{n:n}(Type; T)⌝) defined by (nu b. ⌜¬bg x =b g swap-atoms{n:n}(a; b; x)⌝).
Here, nu b. X[b] means choose a fresh atom b not occring in X and evaluate X[b] to normal form (a boolean in our case)
and evalute to that normal form if it does not mention the fresh b and diverge otherwise.

From this definition we could prove (for types that were atom-free) the strong application inherence property
⌜inheres{n:n}(B[x]; f x; a) ⇒ (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝
 from a purported property of "matters" called
"conservation of matters". Unfortunately, the "conservation of matters" property is not true, as shown by the following
counter-example.
Let g <x,y> = ⌜¬b(x =a y ∧b (¬bx =a "a"))⌝,
let f = ⌜λx.<"a", x>⌝,
let x = "a".
Then g (f x) = g <"a","a"> = ⌜tt⌝.
Any tokens "b", "c" different from "a" do not occur in "a",g,f, or x, and
g (f swap-atoms{$n:n}(a; b; x)) = g <"a","b"> = ⌜tt⌝
g (swap-atoms{$n:n}(a; b; f) x) = g <"b","a"> = ⌜tt⌝
g (swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; c; x)) = g <"b","c"> = ⌜tt⌝, but
g (swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; b; x) ) = g <"b","b"> = ⌜ff⌝.
This example show that it is possible that 
⌜(↑matters{$n:n}(a; g; f x))
 ∧ (¬↑matters{$n:n}(a; λX.(g (f X)); x))
 ∧ (¬↑matters{$n:n}(a; λF.(g (F x)); f))
 ∧ (¬↑matters{$n:n}(a; λF.matters{$n:n}(a; λX.(g (F X)); x); f))⌝
whereas "conservation of matters" purported to show that
⌜(↑matters{$n:n}(a; g; f x)) ⇒ (((↑matters{$n:n}(a; λX.(g (f X)); ...)) ∨ ...) ∨ ...)⌝...

Lemma: free-from-atom_wf_general
∀[T:Type]. ∀[x:T]. ∀[a:Atom$m].  (a#x:T ∈ ℙ)

Lemma: free-from-atom_wf
∀[T:Type]. ∀[x:T]. ∀[a:Atom1].  (a#x:T ∈ ℙ)

Lemma: sq_stable__free-from-atom
∀[T:Type]. ∀[x:T]. ∀[a:Atom1].  SqStable(a#x:T)

Lemma: free-from-atom_wf2
∀[T:Type]. ∀[x:T]. ∀[a:Atom2].  (a#x:T ∈ ℙ)

Lemma: sq_stable__free-from-atom2
∀[T:Type]. ∀[x:T]. ∀[a:Atom2].  SqStable(a#x:T)

Lemma: free-from-atom-atom
∀[a,b:Atom1].  uiff(b#a:Atom1;¬(a = b ∈ Atom1))

Lemma: free-from-atom-outl
∀[A:Type]. ∀[x:A + Top]. ∀[a:Atom1].  (a#outl(x):A) supposing ((↑isl(x)) and a#x:A + Top)

Lemma: free-from-atom-outl2
∀[B,A:Type]. ∀[x:A + B]. ∀[a:Atom1].  (a#outl(x):A) supposing ((↑isl(x)) and a#x:A + B)

Lemma: free-from-atom-outr
∀[A:Type]. ∀[x:Top + A]. ∀[a:Atom1].  (a#outr(x):A) supposing ((¬↑isl(x)) and a#x:Top + A)

Lemma: free-from-atom-outr2
∀[B,A:Type]. ∀[x:B + A]. ∀[a:Atom1].  (a#outr(x):A) supposing ((¬↑isl(x)) and a#x:B + A)

Lemma: free-from-atom-subtype
∀[A,B:Type].  ∀[x:A]. ∀[a:Atom1].  a#x:B supposing a#x:A supposing A ⊆r B

Lemma: free-from-atom2-subtype
∀[A,B:Type].  ∀[x:A]. ∀[a:Atom2].  a#x:B supposing a#x:A supposing A ⊆r B

Lemma: free-from-atom-pair
∀[a:Atom1]. ∀[X,Y:Type]. ∀[x:X]. ∀[y:Y].  (a#<x, y>:X × Y) supposing (a#y:Y and a#x:X)

Lemma: free-from-atom-pair-components
∀[a:Atom1]. ∀[X:Type]. ∀[Y:X ⟶ 𝕌']. ∀[x:X]. ∀[y:Y[x]].  {a#x:X ∧ a#y:Y[x]} supposing a#<x, y>:x:X × Y[x]

Lemma: free-from-atom-pair-iff
∀[a:Atom1]. ∀[X:Type]. ∀[Y:𝕌']. ∀[x:X]. ∀[y:Y].  uiff(a#<x, y>:x:X × Y;a#x:X ∧ a#y:Y)

Lemma: assert_of_eq_atom
∀[x,y:Atom].  uiff(↑x =a y;x = y ∈ Atom)



Home Index