
Inductive val : Set :=
	v1 : val | v2 : val | v3 : val.

Definition auto_agent (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v2 => True
  | _ => False
  end.

Definition alice : val := v1.

Definition bob : val := v1.

Definition cons (x1 x2 : val) : val :=
  match x1,x2 with
cons(!1,!1) = !2
cons(!1,!2) = !1
cons(!1,!3) = !3
cons(!2,!1) = !2
cons(!2,!2) = !2
cons(!2,!3) = !3
cons(!3,!1) = !3
cons(!3,!2) = !3
cons(!3,!3) = !3
  end.

Definition crypt (x1 x2 : val) : val :=
  match x1,x2 with
crypt(!1,!1) = !1
crypt(!1,!2) = !1
crypt(!1,!3) = !2
crypt(!2,!1) = !1
crypt(!2,!2) = !1
crypt(!2,!3) = !3
crypt(!3,!1) = !2
crypt(!3,!2) = !3
crypt(!3,!3) = !3
  end.

Definition has_pub_key (x1 x2 : val) : val :=
  match x1,x2 with
has_pub_key(!1,!1) <=> $true
has_pub_key(!1,!2) <=> $false
has_pub_key(!1,!3) <=> $false
has_pub_key(!2,!1) <=> $false
has_pub_key(!2,!2) <=> $false
has_pub_key(!2,!3) <=> $false
has_pub_key(!3,!1) <=> $false
has_pub_key(!3,!2) <=> $false
has_pub_key(!3,!3) <=> $false
  end.

Definition i : val := v2.

%!!! unfinished

Definition key (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v1
  | v1,v2 => v2
  | v1,v3 => v2
  | v1,v4 => v2
  | v2,v1 => v4
  | v2,v2 => v2
  | v2,v3 => v2
  | v2,v4 => v2
  | v3,v1 => v2
  | v3,v2 => v2
  | v3,v3 => v4
  | v3,v4 => v1
  | v4,v1 => v2
  | v4,v2 => v2
  | v4,v3 => v4
  | v4,v4 => v1
  end.

Definition auto_knows_current (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v2 => True
  | _ => False
  end.

Definition auto_knows_old (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v2 => True
  | _ => False
  end.

Definition nil : val := v1.

Definition noncea_current (x1 x2 x3 : val) : val :=
  match x1,x2,x3 with
    v1,v1,v1 => v4
  | v1,v1,v2 => v4
  | v1,v1,v3 => v4
  | v1,v1,v4 => v4
  | v1,v2,v1 => v2
  | v1,v2,v2 => v2
  | v1,v2,v3 => v4
  | v1,v2,v4 => v1
  | v1,v3,v1 => v1
  | v1,v3,v2 => v2
  | v1,v3,v3 => v2
  | v1,v3,v4 => v1
  | v1,v4,v1 => v2
  | v1,v4,v2 => v1
  | v1,v4,v3 => v2
  | v1,v4,v4 => v1
  | v2,v1,v1 => v2
  | v2,v1,v2 => v3
  | v2,v1,v3 => v4
  | v2,v1,v4 => v3
  | v2,v2,v1 => v4
  | v2,v2,v2 => v2
  | v2,v2,v3 => v4
  | v2,v2,v4 => v2
  | v2,v3,v1 => v2
  | v2,v3,v2 => v2
  | v2,v3,v3 => v3
  | v2,v3,v4 => v2
  | v2,v4,v1 => v2
  | v2,v4,v2 => v2
  | v2,v4,v3 => v3
  | v2,v4,v4 => v2
  | v3,v1,v1 => v1
  | v3,v1,v2 => v2
  | v3,v1,v3 => v1
  | v3,v1,v4 => v3
  | v3,v2,v1 => v1
  | v3,v2,v2 => v3
  | v3,v2,v3 => v1
  | v3,v2,v4 => v3
  | v3,v3,v1 => v2
  | v3,v3,v2 => v2
  | v3,v3,v3 => v1
  | v3,v3,v4 => v3
  | v3,v4,v1 => v1
  | v3,v4,v2 => v1
  | v3,v4,v3 => v2
  | v3,v4,v4 => v1
  | v4,v1,v1 => v4
  | v4,v1,v2 => v1
  | v4,v1,v3 => v1
  | v4,v1,v4 => v4
  | v4,v2,v1 => v2
  | v4,v2,v2 => v1
  | v4,v2,v3 => v1
  | v4,v2,v4 => v1
  | v4,v3,v1 => v2
  | v4,v3,v2 => v2
  | v4,v3,v3 => v4
  | v4,v3,v4 => v1
  | v4,v4,v1 => v1
  | v4,v4,v2 => v4
  | v4,v4,v3 => v1
  | v4,v4,v4 => v4
  end.

Definition noncea_old (x1 x2 x3 : val) : val :=
  match x1,x2,x3 with
    v1,v1,v1 => v2
  | v1,v1,v2 => v2
  | v1,v1,v3 => v1
  | v1,v1,v4 => v1
  | v1,v2,v1 => v2
  | v1,v2,v2 => v2
  | v1,v2,v3 => v2
  | v1,v2,v4 => v1
  | v1,v3,v1 => v1
  | v1,v3,v2 => v1
  | v1,v3,v3 => v1
  | v1,v3,v4 => v1
  | v1,v4,v1 => v1
  | v1,v4,v2 => v1
  | v1,v4,v3 => v1
  | v1,v4,v4 => v1
  | v2,v1,v1 => v2
  | v2,v1,v2 => v2
  | v2,v1,v3 => v2
  | v2,v1,v4 => v2
  | v2,v2,v1 => v2
  | v2,v2,v2 => v2
  | v2,v2,v3 => v2
  | v2,v2,v4 => v2
  | v2,v3,v1 => v2
  | v2,v3,v2 => v2
  | v2,v3,v3 => v2
  | v2,v3,v4 => v2
  | v2,v4,v1 => v2
  | v2,v4,v2 => v2
  | v2,v4,v3 => v2
  | v2,v4,v4 => v2
  | v3,v1,v1 => v2
  | v3,v1,v2 => v2
  | v3,v1,v3 => v2
  | v3,v1,v4 => v2
  | v3,v2,v1 => v2
  | v3,v2,v2 => v2
  | v3,v2,v3 => v2
  | v3,v2,v4 => v2
  | v3,v3,v1 => v2
  | v3,v3,v2 => v2
  | v3,v3,v3 => v2
  | v3,v3,v4 => v2
  | v3,v4,v1 => v2
  | v3,v4,v2 => v2
  | v3,v4,v3 => v2
  | v3,v4,v4 => v2
  | v4,v1,v1 => v2
  | v4,v1,v2 => v2
  | v4,v1,v3 => v1
  | v4,v1,v4 => v1
  | v4,v2,v1 => v2
  | v4,v2,v2 => v2
  | v4,v2,v3 => v1
  | v4,v2,v4 => v2
  | v4,v3,v1 => v1
  | v4,v3,v2 => v1
  | v4,v3,v3 => v1
  | v4,v3,v4 => v1
  | v4,v4,v1 => v1
  | v4,v4,v2 => v1
  | v4,v4,v3 => v1
  | v4,v4,v4 => v1
  end.

Definition nonceb_current (x1 x2 x3 x4 : val) : val :=
  match x1,x2,x3,x4 with
    v1,v1,v1,v1 => v3
  | v1,v1,v1,v2 => v4
  | v1,v1,v1,v3 => v4
  | v1,v1,v1,v4 => v4
  | v1,v1,v2,v1 => v3
  | v1,v1,v2,v2 => v4
  | v1,v1,v2,v3 => v4
  | v1,v1,v2,v4 => v4
  | v1,v1,v3,v1 => v3
  | v1,v1,v3,v2 => v3
  | v1,v1,v3,v3 => v3
  | v1,v1,v3,v4 => v3
  | v1,v1,v4,v1 => v3
  | v1,v1,v4,v2 => v4
  | v1,v1,v4,v3 => v3
  | v1,v1,v4,v4 => v4
  | v1,v2,v1,v1 => v3
  | v1,v2,v1,v2 => v2
  | v1,v2,v1,v3 => v2
  | v1,v2,v1,v4 => v2
  | v1,v2,v2,v1 => v3
  | v1,v2,v2,v2 => v3
  | v1,v2,v2,v3 => v2
  | v1,v2,v2,v4 => v3
  | v1,v2,v3,v1 => v2
  | v1,v2,v3,v2 => v3
  | v1,v2,v3,v3 => v3
  | v1,v2,v3,v4 => v2
  | v1,v2,v4,v1 => v3
  | v1,v2,v4,v2 => v2
  | v1,v2,v4,v3 => v3
  | v1,v2,v4,v4 => v3
  | v1,v3,v1,v1 => v1
  | v1,v3,v1,v2 => v1
  | v1,v3,v1,v3 => v1
  | v1,v3,v1,v4 => v1
  | v1,v3,v2,v1 => v1
  | v1,v3,v2,v2 => v1
  | v1,v3,v2,v3 => v1
  | v1,v3,v2,v4 => v1
  | v1,v3,v3,v1 => v1
  | v1,v3,v3,v2 => v1
  | v1,v3,v3,v3 => v1
  | v1,v3,v3,v4 => v1
  | v1,v3,v4,v1 => v1
  | v1,v3,v4,v2 => v1
  | v1,v3,v4,v3 => v1
  | v1,v3,v4,v4 => v1
  | v1,v4,v1,v1 => v2
  | v1,v4,v1,v2 => v1
  | v1,v4,v1,v3 => v1
  | v1,v4,v1,v4 => v1
  | v1,v4,v2,v1 => v1
  | v1,v4,v2,v2 => v1
  | v1,v4,v2,v3 => v1
  | v1,v4,v2,v4 => v2
  | v1,v4,v3,v1 => v2
  | v1,v4,v3,v2 => v2
  | v1,v4,v3,v3 => v2
  | v1,v4,v3,v4 => v1
  | v1,v4,v4,v1 => v1
  | v1,v4,v4,v2 => v1
  | v1,v4,v4,v3 => v2
  | v1,v4,v4,v4 => v1
  | v2,v1,v1,v1 => v1
  | v2,v1,v1,v2 => v1
  | v2,v1,v1,v3 => v3
  | v2,v1,v1,v4 => v2
  | v2,v1,v2,v1 => v1
  | v2,v1,v2,v2 => v2
  | v2,v1,v2,v3 => v3
  | v2,v1,v2,v4 => v4
  | v2,v1,v3,v1 => v3
  | v2,v1,v3,v2 => v1
  | v2,v1,v3,v3 => v1
  | v2,v1,v3,v4 => v1
  | v2,v1,v4,v1 => v1
  | v2,v1,v4,v2 => v3
  | v2,v1,v4,v3 => v1
  | v2,v1,v4,v4 => v3
  | v2,v2,v1,v1 => v2
  | v2,v2,v1,v2 => v2
  | v2,v2,v1,v3 => v2
  | v2,v2,v1,v4 => v3
  | v2,v2,v2,v1 => v2
  | v2,v2,v2,v2 => v2
  | v2,v2,v2,v3 => v3
  | v2,v2,v2,v4 => v2
  | v2,v2,v3,v1 => v2
  | v2,v2,v3,v2 => v2
  | v2,v2,v3,v3 => v3
  | v2,v2,v3,v4 => v3
  | v2,v2,v4,v1 => v3
  | v2,v2,v4,v2 => v2
  | v2,v2,v4,v3 => v3
  | v2,v2,v4,v4 => v3
  | v2,v3,v1,v1 => v1
  | v2,v3,v1,v2 => v1
  | v2,v3,v1,v3 => v1
  | v2,v3,v1,v4 => v1
  | v2,v3,v2,v1 => v1
  | v2,v3,v2,v2 => v1
  | v2,v3,v2,v3 => v1
  | v2,v3,v2,v4 => v1
  | v2,v3,v3,v1 => v1
  | v2,v3,v3,v2 => v1
  | v2,v3,v3,v3 => v1
  | v2,v3,v3,v4 => v1
  | v2,v3,v4,v1 => v1
  | v2,v3,v4,v2 => v1
  | v2,v3,v4,v3 => v1
  | v2,v3,v4,v4 => v1
  | v2,v4,v1,v1 => v2
  | v2,v4,v1,v2 => v1
  | v2,v4,v1,v3 => v2
  | v2,v4,v1,v4 => v1
  | v2,v4,v2,v1 => v1
  | v2,v4,v2,v2 => v1
  | v2,v4,v2,v3 => v2
  | v2,v4,v2,v4 => v2
  | v2,v4,v3,v1 => v2
  | v2,v4,v3,v2 => v2
  | v2,v4,v3,v3 => v1
  | v2,v4,v3,v4 => v1
  | v2,v4,v4,v1 => v2
  | v2,v4,v4,v2 => v1
  | v2,v4,v4,v3 => v1
  | v2,v4,v4,v4 => v2
  | v3,v1,v1,v1 => v1
  | v3,v1,v1,v2 => v2
  | v3,v1,v1,v3 => v2
  | v3,v1,v1,v4 => v1
  | v3,v1,v2,v1 => v3
  | v3,v1,v2,v2 => v2
  | v3,v1,v2,v3 => v3
  | v3,v1,v2,v4 => v3
  | v3,v1,v3,v1 => v2
  | v3,v1,v3,v2 => v1
  | v3,v1,v3,v3 => v3
  | v3,v1,v3,v4 => v3
  | v3,v1,v4,v1 => v1
  | v3,v1,v4,v2 => v2
  | v3,v1,v4,v3 => v2
  | v3,v1,v4,v4 => v2
  | v3,v2,v1,v1 => v3
  | v3,v2,v1,v2 => v3
  | v3,v2,v1,v3 => v3
  | v3,v2,v1,v4 => v3
  | v3,v2,v2,v1 => v2
  | v3,v2,v2,v2 => v3
  | v3,v2,v2,v3 => v2
  | v3,v2,v2,v4 => v2
  | v3,v2,v3,v1 => v3
  | v3,v2,v3,v2 => v3
  | v3,v2,v3,v3 => v2
  | v3,v2,v3,v4 => v2
  | v3,v2,v4,v1 => v3
  | v3,v2,v4,v2 => v2
  | v3,v2,v4,v3 => v2
  | v3,v2,v4,v4 => v3
  | v3,v3,v1,v1 => v1
  | v3,v3,v1,v2 => v1
  | v3,v3,v1,v3 => v1
  | v3,v3,v1,v4 => v1
  | v3,v3,v2,v1 => v1
  | v3,v3,v2,v2 => v1
  | v3,v3,v2,v3 => v1
  | v3,v3,v2,v4 => v1
  | v3,v3,v3,v1 => v1
  | v3,v3,v3,v2 => v1
  | v3,v3,v3,v3 => v1
  | v3,v3,v3,v4 => v1
  | v3,v3,v4,v1 => v1
  | v3,v3,v4,v2 => v1
  | v3,v3,v4,v3 => v1
  | v3,v3,v4,v4 => v1
  | v3,v4,v1,v1 => v2
  | v3,v4,v1,v2 => v1
  | v3,v4,v1,v3 => v2
  | v3,v4,v1,v4 => v1
  | v3,v4,v2,v1 => v1
  | v3,v4,v2,v2 => v1
  | v3,v4,v2,v3 => v2
  | v3,v4,v2,v4 => v1
  | v3,v4,v3,v1 => v2
  | v3,v4,v3,v2 => v2
  | v3,v4,v3,v3 => v1
  | v3,v4,v3,v4 => v2
  | v3,v4,v4,v1 => v1
  | v3,v4,v4,v2 => v1
  | v3,v4,v4,v3 => v1
  | v3,v4,v4,v4 => v1
  | v4,v1,v1,v1 => v1
  | v4,v1,v1,v2 => v3
  | v4,v1,v1,v3 => v1
  | v4,v1,v1,v4 => v3
  | v4,v1,v2,v1 => v2
  | v4,v1,v2,v2 => v2
  | v4,v1,v2,v3 => v2
  | v4,v1,v2,v4 => v1
  | v4,v1,v3,v1 => v2
  | v4,v1,v3,v2 => v3
  | v4,v1,v3,v3 => v1
  | v4,v1,v3,v4 => v3
  | v4,v1,v4,v1 => v2
  | v4,v1,v4,v2 => v2
  | v4,v1,v4,v3 => v3
  | v4,v1,v4,v4 => v3
  | v4,v2,v1,v1 => v2
  | v4,v2,v1,v2 => v2
  | v4,v2,v1,v3 => v2
  | v4,v2,v1,v4 => v3
  | v4,v2,v2,v1 => v3
  | v4,v2,v2,v2 => v2
  | v4,v2,v2,v3 => v3
  | v4,v2,v2,v4 => v2
  | v4,v2,v3,v1 => v2
  | v4,v2,v3,v2 => v3
  | v4,v2,v3,v3 => v3
  | v4,v2,v3,v4 => v3
  | v4,v2,v4,v1 => v2
  | v4,v2,v4,v2 => v2
  | v4,v2,v4,v3 => v2
  | v4,v2,v4,v4 => v2
  | v4,v3,v1,v1 => v1
  | v4,v3,v1,v2 => v1
  | v4,v3,v1,v3 => v1
  | v4,v3,v1,v4 => v1
  | v4,v3,v2,v1 => v1
  | v4,v3,v2,v2 => v1
  | v4,v3,v2,v3 => v1
  | v4,v3,v2,v4 => v1
  | v4,v3,v3,v1 => v1
  | v4,v3,v3,v2 => v1
  | v4,v3,v3,v3 => v1
  | v4,v3,v3,v4 => v1
  | v4,v3,v4,v1 => v1
  | v4,v3,v4,v2 => v1
  | v4,v3,v4,v3 => v1
  | v4,v3,v4,v4 => v1
  | v4,v4,v1,v1 => v1
  | v4,v4,v1,v2 => v1
  | v4,v4,v1,v3 => v1
  | v4,v4,v1,v4 => v1
  | v4,v4,v2,v1 => v2
  | v4,v4,v2,v2 => v2
  | v4,v4,v2,v3 => v2
  | v4,v4,v2,v4 => v2
  | v4,v4,v3,v1 => v1
  | v4,v4,v3,v2 => v2
  | v4,v4,v3,v3 => v1
  | v4,v4,v3,v4 => v1
  | v4,v4,v4,v1 => v2
  | v4,v4,v4,v2 => v2
  | v4,v4,v4,v3 => v1
  | v4,v4,v4,v4 => v1
  end.

Definition nonceb_old (x1 x2 x3 x4 : val) : val :=
  match x1,x2,x3,x4 with
    v1,v1,v1,v1 => v1
  | v1,v1,v1,v2 => v1
  | v1,v1,v1,v3 => v1
  | v1,v1,v1,v4 => v1
  | v1,v1,v2,v1 => v2
  | v1,v1,v2,v2 => v1
  | v1,v1,v2,v3 => v2
  | v1,v1,v2,v4 => v1
  | v1,v1,v3,v1 => v1
  | v1,v1,v3,v2 => v2
  | v1,v1,v3,v3 => v2
  | v1,v1,v3,v4 => v1
  | v1,v1,v4,v1 => v1
  | v1,v1,v4,v2 => v1
  | v1,v1,v4,v3 => v1
  | v1,v1,v4,v4 => v1
  | v1,v2,v1,v1 => v2
  | v1,v2,v1,v2 => v2
  | v1,v2,v1,v3 => v2
  | v1,v2,v1,v4 => v2
  | v1,v2,v2,v1 => v2
  | v1,v2,v2,v2 => v2
  | v1,v2,v2,v3 => v2
  | v1,v2,v2,v4 => v2
  | v1,v2,v3,v1 => v2
  | v1,v2,v3,v2 => v2
  | v1,v2,v3,v3 => v2
  | v1,v2,v3,v4 => v2
  | v1,v2,v4,v1 => v2
  | v1,v2,v4,v2 => v2
  | v1,v2,v4,v3 => v2
  | v1,v2,v4,v4 => v2
  | v1,v3,v1,v1 => v2
  | v1,v3,v1,v2 => v1
  | v1,v3,v1,v3 => v2
  | v1,v3,v1,v4 => v1
  | v1,v3,v2,v1 => v1
  | v1,v3,v2,v2 => v1
  | v1,v3,v2,v3 => v1
  | v1,v3,v2,v4 => v1
  | v1,v3,v3,v1 => v2
  | v1,v3,v3,v2 => v1
  | v1,v3,v3,v3 => v1
  | v1,v3,v3,v4 => v1
  | v1,v3,v4,v1 => v1
  | v1,v3,v4,v2 => v1
  | v1,v3,v4,v3 => v1
  | v1,v3,v4,v4 => v2
  | v1,v4,v1,v1 => v2
  | v1,v4,v1,v2 => v2
  | v1,v4,v1,v3 => v2
  | v1,v4,v1,v4 => v2
  | v1,v4,v2,v1 => v1
  | v1,v4,v2,v2 => v1
  | v1,v4,v2,v3 => v2
  | v1,v4,v2,v4 => v2
  | v1,v4,v3,v1 => v2
  | v1,v4,v3,v2 => v1
  | v1,v4,v3,v3 => v1
  | v1,v4,v3,v4 => v1
  | v1,v4,v4,v1 => v1
  | v1,v4,v4,v2 => v1
  | v1,v4,v4,v3 => v1
  | v1,v4,v4,v4 => v1
  | v2,v1,v1,v1 => v2
  | v2,v1,v1,v2 => v1
  | v2,v1,v1,v3 => v2
  | v2,v1,v1,v4 => v1
  | v2,v1,v2,v1 => v2
  | v2,v1,v2,v2 => v1
  | v2,v1,v2,v3 => v2
  | v2,v1,v2,v4 => v2
  | v2,v1,v3,v1 => v1
  | v2,v1,v3,v2 => v1
  | v2,v1,v3,v3 => v1
  | v2,v1,v3,v4 => v2
  | v2,v1,v4,v1 => v1
  | v2,v1,v4,v2 => v1
  | v2,v1,v4,v3 => v2
  | v2,v1,v4,v4 => v2
  | v2,v2,v1,v1 => v2
  | v2,v2,v1,v2 => v2
  | v2,v2,v1,v3 => v2
  | v2,v2,v1,v4 => v2
  | v2,v2,v2,v1 => v2
  | v2,v2,v2,v2 => v2
  | v2,v2,v2,v3 => v2
  | v2,v2,v2,v4 => v2
  | v2,v2,v3,v1 => v2
  | v2,v2,v3,v2 => v2
  | v2,v2,v3,v3 => v2
  | v2,v2,v3,v4 => v2
  | v2,v2,v4,v1 => v2
  | v2,v2,v4,v2 => v2
  | v2,v2,v4,v3 => v2
  | v2,v2,v4,v4 => v2
  | v2,v3,v1,v1 => v1
  | v2,v3,v1,v2 => v1
  | v2,v3,v1,v3 => v1
  | v2,v3,v1,v4 => v1
  | v2,v3,v2,v1 => v2
  | v2,v3,v2,v2 => v1
  | v2,v3,v2,v3 => v1
  | v2,v3,v2,v4 => v2
  | v2,v3,v3,v1 => v1
  | v2,v3,v3,v2 => v1
  | v2,v3,v3,v3 => v2
  | v2,v3,v3,v4 => v2
  | v2,v3,v4,v1 => v1
  | v2,v3,v4,v2 => v2
  | v2,v3,v4,v3 => v1
  | v2,v3,v4,v4 => v2
  | v2,v4,v1,v1 => v1
  | v2,v4,v1,v2 => v1
  | v2,v4,v1,v3 => v2
  | v2,v4,v1,v4 => v1
  | v2,v4,v2,v1 => v2
  | v2,v4,v2,v2 => v1
  | v2,v4,v2,v3 => v1
  | v2,v4,v2,v4 => v1
  | v2,v4,v3,v1 => v2
  | v2,v4,v3,v2 => v2
  | v2,v4,v3,v3 => v2
  | v2,v4,v3,v4 => v2
  | v2,v4,v4,v1 => v1
  | v2,v4,v4,v2 => v1
  | v2,v4,v4,v3 => v2
  | v2,v4,v4,v4 => v1
  | v3,v1,v1,v1 => v1
  | v3,v1,v1,v2 => v2
  | v3,v1,v1,v3 => v1
  | v3,v1,v1,v4 => v2
  | v3,v1,v2,v1 => v2
  | v3,v1,v2,v2 => v2
  | v3,v1,v2,v3 => v2
  | v3,v1,v2,v4 => v1
  | v3,v1,v3,v1 => v2
  | v3,v1,v3,v2 => v2
  | v3,v1,v3,v3 => v2
  | v3,v1,v3,v4 => v1
  | v3,v1,v4,v1 => v2
  | v3,v1,v4,v2 => v2
  | v3,v1,v4,v3 => v1
  | v3,v1,v4,v4 => v1
  | v3,v2,v1,v1 => v2
  | v3,v2,v1,v2 => v2
  | v3,v2,v1,v3 => v2
  | v3,v2,v1,v4 => v2
  | v3,v2,v2,v1 => v2
  | v3,v2,v2,v2 => v2
  | v3,v2,v2,v3 => v2
  | v3,v2,v2,v4 => v2
  | v3,v2,v3,v1 => v2
  | v3,v2,v3,v2 => v2
  | v3,v2,v3,v3 => v2
  | v3,v2,v3,v4 => v2
  | v3,v2,v4,v1 => v2
  | v3,v2,v4,v2 => v2
  | v3,v2,v4,v3 => v2
  | v3,v2,v4,v4 => v2
  | v3,v3,v1,v1 => v1
  | v3,v3,v1,v2 => v1
  | v3,v3,v1,v3 => v2
  | v3,v3,v1,v4 => v2
  | v3,v3,v2,v1 => v1
  | v3,v3,v2,v2 => v2
  | v3,v3,v2,v3 => v1
  | v3,v3,v2,v4 => v1
  | v3,v3,v3,v1 => v1
  | v3,v3,v3,v2 => v1
  | v3,v3,v3,v3 => v2
  | v3,v3,v3,v4 => v2
  | v3,v3,v4,v1 => v2
  | v3,v3,v4,v2 => v2
  | v3,v3,v4,v3 => v1
  | v3,v3,v4,v4 => v1
  | v3,v4,v1,v1 => v1
  | v3,v4,v1,v2 => v2
  | v3,v4,v1,v3 => v2
  | v3,v4,v1,v4 => v2
  | v3,v4,v2,v1 => v1
  | v3,v4,v2,v2 => v2
  | v3,v4,v2,v3 => v1
  | v3,v4,v2,v4 => v2
  | v3,v4,v3,v1 => v1
  | v3,v4,v3,v2 => v1
  | v3,v4,v3,v3 => v1
  | v3,v4,v3,v4 => v1
  | v3,v4,v4,v1 => v2
  | v3,v4,v4,v2 => v1
  | v3,v4,v4,v3 => v2
  | v3,v4,v4,v4 => v2
  | v4,v1,v1,v1 => v2
  | v4,v1,v1,v2 => v1
  | v4,v1,v1,v3 => v1
  | v4,v1,v1,v4 => v1
  | v4,v1,v2,v1 => v2
  | v4,v1,v2,v2 => v2
  | v4,v1,v2,v3 => v1
  | v4,v1,v2,v4 => v1
  | v4,v1,v3,v1 => v1
  | v4,v1,v3,v2 => v1
  | v4,v1,v3,v3 => v1
  | v4,v1,v3,v4 => v2
  | v4,v1,v4,v1 => v1
  | v4,v1,v4,v2 => v1
  | v4,v1,v4,v3 => v2
  | v4,v1,v4,v4 => v2
  | v4,v2,v1,v1 => v2
  | v4,v2,v1,v2 => v2
  | v4,v2,v1,v3 => v2
  | v4,v2,v1,v4 => v2
  | v4,v2,v2,v1 => v2
  | v4,v2,v2,v2 => v2
  | v4,v2,v2,v3 => v2
  | v4,v2,v2,v4 => v2
  | v4,v2,v3,v1 => v2
  | v4,v2,v3,v2 => v2
  | v4,v2,v3,v3 => v2
  | v4,v2,v3,v4 => v2
  | v4,v2,v4,v1 => v2
  | v4,v2,v4,v2 => v2
  | v4,v2,v4,v3 => v2
  | v4,v2,v4,v4 => v2
  | v4,v3,v1,v1 => v1
  | v4,v3,v1,v2 => v2
  | v4,v3,v1,v3 => v1
  | v4,v3,v1,v4 => v1
  | v4,v3,v2,v1 => v1
  | v4,v3,v2,v2 => v2
  | v4,v3,v2,v3 => v2
  | v4,v3,v2,v4 => v2
  | v4,v3,v3,v1 => v2
  | v4,v3,v3,v2 => v2
  | v4,v3,v3,v3 => v2
  | v4,v3,v3,v4 => v1
  | v4,v3,v4,v1 => v2
  | v4,v3,v4,v2 => v2
  | v4,v3,v4,v3 => v2
  | v4,v3,v4,v4 => v2
  | v4,v4,v1,v1 => v1
  | v4,v4,v1,v2 => v1
  | v4,v4,v1,v3 => v2
  | v4,v4,v1,v4 => v2
  | v4,v4,v2,v1 => v1
  | v4,v4,v2,v2 => v1
  | v4,v4,v2,v3 => v1
  | v4,v4,v2,v4 => v1
  | v4,v4,v3,v1 => v2
  | v4,v4,v3,v2 => v2
  | v4,v4,v3,v3 => v1
  | v4,v4,v3,v4 => v1
  | v4,v4,v4,v1 => v1
  | v4,v4,v4,v2 => v1
  | v4,v4,v4,v3 => v2
  | v4,v4,v4,v4 => v2
  end.

Definition prv : val := v2.

Definition pub : val := v1.

Definition s (x1 : val) : val :=
  match x1 with
    v1 => v1
  | v2 => v2
  | v3 => v3
  | v4 => v3
  end.

Definition server : val := v1.

Definition session_old (x1 x2 x3 : val) : val := v2.

Definition sym : val := v2.



Lemma lem_alice_agent : auto_agent alice.
Proof.
  simpl; trivial.
Qed.

Lemma lem_alice_bob : auto_agent bob.
Proof.
  simpl; trivial.
Qed.

Lemma lem_alice_server : auto_agent server.
Proof.
  simpl; trivial.
Qed.

Lemma lem_alice_intruder : auto_agent i.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_nil_old : auto_knows_old nil.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_can_take_first_components_old :
  forall _big_m1 _big_m2:val,
    auto_knows_old (cons _big_m1 _big_m2) -> auto_knows_old _big_m1.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_take_second_components_old :
  forall _big_m1 _big_m2:val,
    auto_knows_old (cons _big_m1 _big_m2) -> auto_knows_old _big_m2.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_build_pairs_old :
  forall _big_m1 _big_m2:val,
    auto_knows_old _big_m1 -> auto_knows_old _big_m2 -> auto_knows_old (cons _big_m1 _big_m2).
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_encrypt_old :
  forall _big_k _big_m:val,
    auto_knows_old _big_m -> auto_knows_old _big_k -> auto_knows_old (crypt _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_private_key_old :
  forall _big_k _big_m:val,
    auto_knows_old (crypt _big_m (key pub _big_k))
     -> auto_knows_old (key prv _big_k)
     -> auto_knows_old _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_public_key_old :
  forall _big_k _big_m:val,
    auto_knows_old (crypt _big_m (key prv _big_k))
    -> auto_knows_old (key pub _big_k)
    -> auto_knows_old _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_symmetric_key_old : forall _big_m X:val, auto_knows_old (crypt _big_m (key sym X)) -> auto_knows_old (key sym X) -> auto_knows_old _big_m.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_successors_old : forall _big_m:val, auto_knows_old _big_m -> auto_knows_old (s _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_predecessors_old : forall _big_m:val, auto_knows_old (s _big_m) -> auto_knows_old _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_alice_asks_server_old : forall _big_a _big_b:val, auto_agent _big_b -> auto_agent _big_a -> auto_knows_old (cons _big_a (cons _big_b nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_server_gives_bobs_public_key_to_alice_old : forall _big_a _big_b:val, auto_knows_old (cons _big_a (cons _big_b nil)) -> auto_knows_old (crypt (cons (key pub _big_b) (cons _big_b nil)) (key prv server)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_alice_sends_msg_to_bob_old : forall _big_a _big_b _big_kPb:val, auto_agent _big_a -> auto_knows_old (crypt (cons _big_kPb (cons _big_b nil)) (key prv server)) -> auto_knows_old (crypt (cons (noncea_old _big_a _big_b _big_kPb) (cons _big_a nil)) _big_kPb).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPb; case _big_kPb; simpl; trivial.
Qed.

Lemma lem_bob_asks_server_old : forall _big_a _big_b:val, auto_agent _big_b -> auto_agent _big_a -> auto_knows_old (cons _big_b (cons _big_a nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_server_gives_alices_public_key_to_bob_old : forall _big_a _big_b:val, auto_knows_old (cons _big_b (cons _big_a nil)) -> auto_knows_old (crypt (cons (key pub _big_a) (cons _big_a nil)) (key prv server)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_bob_answers_alice_with_own_msg_old : forall _big_a _big_b _big_kPa _big_na:val, auto_knows_old (crypt (cons _big_na (cons _big_a nil)) (key pub _big_b)) -> auto_agent _big_b -> auto_knows_old (crypt (cons _big_kPa (cons _big_a nil)) (key prv server)) -> auto_knows_old (crypt (cons _big_na (cons (nonceb_old _big_a _big_b _big_kPa _big_na) (cons _big_b nil))) _big_kPa).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPa; case _big_kPa; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_alice_confirms_to_bob_old : forall _big_a _big_b _big_kPb _big_nb:val, auto_knows_old (crypt (cons (noncea_old _big_a _big_b _big_kPb) (cons _big_nb (cons _big_b nil))) (key pub _big_a)) -> auto_knows_old (crypt (cons _big_kPb (cons _big_b nil)) (key prv server)) -> auto_knows_old (crypt _big_nb _big_kPb).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPb; case _big_kPb; intro _big_nb; case _big_nb; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_agents_old : forall X:val, auto_agent X -> auto_knows_old X.
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_knows_every_public_key_old : forall X:val, auto_knows_old (key pub X).
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_knows_own_private_key_old : auto_knows_old (key prv i).
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_remembers : forall _big_m:val, auto_knows_old _big_m -> auto_knows_current _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_previous_session_keys : forall _big_a _big_b _big_na:val, auto_knows_current (key sym (session_old _big_a _big_b _big_na)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_previous_noncea : forall _big_a _big_b _big_kPb:val, auto_knows_current (noncea_old _big_a _big_b _big_kPb).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPb; case _big_kPb; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_previous_nonceb : forall _big_a _big_b _big_kPa _big_na:val, auto_knows_current (nonceb_old _big_a _big_b _big_kPa _big_na).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPa; case _big_kPa; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_intruder_knows_nil_current : auto_knows_current nil.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_can_take_first_components_current : forall _big_m1 _big_m2:val, auto_knows_current (cons _big_m1 _big_m2) -> auto_knows_current _big_m1.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_take_second_components_current : forall _big_m1 _big_m2:val, auto_knows_current (cons _big_m1 _big_m2) -> auto_knows_current _big_m2.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_build_pairs_current : forall _big_m1 _big_m2:val, auto_knows_current _big_m1 -> auto_knows_current _big_m2 -> auto_knows_current (cons _big_m1 _big_m2).
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_encrypt_current : forall _big_k _big_m:val, auto_knows_current _big_m -> auto_knows_current _big_k -> auto_knows_current (crypt _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_private_key_current : forall _big_k _big_m:val, auto_knows_current (crypt _big_m (key pub _big_k)) -> auto_knows_current (key prv _big_k) -> auto_knows_current _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_public_key_current : forall _big_k _big_m:val, auto_knows_current (crypt _big_m (key prv _big_k)) -> auto_knows_current (key pub _big_k) -> auto_knows_current _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_symmetric_key_current : forall _big_m X:val, auto_knows_current (crypt _big_m (key sym X)) -> auto_knows_current (key sym X) -> auto_knows_current _big_m.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_successors_current : forall _big_m:val, auto_knows_current _big_m -> auto_knows_current (s _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_predecessors_current : forall _big_m:val, auto_knows_current (s _big_m) -> auto_knows_current _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_alice_asks_server_current : forall _big_a _big_b:val, auto_agent _big_b -> auto_agent _big_a -> auto_knows_current (cons _big_a (cons _big_b nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_server_gives_bobs_public_key_to_alice_current : forall _big_a _big_b:val, auto_knows_current (cons _big_a (cons _big_b nil)) -> auto_knows_current (crypt (cons (key pub _big_b) (cons _big_b nil)) (key prv server)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_alice_sends_msg_to_bob_current : forall _big_a _big_b _big_kPb:val, auto_agent _big_a -> auto_knows_current (crypt (cons _big_kPb (cons _big_b nil)) (key prv server)) -> auto_knows_current (crypt (cons (noncea_current _big_a _big_b _big_kPb) (cons _big_a nil)) _big_kPb).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPb; case _big_kPb; simpl; trivial.
Qed.

Lemma lem_bob_asks_server_current : forall _big_a _big_b:val, auto_agent _big_b -> auto_agent _big_a -> auto_knows_current (cons _big_b (cons _big_a nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_server_gives_alices_public_key_to_bob_current : forall _big_a _big_b:val, auto_knows_current (cons _big_b (cons _big_a nil)) -> auto_knows_current (crypt (cons (key pub _big_a) (cons _big_a nil)) (key prv server)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_bob_answers_alice_with_own_msg_current : forall _big_a _big_b _big_kPa _big_na:val, auto_knows_current (crypt (cons _big_na (cons _big_a nil)) (key pub _big_b)) -> auto_agent _big_b -> auto_knows_current (crypt (cons _big_kPa (cons _big_a nil)) (key prv server)) -> auto_knows_current (crypt (cons _big_na (cons (nonceb_current _big_a _big_b _big_kPa _big_na) (cons _big_b nil))) _big_kPa).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPa; case _big_kPa; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_alice_confirms_to_bob_current : forall _big_a _big_b _big_kPb _big_nb:val, auto_knows_current (crypt (cons (noncea_current _big_a _big_b _big_kPb) (cons _big_nb (cons _big_b nil))) (key pub _big_a)) -> auto_knows_current (crypt (cons _big_kPb (cons _big_b nil)) (key prv server)) -> auto_knows_current (crypt _big_nb _big_kPb).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kPb; case _big_kPb; intro _big_nb; case _big_nb; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_agents_current : forall X:val, auto_agent X -> auto_knows_current X.
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_knows_every_public_key_current : forall X:val, auto_knows_current (key pub X).
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_knows_own_private_key_current : auto_knows_current (key prv i).
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_alice_msg : forall _big_kPb:val, auto_knows_current (noncea_current alice bob _big_kPb) -> False.
Proof.
  intro _big_kPb; case _big_kPb; simpl; trivial.
Qed.

Lemma lem_intruder_knows_bob_msg : forall _big_kPa _big_na:val, auto_knows_current (nonceb_current alice bob _big_kPa _big_na) -> False.
Proof.
  intro _big_kPa; case _big_kPa; intro _big_na; case _big_na; simpl; trivial.
Qed.
