%%%%%% Multisets of natural numbers
%%%%%% John Boyland
%%%%%% You may freely use, modify and distribute this file without restrictions.
%%%%% This file requires the "nat.elf" signature
%{%
This signature implements (finite) multisets of natural numbers.
They can be seen as maps from natural numbers o natural numbers
wherea only a finite subset of the domain maps to non-zero.
The representation is "adequate" in that every multiset
has a unique representation. In other words, equality of the terms
is the same as semantic equality.
%}%
%{%
This signature was created using "map" and is not "optimally" concise.
The proofs of the theorems are more general than necessary and
use many trivial lemmas.
%}%
%{%
This file follows the same theorem naming convention as nat.elf (q.v.)
%}%
%%%%% multiset-help.elf
%%%%% Theorems needed to help 'multiset' use 'map.'
%%%%% This file is part of the multiset.elf signature
%%%% Renamings
%{%
What follows is a series of renamings, to get
the existing nat min/max theorems named in the way
the map functor requires.
%}%
%abbrev nat`leq = nat`le.
%abbrev nat`false-implies-leq = nat`false-implies-le.
%abbrev nat`leq-reflexive = nat`le-reflexive.
%abbrev nat`leq-transitive = nat`le-transitive.
%abbrev nat`leq-anti-symmetric = nat`le-anti-symmetric.
%abbrev nat`union = nat`max.
%abbrev nat`false-implies-union = nat`false-implies-max.
%abbrev nat`union-deterministic = nat`max-deterministic.
%abbrev nat`union-total* = nat`max-total*.
%abbrev nat`union-commutative = nat`max-commutative.
%abbrev nat`union-associative = nat`max-associative.
%abbrev nat`union-associative* = nat`max-associative*.
%abbrev nat`union-left-preserves-leq* = nat`max-left-preserves-le*.
%abbrev nat`union-preserves-leq = nat`max-preserves-le.
%abbrev nat`union-implies-leq* = [G] [L] nat`max-implies-ge G L IG.
%abbrev nat`union-implies-leq = nat`max-implies-ge.
%abbrev nat`union-is-lub = nat`max-is-lub.
%abbrev nat`intersection = nat`min.
%abbrev nat`false-implies-intersection = nat`false-implies-min.
%abbrev nat`intersection-deterministic = nat`min-deterministic.
%abbrev nat`intersection-total* = nat`min-total*.
%abbrev nat`intersection-commutative = nat`min-commutative.
%abbrev nat`intersection-associative = nat`min-associative.
%abbrev nat`intersection-associative* = nat`min-associative*.
%abbrev nat`intersection-implies-leq* = [M] [L] nat`min-implies-ge M L IG.
%abbrev nat`intersection-left-preserves-leq* = nat`min-left-preserves-le*.
%abbrev nat`intersection-is-glb = nat`min-is-glb.
%abbrev nat`intersection-right-distributes-over-union =
nat`min-right-distributes-over-max.
%abbrev nat`union-right-distributes-over-intersection =
nat`max-right-distributes-over-min.
%%%% Functor Use
%%%% Definitions of Maps
map : type.
map/0 : map.
map/+ : nat -> nat -> map -> map.
%%%% Relations on maps
eq : map -> map -> type.
eq/ : eq M M.
ne : map -> map -> type.
ne/L : ne map/0 (map/+ _ _ _).
ne/R : ne (map/+ _ _ _) map/0.
ne/N : nat`ne N1 N2 -> ne (map/+ N1 _ _) (map/+ N2 _ _).
ne/D : nat`ne D1 D2 -> ne (map/+ _ D1 _) (map/+ _ D2 _).
ne/+ : ne M1 M2 -> ne (map/+ _ _ M1) (map/+ _ _ M2).
eq? : map -> map -> bool -> type.
eq?/yes : eq? X X true.
eq?/no : eq? X Y false
<- ne X Y.
lookup : map -> nat -> nat -> type.
lookup/= : lookup (map/+ N1 D _) N2 D
<- nat`eq N1 N2.
lookup/> : lookup (map/+ N1 _ F) N2 D
<- plus (s N0) N1 N2
<- lookup F N0 D.
not-member : map -> nat -> type.
not-member/0 : not-member map/0 M.
not-member/< : not-member (map/+ N _ F) M
<- gt N M.
not-member/> : not-member (map/+ N _ F) M
<- plus (s M1) N M
<- not-member F M1.
member? : map -> nat -> bool -> type.
member?/in : member? M N true
<- lookup M N _.
member?/out : member? M N false
<- not-member M N.
disjoint : map -> map -> type.
disjoint/L : disjoint map/0 M.
disjoint/R : disjoint M map/0.
disjoint/< : disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`plus (s N0) N1 N2
<- disjoint M1 (map/+ N0 D2 M2).
disjoint/> : disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`plus (s N3) N2 N1
<- disjoint (map/+ N3 D1 M1) M2.
disjoint? : map -> map -> bool -> type.
disjoint?/yes : disjoint M1 M2 -> disjoint? M1 M2 true.
disjoint?/no :
lookup M1 N D1 ->
lookup M2 N D2 ->
disjoint? M1 M2 false.
size : map -> nat -> type.
size/0 : size map/0 z.
size/+ : size (map/+ _ _ M) (s N)
<- size M N.
%% useful for proving termination on map operations:
bound : map -> nat -> type.
bound/0 : bound map/0 z.
bound/+ : bound (map/+ N1 D M) N3
<- bound M N2
<- plus (s N1) N2 N3.
shift : nat -> map -> map -> type.
shift/0 : shift _ map/0 map/0.
shift/+ : shift N1 (map/+ N2 D M) (map/+ N3 D M)
<- plus (s N1) N2 N3.
update : map -> nat -> nat -> map -> type.
update/0 : update map/0 N D (map/+ N D map/0).
update/= : update (map/+ N1 _ F) N2 D (map/+ N2 D F)
<- nat`eq N1 N2.
update/< : update (map/+ N1 D1 F) N2 D2 (map/+ N2 D2 (map/+ N3 D1 F))
<- plus (s N3) N2 N1.
update/> : update (map/+ N1 D1 F1) N2 D2 (map/+ N1 D1 F2)
<- plus (s N0) N1 N2
<- update F1 N0 D2 F2.
%%%% Theorems
%%% Theorems about eq
%theorem meta-eq :
forall {M} {N} {E:eq M N}
true.
- : meta-eq M M eq/.
%worlds () (meta-eq _ _ _).
%total {} (meta-eq _ _ _).
%reduces M = N (meta-eq M N _).
%theorem false-implies-eq :
forall* {M} {M'} forall {F:void} exists {E:eq M M'} true.
%worlds () (false-implies-eq _ %{=>}% M=M').
%total {} (false-implies-eq _ _).
%theorem eq-reflexive : forall {M} exists {E:eq M M} true.
- : eq-reflexive _ eq/.
%worlds () (eq-reflexive M %{=>}% M=M).
%total {} (eq-reflexive _ _).
%theorem eq-symmetric :
forall* {M} {M'}
forall {E1:eq M M'}
exists {E2:eq M' M}
true.
- : eq-symmetric eq/ eq/.
%worlds () (eq-symmetric M=M' %{=>}% M'=M).
%total {} (eq-symmetric _ _).
%theorem eq-transitive:
forall* {M1} {M2} {M3}
forall {E12:eq M1 M2} {E23:eq M2 M3}
exists {E13:eq M1 M3}
true.
- : eq-transitive eq/ eq/ eq/.
%worlds () (eq-transitive M1=M2 M2=M3 %{=>}% M1=M3).
%total {} (eq-transitive _ _ _).
%theorem map/+-preserves-eq :
forall* {N} {NP} {D} {DP} {F} {FP}
forall {EN:nat`eq N NP} {ED:nat`eq D DP} {EF:eq F FP}
exists {E:eq (map/+ N D F) (map/+ NP DP FP)}
true.
- : map/+-preserves-eq nat`eq/ nat`eq/ eq/ eq/.
%worlds () (map/+-preserves-eq N=N' D=D' F=F' %{=>}% NDF=N'D'F').
%total {} (map/+-preserves-eq _ _ _ _).
%theorem map/+-preserves-eq-converse :
forall* {N} {NP} {D} {DP} {F} {FP}
forall {E:eq (map/+ N D F) (map/+ NP DP FP)}
exists {EN:nat`eq N NP} {ED:nat`eq D DP} {EF:eq F FP}
true.
- : map/+-preserves-eq-converse eq/ nat`eq/ nat`eq/ eq/.
%worlds () (map/+-preserves-eq-converse _ _ _ _).
%total {} (map/+-preserves-eq-converse _ _ _ _).
%theorem eq-no-occur :
forall* {M} {N} {D}
forall {E:eq M (map/+ N D M)}
exists {F:void}
true.
%worlds () (eq-no-occur _ _).
%total {} (eq-no-occur _ _).
%theorem eq-contradiction :
forall* {N} {D} {M}
forall {E:eq map/0 (map/+ N D M)}
exists {F:void}
true.
%worlds () (eq-contradiction _ _).
%total {} (eq-contradiction _ _).
%%% Theorems about ne
%theorem false-implies-ne :
forall* {M1} {M2}
forall {F:void}
exists {N:ne M1 M2}
true.
%worlds () (false-implies-ne _ _).
%total { } (false-implies-ne _ _).
%theorem ne-respects-eq :
forall* {M11} {M12} {M21} {M22}
forall {N1:ne M11 M12} {E1:eq M11 M21} {E2:eq M12 M22}
exists {N2:ne M21 M22}
true.
- : ne-respects-eq N eq/ eq/ N.
%worlds () (ne-respects-eq _ _ _ _).
%total { } (ne-respects-eq _ _ _ _).
%theorem ne-anti-reflexive :
forall* {M}
forall {N:ne M M}
exists {F:void}
true.
- : ne-anti-reflexive (ne/N N) F
<- nat`ne-anti-reflexive N F.
- : ne-anti-reflexive (ne/D N) F
<- nat`ne-anti-reflexive N F.
- : ne-anti-reflexive (ne/+ N) F
<- ne-anti-reflexive N F.
%worlds () (ne-anti-reflexive _ _).
%total (N) (ne-anti-reflexive N _).
%theorem ne-symmetric :
forall* {M1} {M2}
forall {N1:ne M1 M2}
exists {N2:ne M2 M1}
true.
- : ne-symmetric ne/L ne/R.
- : ne-symmetric ne/R ne/L.
- : ne-symmetric (ne/N N1) (ne/N N2)
<- nat`ne-symmetric N1 N2.
- : ne-symmetric (ne/D N1) (ne/D N2)
<- nat`ne-symmetric N1 N2.
- : ne-symmetric (ne/+ N1) (ne/+ N2)
<- ne-symmetric N1 N2.
%worlds () (ne-symmetric _ _).
%total (N) (ne-symmetric N _).
%theorem eq-ne-implies-false :
forall* {X} {Y}
forall {D1:eq X Y} {D2:ne X Y}
exists {F:void}
true.
- : eq-ne-implies-false eq/ X<>X F
<- ne-anti-reflexive X<>X F.
%worlds () (eq-ne-implies-false _ _ _).
%total { } (eq-ne-implies-false _ _ _).
%theorem eq?-total* :
forall {M} {N}
exists {B} {T:eq? M N B}
true.
%abbrev eq?-total = eq?-total* _ _ _.
%theorem eq?-total/+ :
forall* {N1} {D1} {N2} {D2} {M2} {EN} {ED} {EM}
forall {M1}
{EN?:nat`eq? N1 N2 EN}
{ED?:nat`eq? D1 D2 ED}
{EM?:eq? M1 M2 EM}
exists {B}
{E?:eq? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
- : eq?-total eq?/yes.
- : eq?-total (eq?/no ne/L).
- : eq?-total (eq?/no ne/R).
- : eq?-total E?
<- nat`eq?-total EN?
<- nat`eq?-total ED?
<- eq?-total EM?
<- eq?-total/+ _ EN? ED? EM? _ E?.
- : eq?-total/+ _ (nat`eq?/yes) (nat`eq?/yes) (eq?/yes) _ eq?/yes.
- : eq?-total/+ _ (nat`eq?/no N) _ _ _ (eq?/no (ne/N N)).
- : eq?-total/+ _ _ (nat`eq?/no N) _ _ (eq?/no (ne/D N)).
- : eq?-total/+ _ _ _ (eq?/no N) _ (eq?/no (ne/+ N)).
%worlds () (eq?-total* _ _ _ _) (eq?-total/+ _ _ _ _ _ _).
%total (M W) (eq?-total* M _ _ _) (eq?-total/+ W _ _ _ _ _).
%%% Theorems about lookup
%theorem false-implies-lookup :
forall* {M} {N} {D}
forall {F:void}
exists {L:lookup M N D}
true.
%worlds () (false-implies-lookup _ %{=>}% F^N=D).
%total {} (false-implies-lookup _ _).
%theorem lookup-respects-eq :
forall* {M} {N} {D} {MP} {NP} {DP}
forall {L:lookup M N D} {EM:eq M MP} {EN:nat`eq N NP} {ED:nat`eq D DP}
exists {LP:lookup MP NP DP}
true.
- : lookup-respects-eq L eq/ nat`eq/ nat`eq/ L.
%worlds () (lookup-respects-eq M^N=D M=M' N=N' D=D' %{=>}% M'^N'=D').
%total {} (lookup-respects-eq _ _ _ _ _).
%theorem lookup-deterministic :
forall* {M} {N} {D} {MP} {NP} {DP}
forall {L:lookup M N D} {LP:lookup MP NP DP}
{EM:eq M MP} {EN:nat`eq N NP}
exists {ED:nat`eq D DP}
true.
- : lookup-deterministic (lookup/= nat`eq/) (lookup/= nat`eq/) eq/ nat`eq/ nat`eq/.
- : lookup-deterministic (lookup/> F^N0=D N0+1+N1=N2)
(lookup/> F^N0'=D' N0'+1+N1=N2) eq/ nat`eq/ D=D'
<- plus-right-cancels N0+1+N1=N2 N0'+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0'
<- lookup-deterministic F^N0=D F^N0'=D' eq/ N0=N0' D=D'.
%% contradiction cases
- : lookup-deterministic (lookup/= nat`eq/) (lookup/> _ N0+1+N=N)
eq/ nat`eq/ D=D'
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N FALSE
<- nat`false-implies-eq FALSE D=D'.
- : lookup-deterministic (lookup/> _ N0+1+N=N) (lookup/= nat`eq/)
eq/ nat`eq/ D=D'
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N FALSE
<- nat`false-implies-eq FALSE D=D'.
%worlds () (lookup-deterministic M^N=D M'^N'=D' M=M' N=N' %{=>}% D=D').
%total (L) (lookup-deterministic L _ _ _ _).
%% lookup is NOT total
%theorem lookup-contradiction :
forall* {N} {D}
forall {L:lookup map/0 N D}
exists {F:void}
true.
%worlds () (lookup-contradiction _ _).
%total { } (lookup-contradiction _ _).
%theorem lookup-one-choice :
forall* {N1} {D1} {N2} {D2}
forall {L:lookup (map/+ N1 D1 map/0) N2 D2}
exists {NE:nat`eq N1 N2} {DE:nat`eq D1 D2}
true.
- : lookup-one-choice (lookup/= nat`eq/) nat`eq/ nat`eq/.
%worlds () (lookup-one-choice _ _ _).
%total { } (lookup-one-choice _ _ _).
%theorem lookup-ne-implies-ne :
forall* {M1} {N1} {D1} {M2} {N2} {D2}
forall {L1:lookup M1 N1 D1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
{ND:nat`ne D1 D2}
exists {NM:ne M1 M2}
true.
%theorem lookup-ne-implies-ne/L :
forall* {M1} {N1} {D1} {M2} {N2} {D2} {B}
forall {L1:lookup M1 N1 D1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
{ND:nat`ne D1 D2}
{EM?:eq? M1 M2 B}
exists {NM:ne M1 M2}
true.
- : lookup-ne-implies-ne L1 L2 EN ND NM
<- eq?-total EM?
<- lookup-ne-implies-ne/L L1 L2 EN ND EM? NM.
- : lookup-ne-implies-ne/L L1 L2 _ _ (eq?/no NM) NM.
- : lookup-ne-implies-ne/L L1 L2 nat`eq/ D1<>D2 eq?/yes NM
<- lookup-deterministic L1 L2 eq/ nat`eq/ D1=D2
<- nat`eq-ne-implies-false D1=D2 D1<>D2 F
<- false-implies-ne F NM.
%worlds () (lookup-ne-implies-ne/L _ _ _ _ _ _).
%total { } (lookup-ne-implies-ne/L _ _ _ _ _ _).
%worlds () (lookup-ne-implies-ne _ _ _ _ _).
%total { } (lookup-ne-implies-ne _ _ _ _ _).
%%% Theorems about not-member
%theorem false-implies-not-member :
forall* {M} {N} forall {F:void} exists {D:not-member M N} true.
%worlds () (false-implies-not-member _ %{=>}% N-not-in-member-M).
%total {} (false-implies-not-member _ _).
%theorem not-member-respects-eq :
forall* {M} {N} {MP} {NP}
forall {D:not-member M N} {EM:eq M MP} {EN:nat`eq N NP}
exists {DP:not-member MP NP}
true.
- : not-member-respects-eq D eq/ nat`eq/ D.
%worlds () (not-member-respects-eq _ _ _ _).
%total {} (not-member-respects-eq _ _ _ _).
%% not-member is NOT deterministic
%theorem not-member-total* :
forall {M}
exists {N} {F:not-member M N}
true.
- : not-member-total* map/0 z not-member/0.
- : not-member-total* (map/+ N1 _ M) N3 (not-member/> F N+1+N1=N3)
<- not-member-total* M N F
<- plus-total* (s N) N1 N3 N+1+N1=N3.
%worlds () (not-member-total* M %{=>}% N N-not-in-member-of-M).
%total (M) (not-member-total* M _ _).
%abbrev not-member-total = not-member-total* _ _.
%theorem not-member-lookup-not-equal :
forall* {M} {N1} {N2} {D2}
forall {F:not-member M N1} {L:lookup M N2 D2}
exists {NE:nat`ne N1 N2}
true.
- : not-member-lookup-not-equal (not-member/< N2>N1) (lookup/= nat`eq/) (nat`ne/< N2>N1).
- : not-member-lookup-not-equal (not-member/< N1>N3) (lookup/> _ N0+1+N1=N2)
(nat`ne/< N2>N3)
<- plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- gt-transitive N2>N1 N1>N3 N2>N3.
- : not-member-lookup-not-equal (not-member/> _ X+1+N2=N1) (lookup/= nat`eq/) (nat`ne/> N1>N2)
<- plus-implies-gt X+1+N2=N1 nat`eq/ N1>N2.
- : not-member-lookup-not-equal (not-member/> F N4+1+N1=N3) (lookup/> L N0+1+N1=N2)
N3<>N2
<- not-member-lookup-not-equal F L N4<>N0
<- succ-preserves-ne N4<>N0 N4+1<>N0+1
<- plus-right-preserves-ne* N4+1<>N0+1 N4+1+N1=N3 N0+1+N1=N2 N3<>N2.
%worlds () (not-member-lookup-not-equal N1-not-in-member-of-M M^N2=D %{=>}% N1<>N2).
%total (F) (not-member-lookup-not-equal F _ _).
%theorem not-member-contradiction :
forall* {M} {N} {D}
forall {F:not-member (map/+ N D M) N}
exists {V:void}
true.
- : not-member-contradiction (not-member/< N>N) V
<- nat`gt-anti-reflexive N>N V.
- : not-member-contradiction (not-member/> _ N0+1+N=N) V
<- nat`plus-implies-gt N0+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N V.
%worlds () (not-member-contradiction _ _).
%total {} (not-member-contradiction _ _).
%theorem ne-implies-unit-map-not-member :
forall* {N1} {D} {N2}
forall {NE:nat`ne N1 N2}
exists {F:not-member (map/+ N1 D map/0) N2}
true.
- : ne-implies-unit-map-not-member
(nat`ne/< N1 not-member/0 N0+1+N1=N2)
<- nat`gt-implies-plus N1 N1>N2) (not-member/< N1>N2).
%worlds () (ne-implies-unit-map-not-member _ _).
%total { } (ne-implies-unit-map-not-member _ _).
%theorem plus-right-preserves-not-member* :
forall* {M} {N1} {D} {N2} {N} {N3} {N4}
forall {F:not-member (map/+ N1 D M) N2}
{P1:plus N1 N N3} {P2:plus N2 N N4}
exists {FP:not-member (map/+ N3 D M) N4}
true.
- : plus-right-preserves-not-member* (not-member/< N2>N1) N1+N=N3 N2+N=N4 (not-member/< N4>N3)
<- nat`plus-right-preserves-gt* N2>N1 N1+N=N3 N2+N=N4 N4>N3.
- : plus-right-preserves-not-member* (not-member/> F10 N0+1+N1=N2) N1+N=N3 N2+N=N4
(not-member/> F10 N0+1+N3=N4)
<- nat`plus-associative* N0+1+N1=N2 N2+N=N4 N1+N=N3 N0+1+N3=N4.
%worlds () (plus-right-preserves-not-member* _ _ _ _).
%total {} (plus-right-preserves-not-member* _ _ _ _).
%theorem not-member-lookup-implies-ne :
forall* {M1} {N1} {M2} {N2} {D2}
forall {L1:not-member M1 N1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
exists {NM:ne M1 M2}
true.
%theorem not-member-lookup-implies-ne/L :
forall* {M1} {N1} {M2} {N2} {D2} {B}
forall {L1:not-member M1 N1}
{L2:lookup M2 N2 D2}
{EN:nat`eq N1 N2}
{EM?:eq? M1 M2 B}
exists {NM:ne M1 M2}
true.
- : not-member-lookup-implies-ne F1 L2 EN NM
<- eq?-total EM?
<- not-member-lookup-implies-ne/L F1 L2 EN EM? NM.
- : not-member-lookup-implies-ne/L _ _ _ (eq?/no NM) NM.
- : not-member-lookup-implies-ne/L F1 L2 nat`eq/ eq?/yes NM
<- not-member-lookup-not-equal F1 L2 N<>N
<- nat`ne-anti-reflexive N<>N F
<- false-implies-ne F NM.
%worlds () (not-member-lookup-implies-ne/L _ _ _ _ _).
%total { } (not-member-lookup-implies-ne/L _ _ _ _ _).
%worlds () (not-member-lookup-implies-ne _ _ _ _).
%total { } (not-member-lookup-implies-ne _ _ _ _).
%%% Theorems about map/member
%theorem false-implies-member? :
forall* {M} {N} {D}
forall {F:void}
exists {MD:member? M N D}
true.
%worlds () (false-implies-member? _ _).
%total {} (false-implies-member? _ _).
%theorem member?-respects-eq :
forall* {M1} {N1} {B1} {M2} {N2} {B2}
forall {MD1:member? M1 N1 B1}
{EM:eq M1 M2}
{EN:nat`eq N1 N2}
{BE:bool`eq B1 B2}
exists {MD2:member? M2 N2 B2}
true.
- : member?-respects-eq MD eq/ nat`eq/ bool`eq/ MD.
%worlds () (member?-respects-eq _ _ _ _ _).
%total { } (member?-respects-eq _ _ _ _ _).
%theorem member?-deterministic :
forall* {M1} {N1} {B1} {M2} {N2} {B2}
forall {MD1:member? M1 N1 B1}
{MD2:member? M2 N2 B2}
{EM:eq M1 M2}
{EN:nat`eq N1 N2}
exists {BE:bool`eq B1 B2}
true.
- : member?-deterministic _ _ _ _ bool`eq/.
- : member?-deterministic (member?/in L) (member?/out F) eq/ nat`eq/ BE
<- not-member-lookup-not-equal F L NE
<- nat`ne-anti-reflexive NE V
<- bool`false-implies-eq V BE.
- : member?-deterministic (member?/out F) (member?/in L) eq/ nat`eq/ BE
<- not-member-lookup-not-equal F L NE
<- nat`ne-anti-reflexive NE V
<- bool`false-implies-eq V BE.
%worlds () (member?-deterministic _ _ _ _ _).
%total { } (member?-deterministic _ _ _ _ _).
%theorem member?-total* :
forall {M} {N}
exists {B} {MD:member? M N B}
true.
%% we need a lemma
%theorem member?-map/+-total :
forall {N1} {D1} {M1} {N2} {C} {CMP:nat`compare N1 N2 C}
exists {B} {MD:member? (map/+ N1 D1 M1) N2 B}
true.
%% and this lemma needs a lemma
%theorem member?-map/+-complete :
forall {N1} {D1} {M1} {N2} {N0} {P:plus (s N0) N1 N2}
{B} {MD1:member? M1 N0 B}
exists {MD:member? (map/+ N1 D1 M1) N2 B}
true.
- : member?-total* map/0 N false (member?/out not-member/0).
- : member?-total* (map/+ N1 D1 M1) N2 B MD
<- nat`compare-total* N1 N2 C CMP
<- member?-map/+-total N1 D1 M1 N2 C CMP B MD.
- : member?-map/+-total N1 D1 M1 N2 equal CMP true
(member?/in (lookup/= N1=N2))
<- equal-implies-eq CMP N1=N2.
- : member?-map/+-total N1 D1 M1 N2 greater CMP false
(member?/out (not-member/< N1>N2))
<- greater-implies-gt CMP N1>N2.
- : member?-map/+-total N1 D1 M1 N2 less CMP B MD
<- less-implies-lt CMP N2>N1
<- gt-implies-plus N2>N1 N0 N0+1+N1=N2
<- member?-total* M1 N0 B MD1
<- member?-map/+-complete N1 D1 M1 N2 N0 N0+1+N1=N2 B MD1 MD.
- : member?-map/+-complete N1 D1 M1 N2 N0 N0+1+N1=N2 true (member?/in L1)
(member?/in (lookup/> L1 N0+1+N1=N2)).
- : member?-map/+-complete N1 D1 M1 N2 N0 N0+1+N1=N2 false (member?/out F1)
(member?/out (not-member/> F1 N0+1+N1=N2)).
%worlds () (member?-map/+-complete _ _ _ _ _ _ _ _ _).
%total {} (member?-map/+-complete _ _ _ _ _ _ _ _ _).
%worlds () (member?-total* _ _ _ _)
(member?-map/+-total _ _ _ _ _ _ _ _).
%total (M M1) (member?-total* M _ _ _)
(member?-map/+-total _ _ M1 _ _ _ _ _).
%abbrev member?-total = member?-total* _ _ _.
%theorem in-implies-lookup :
forall* {M} {N}
forall {MD:member? M N true}
exists {D} {L:lookup M N D}
true.
- : in-implies-lookup (member?/in L) _ L.
%worlds () (in-implies-lookup _ _ _).
%total {} (in-implies-lookup _ _ _).
%theorem out-implies-not-member :
forall* {M} {N}
forall {MD:member? M N false}
exists {F:not-member M N}
true.
- : out-implies-not-member (member?/out F) F.
%worlds () (out-implies-not-member _ _).
%total {} (out-implies-not-member _ _).
%%% Theorems about disjoint
%theorem false-implies-disjoint :
forall* {M1} {M2}
forall {F:void}
exists {D:disjoint M1 M2}
true.
%worlds () (false-implies-disjoint _ _).
%total { } (false-implies-disjoint _ _).
%theorem disjoint-respects-eq :
forall* {M1} {M2} {M1P} {M2P}
forall {A:disjoint M1 M2} {E1:eq M1 M1P} {E2:eq M2 M2P}
exists {AP:disjoint M1P M2P}
true.
- : disjoint-respects-eq A eq/ eq/ A.
%worlds () (disjoint-respects-eq _ _ _ _).
%total {} (disjoint-respects-eq _ _ _ _).
%reduces A = AP (disjoint-respects-eq A _ _ AP).
%theorem disjoint/=-contradiction :
forall* {N1} {D1} {M1} {N2} {D2} {M2}
forall {A:disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{G:nat`eq N1 N2}
exists {F:void}
true.
- : disjoint/=-contradiction (disjoint/< _ N0+1+N=N) nat`eq/ F
<- nat`plus-implies-gt N0+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F.
- : disjoint/=-contradiction (disjoint/> _ N3+1+N=N) nat`eq/ F
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F.
%worlds () (disjoint/=-contradiction _ _ _).
%total { } (disjoint/=-contradiction _ _ _).
%theorem disjoint/<-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0}
forall {A:disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N0) N1 N2}
exists {AP:disjoint M1 (map/+ N0 D2 M2)}
true.
- : disjoint/<-inversion (disjoint/< A P) P' A'
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0P
<- map/+-preserves-eq N0=N0P nat`eq/ eq/ M022=M022'
<- disjoint-respects-eq A eq/ M022=M022' A'.
- : disjoint/<-inversion (disjoint/> A' N3+1+N2=N1) N0+1+N1=N2 A
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M311=M1
<- false-implies-eq F M2=M022
<- disjoint-respects-eq A' M311=M1 M2=M022 A.
%worlds () (disjoint/<-inversion _ _ _).
%total {} (disjoint/<-inversion _ _ _).
%reduces AP < A (disjoint/<-inversion A _ AP).
%theorem disjoint/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3}
forall {A:disjoint (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N3) N2 N1}
exists {AP:disjoint (map/+ N3 D1 M1) M2}
true.
- : disjoint/>-inversion (disjoint/> A P) P' A'
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N3+1=N3'+1
<- succ-cancels N3+1=N3'+1 N3=N3P
<- map/+-preserves-eq N3=N3P nat`eq/ eq/ M311=M311'
<- disjoint-respects-eq A M311=M311' eq/ A'.
- : disjoint/>-inversion (disjoint/< A' N0+1+N1=N2) N3+1+N2=N1 A
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M1=M311
<- false-implies-eq F M022=M2
<- disjoint-respects-eq A' M1=M311 M022=M2 A.
%worlds () (disjoint/>-inversion _ _ _).
%total { } (disjoint/>-inversion _ _ _).
%reduces AP < A (disjoint/>-inversion A _ AP).
%theorem disjoint-anti-reflexive :
forall* {M}
forall {D:disjoint M M}
exists {E:eq map/0 M}
true.
- : disjoint-anti-reflexive disjoint/L eq/.
- : disjoint-anti-reflexive disjoint/R eq/.
- : disjoint-anti-reflexive (A:disjoint (map/+ N D M) (map/+ N D M)) E
<- disjoint/=-contradiction A nat`eq/ F
<- false-implies-eq F E.
%worlds () (disjoint-anti-reflexive _ _).
%total { } (disjoint-anti-reflexive _ _).
%theorem disjoint-symmetric :
forall* {M1} {M2}
forall {D:disjoint M1 M2}
exists {D:disjoint M2 M1}
true.
- : disjoint-symmetric disjoint/L disjoint/R.
- : disjoint-symmetric disjoint/R disjoint/L.
- : disjoint-symmetric (disjoint/< D P) (disjoint/> D' P)
<- disjoint-symmetric D D'.
- : disjoint-symmetric (disjoint/> D P) (disjoint/< D' P)
<- disjoint-symmetric D D'.
%worlds () (disjoint-symmetric _ _).
%total (D) (disjoint-symmetric D _).
%theorem disjoint-lookup-contradiction :
forall* {M1} {M2} {N} {D1} {D2}
forall {A:disjoint M1 M2}
{L1:lookup M1 N D1} {L2:lookup M2 N D2}
exists {F:void}
true.
- : disjoint-lookup-contradiction disjoint/L L _ F
<- lookup-contradiction L F.
- : disjoint-lookup-contradiction disjoint/R _ L F
<- lookup-contradiction L F.
- : disjoint-lookup-contradiction (disjoint/< _ N0+1+N=N)
(lookup/= nat`eq/) (lookup/= nat`eq/) F
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F.
- : disjoint-lookup-contradiction (disjoint/< _ N0+1+N1=N2)
(lookup/= nat`eq/)
(lookup/> _ N3+1+N2=N1) F
<- plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- gt-anti-symmetric N2>N1 N1>N2 F.
- : disjoint-lookup-contradiction (disjoint/< D N0+1+N1=N2)
(lookup/> L1P N0P+1+N1=N2)
(lookup/= nat`eq/) F
<- plus-right-cancels N0P+1+N1=N2 N0+1+N1=N2 nat`eq/ nat`eq/ N0P+1=N0+1
<- succ-cancels N0P+1=N0+1 N0P=N0
<- lookup-respects-eq L1P eq/ N0P=N0 nat`eq/ L1
<- disjoint-lookup-contradiction D L1 (lookup/= nat`eq/) F.
- : disjoint-lookup-contradiction (disjoint/< D N0+1+N1=N2)
(lookup/> L1 N1P+1+N1=N)
(lookup/> L2 N2P+1+N2=N) F
<- plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- plus-associative-converse N0+N1+1=N2 N2P+1+N2=N NX
N2P+1+N0=NX NX+N1+1=N
<- plus-swap-succ N1P+1+N1=N N1P+N1+1=N
<- plus-right-cancels NX+N1+1=N N1P+N1+1=N nat`eq/ nat`eq/ NX=N1P
<- plus-respects-eq N2P+1+N0=NX nat`eq/ nat`eq/ NX=N1P N2P+1+N0=N1P
<- disjoint-lookup-contradiction D L1 (lookup/> L2 N2P+1+N0=N1P) F.
- : disjoint-lookup-contradiction (disjoint/> _ N3+1+N=N)
(lookup/= nat`eq/) (lookup/= nat`eq/) F
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F.
- : disjoint-lookup-contradiction (disjoint/> _ N3+1+N2=N1)
(lookup/> _ N3+1+N1=N2)
(lookup/= nat`eq/) F
<- plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- plus-implies-gt N3+1+N1=N2 nat`eq/ N2>N1
<- gt-anti-symmetric N1>N2 N2>N1 F.
- : disjoint-lookup-contradiction (disjoint/> D N3+1+N2=N1)
(lookup/= nat`eq/)
(lookup/> L2P N3P+1+N2=N1) F
<- plus-right-cancels N3P+1+N2=N1 N3+1+N2=N1 nat`eq/ nat`eq/ N3P+1=N3+1
<- succ-cancels N3P+1=N3+1 N3P=N3
<- lookup-respects-eq L2P eq/ N3P=N3 nat`eq/ L2
<- disjoint-lookup-contradiction D (lookup/= nat`eq/) L2 F.
- : disjoint-lookup-contradiction (disjoint/> D N3+1+N2=N1)
(lookup/> L1 N1P+1+N1=N)
(lookup/> L2 N2P+1+N2=N) F
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 N1P+1+N1=N NX
N1P+1+N3=NX NX+N2+1=N
<- plus-swap-succ N2P+1+N2=N N2P+N2+1=N
<- plus-right-cancels NX+N2+1=N N2P+N2+1=N nat`eq/ nat`eq/ NX=N2P
<- plus-respects-eq N1P+1+N3=NX nat`eq/ nat`eq/ NX=N2P N1P+1+N3=N2P
<- disjoint-lookup-contradiction D (lookup/> L1 N1P+1+N3=N2P) L2 F.
%worlds () (disjoint-lookup-contradiction _ _ _ _).
%total (D) (disjoint-lookup-contradiction D _ _ _).
%theorem shift-left-preserves-disjoint :
forall* {N} {D} {M1} {M2} {SM1}
forall {A:disjoint M1 M2} {S1:shift N M1 SM1}
exists {SA:disjoint SM1 (map/+ N D M2)}
true.
- : shift-left-preserves-disjoint _ shift/0 disjoint/L.
- : shift-left-preserves-disjoint M111*M2 (shift/+ N+1+N1=N1P)
(disjoint/> M111*M2 N1+1+N=N1P)
<- plus-swap-succ N+1+N1=N1P N+N1+1=N1P
<- plus-commutative N+N1+1=N1P N1+1+N=N1P.
%worlds () (shift-left-preserves-disjoint _ _ _).
%total { } (shift-left-preserves-disjoint _ _ _).
%theorem shift-left-preserves-disjoint-converse :
forall* {N} {D} {M1} {M2} {SM1}
forall {SA:disjoint SM1 (map/+ N D M2)} {S1:shift N M1 SM1}
exists {A:disjoint M1 M2}
true.
- : shift-left-preserves-disjoint-converse _ shift/0 disjoint/L.
- : shift-left-preserves-disjoint-converse M111*M222 (shift/+ N2+1+N3=N1)
M311*M2
<- plus-swap-succ N2+1+N3=N1 N2+N3+1=N1
<- plus-commutative N2+N3+1=N1 N3+1+N2=N1
<- disjoint/>-inversion M111*M222 N3+1+N2=N1 M311*M2.
%worlds () (shift-left-preserves-disjoint-converse _ _ _).
%total { } (shift-left-preserves-disjoint-converse _ _ _).
%theorem shift-right-preserves-disjoint :
forall* {N} {D} {M1} {M2} {SM2}
forall {A:disjoint M1 M2} {S2:shift N M2 SM2}
exists {SA:disjoint (map/+ N D M1) SM2}
true.
- : shift-right-preserves-disjoint _ shift/0 disjoint/R.
- : shift-right-preserves-disjoint M1*M222 (shift/+ N+1+N2=N2P)
(disjoint/< M1*M222 N2+1+N=N2P)
<- plus-swap-succ N+1+N2=N2P N+N2+1=N2P
<- plus-commutative N+N2+1=N2P N2+1+N=N2P.
%worlds () (shift-right-preserves-disjoint _ _ _).
%total { } (shift-right-preserves-disjoint _ _ _).
%theorem shift-right-preserves-disjoint-converse :
forall* {N} {D} {M1} {M2} {SM2}
forall {SA:disjoint (map/+ N D M1) SM2} {S2:shift N M2 SM2}
exists {A:disjoint M1 M2}
true.
- : shift-right-preserves-disjoint-converse _ shift/0 disjoint/R.
- : shift-right-preserves-disjoint-converse M111*M322 (shift/+ N1+1+N2=N3)
M1*M222
<- plus-swap-succ N1+1+N2=N3 N1+N2+1=N3
<- plus-commutative N1+N2+1=N3 N2+1+N1=N3
<- disjoint/<-inversion M111*M322 N2+1+N1=N3 M1*M222.
%worlds () (shift-right-preserves-disjoint-converse _ _ _).
%total { } (shift-right-preserves-disjoint-converse _ _ _).
%theorem shift-preserves-disjoint :
forall* {N} {M1} {M2} {SM1} {SM2}
forall {A:disjoint M1 M2}
{S1:shift N M1 SM1} {S2:shift N M2 SM2}
exists {SA:disjoint SM1 SM2}
true.
- : shift-preserves-disjoint _ shift/0 _ disjoint/L.
- : shift-preserves-disjoint _ _ shift/0 disjoint/R.
- : shift-preserves-disjoint (disjoint/< M1*M022 N0+1+N1=N2)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/< M1*M022 N0+1+N4=N5)
<- plus-swap-succ N+1+N1=N4 N+N1+1=N4
<- plus-commutative N+N1+1=N4 N1+1+N=N4
<- plus-commutative N0+1+N1=N2 N1+N0+1=N2
<- plus-associative-converse* N1+N0+1=N2 N+1+N2=N5 N+1+N1=N4 N4+N0+1=N5
<- plus-commutative N4+N0+1=N5 N0+1+N4=N5.
- : shift-preserves-disjoint (disjoint/> M311*M2 N3+1+N2=N1)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/> M311*M2 N3+1+N5=N4)
<- plus-swap-succ N+1+N2=N5 N+N2+1=N5
<- plus-commutative N+N2+1=N5 N2+1+N=N5
<- plus-commutative N3+1+N2=N1 N2+N3+1=N1
<- plus-associative-converse* N2+N3+1=N1 N+1+N1=N4 N+1+N2=N5 N5+N3+1=N4
<- plus-commutative N5+N3+1=N4 N3+1+N5=N4.
%worlds () (shift-preserves-disjoint _ _ _ _).
%total { } (shift-preserves-disjoint _ _ _ _).
%theorem shift-preserves-disjoint-converse :
forall* {N} {M1} {M2} {SM1} {SM2}
forall {SA:disjoint SM1 SM2}
{S1:shift N M1 SM1} {S2:shift N M2 SM2}
exists {A:disjoint M1 M2}
true.
- : shift-preserves-disjoint-converse _ shift/0 _ disjoint/L.
- : shift-preserves-disjoint-converse _ _ shift/0 disjoint/R.
- : shift-preserves-disjoint-converse (disjoint/< M1*M055 N0+1+N4=N5)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/< M1*M055 N0+1+N1=N2)
<- plus-commutative N+1+N1=N4 N1+N+1=N4
<- plus-swap-succ-converse N1+N+1=N4 N1+1+N=N4
<- plus-associative-converse N1+N+1=N4 N0+1+N4=N5 N2P N0+1+N1=N2P N2P+N+1=N5
<- plus-commutative N+1+N2=N5 N2+N+1=N5
<- plus-right-cancels N2P+N+1=N5 N2+N+1=N5 nat`eq/ nat`eq/ N2P=N2
<- plus-respects-eq N0+1+N1=N2P nat`eq/ nat`eq/ N2P=N2 N0+1+N1=N2.
- : shift-preserves-disjoint-converse (disjoint/> M611*M2 N6+1+N5=N4)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(disjoint/> M611*M2 N6+1+N2=N1)
<- plus-commutative N+1+N2=N5 N2+N+1=N5
<- plus-swap-succ-converse N2+N+1=N5 N2+1+N=N5
<- plus-associative-converse N2+N+1=N5 N6+1+N5=N4 N1P N6+1+N2=N1P N1P+N+1=N4
<- plus-commutative N+1+N1=N4 N1+N+1=N4
<- plus-right-cancels N1P+N+1=N4 N1+N+1=N4 nat`eq/ nat`eq/ N1P=N1
<- plus-respects-eq N6+1+N2=N1P nat`eq/ nat`eq/ N1P=N1 N6+1+N2=N1.
%worlds () (shift-preserves-disjoint-converse _ _ _ _).
%total { } (shift-preserves-disjoint-converse _ _ _ _).
%theorem ne-implies-disjoint :
forall* {N1} {D1} {N2} {D2}
forall {NE:nat`ne N1 N2}
exists {D:disjoint (map/+ N1 D1 map/0) (map/+ N2 D2 map/0)}
true.
- : ne-implies-disjoint (nat`ne/< N1 N1>N2)
(disjoint/> disjoint/R N3+1+N2=N1)
<- gt-implies-plus N1>N2 _ N3+1+N2=N1.
%worlds () (ne-implies-disjoint _ _).
%total { } (ne-implies-disjoint _ _).
%%% Theorems about size
%theorem false-implies-size :
forall* {M} {N}
forall {F:void}
exists {SZ:size M N}
true.
%worlds () (false-implies-size _ _).
%total { } (false-implies-size _ _).
%theorem size-total* :
forall {M}
exists {N} {MX:size M N}
true.
- : size-total* map/0 _ size/0.
- : size-total* _ _ (size/+ SZ)
<- size-total* _ _ SZ.
%worlds () (size-total* _ _ _).
%total (M) (size-total* M _ _).
%abbrev size-total = size-total* _ _.
%theorem size-deterministic :
forall* {M1} {M2} {N1} {N2}
forall {SZ1:size M1 N1} {SZ2:size M2 N2} {EM:eq M1 M2}
exists {EN:nat`eq N1 N2}
true.
- : size-deterministic size/0 size/0 eq/ nat`eq/.
- : size-deterministic (size/+ N1=|M1|) (size/+ N2=|M2|) eq/ N1+1=N2+1
<- size-deterministic N1=|M1| N2=|M2| eq/ N1=N2
<- succ-deterministic N1=N2 N1+1=N2+1.
%worlds () (size-deterministic _ _ _ _).
%total (S) (size-deterministic S _ _ _).
%%% Theorems about bound
%theorem false-implies-bound :
forall* {M} {N}
forall {F:void}
exists {MX:bound M N}
true.
%worlds () (false-implies-bound _ _).
%total { } (false-implies-bound _ _).
%theorem bound-total* :
forall {M}
exists {N} {MX:bound M N}
true.
- : bound-total* map/0 _ bound/0.
- : bound-total* _ _ (bound/+ P MX)
<- bound-total* _ _ MX
<- plus-total P.
%worlds () (bound-total* _ _ _).
%total (M) (bound-total* M _ _).
%abbrev bound-total = bound-total* _ _.
%theorem ge-bound-implies-not-member :
forall* {M} {X} {N}
forall {B:bound M X} {G:nat`ge N X}
exists {F:not-member M N}
true.
- : ge-bound-implies-not-member bound/0 _ not-member/0.
- : ge-bound-implies-not-member (bound/+ M1+1+X1=X B) N>=X (not-member/> F1 N1+1+M1=N)
<- nat`ge-implies-plus N>=X Y1 Y1+X=N
<- nat`plus-commutative M1+1+X1=X X1+M1+1=X
<- nat`plus-associative-converse X1+M1+1=X Y1+X=N N1 Y1+X1=N1 N1+M1+1=N
<- plus-swap-succ-converse N1+M1+1=N N1+1+M1=N
<- plus-implies-ge Y1+X1=N1 N1>=X1
<- ge-bound-implies-not-member B N1>=X1 F1.
%worlds () (ge-bound-implies-not-member _ _ _).
%total (B) (ge-bound-implies-not-member B _ _).
%%% Theorems about shift
%theorem false-implies-shift :
forall* {M} {N} {M'}
forall {F:void}
exists {S:shift N M M'}
true.
%worlds () (false-implies-shift _ _).
%total { } (false-implies-shift _ _).
%theorem shift-respects-eq :
forall* {N} {M1} {M2} {N'} {M1'} {M2'}
forall {S:shift N M1 M2}
{EN:nat`eq N N'} {E1:eq M1 M1'} {E2:eq M2 M2'}
exists {S':shift N' M1' M2'}
true.
- : shift-respects-eq S nat`eq/ eq/ eq/ S.
%worlds () (shift-respects-eq _ _ _ _ _).
%total { } (shift-respects-eq _ _ _ _ _).
%theorem shift-total* :
forall {N} {M1}
exists {M2} {S:shift N M1 M2}
true.
- : shift-total* N map/0 map/0 shift/0.
- : shift-total* N1 (map/+ N2 D M) (map/+ N3 D M) (shift/+ N1+1+N2=N3)
<- plus-total N1+1+N2=N3.
%worlds () (shift-total* _ _ _ _).
%total { } (shift-total* _ _ _ _).
%abbrev shift-total = shift-total* _ _ _.
%theorem shift-deterministic :
forall* {N} {M1} {M2} {N'} {M1'} {M2'}
forall {S:shift N M1 M2} {S':shift N' M1' M2'}
{EN:nat`eq N N'} {EM1:eq M1 M1'}
exists {EM2:eq M2 M2'}
true.
- : shift-deterministic shift/0 shift/0 nat`eq/ eq/ eq/.
- : shift-deterministic (shift/+ N1+1+N2=N3) (shift/+ N1+1+N2=N3') nat`eq/ eq/ E
<- plus-deterministic N1+1+N2=N3 N1+1+N2=N3' nat`eq/ nat`eq/ N3=N3P
<- map/+-preserves-eq N3=N3P nat`eq/ eq/ E.
%worlds () (shift-deterministic _ _ _ _ _).
%total { } (shift-deterministic _ _ _ _ _).
%theorem shifts-add :
forall* {N1} {N2} {N3} {M0} {M1} {M3}
forall {S1:shift N1 M0 M1} {S2:shift N2 M1 M3} {P:plus (s N1) N2 N3}
exists {S3:shift N3 M0 M3}
true.
- : shifts-add shift/0 shift/0 _ shift/0.
- : shifts-add (shift/+ N1+1+N4=N5) (shift/+ N2+1+N5=N7) N1+1+N2=N3
(shift/+ N3+1+N4=N7)
<- plus-total N3+1+N4=N7'
<- plus-swap-succ N3+1+N4=N7' N3+N4+1=N7'
<- plus-swap-succ N1+1+N2=N3 N1+N2+1=N3
<- plus-swap-succ N1+1+N4=N5 N1+N4+1=N5
<- plus-commutative N1+N2+1=N3 N2+1+N1=N3
<- plus-associative* N2+1+N1=N3 N3+N4+1=N7' N1+N4+1=N5 N2+1+N5=N7'
<- plus-deterministic N2+1+N5=N7' N2+1+N5=N7 nat`eq/ nat`eq/ N7'=N7
<- plus-respects-eq N3+1+N4=N7' nat`eq/ nat`eq/ N7'=N7 N3+1+N4=N7.
%worlds () (shifts-add _ _ _ _).
%total { } (shifts-add _ _ _ _).
%theorem shifts-add-converse :
forall* {N1} {N2} {N3} {M0} {M3}
forall {S3:shift N3 M0 M3} {P:plus (s N1) N2 N3}
exists {M1} {S1:shift N1 M0 M1} {S2:shift N2 M1 M3}
true.
- : shifts-add-converse S3 P M1 S1 S2
<- shift-total S1
<- shift-total S2'
<- shifts-add S1 S2' P S3'
<- shift-deterministic S3' S3 nat`eq/ eq/ M3'=M3
<- shift-respects-eq S2' nat`eq/ eq/ M3'=M3 S2.
%worlds () (shifts-add-converse _ _ _ _ _).
%total { } (shifts-add-converse _ _ _ _ _).
%theorem shift-preserves-lookup :
forall* {M1} {N1} {D} {N0} {M2}
forall {L1:lookup M1 N1 D} {S:shift N0 M1 M2}
exists {N2} {P:plus (s N0) N1 N2} {L2:lookup M2 N2 D}
true.
- : shift-preserves-lookup (lookup/= nat`eq/) (shift/+ N0+1+N1=N2) _
N0+1+N1=N2 (lookup/= nat`eq/).
- : shift-preserves-lookup (lookup/> L N3+1+N1=N4) (shift/+ N0+1+N1=N2) _
N0+1+N4=N5 (lookup/> L N3+1+N2=N5)
<- plus-total N0+1+N4=N5
<- plus-commutative N3+1+N1=N4 N1+N3+1=N4
<- plus-associative-converse* N1+N3+1=N4 N0+1+N4=N5 N0+1+N1=N2 N2+N3+1=N5
<- plus-commutative N2+N3+1=N5 N3+1+N2=N5.
%worlds () (shift-preserves-lookup _ _ _ _ _).
%total { } (shift-preserves-lookup _ _ _ _ _).
%theorem shift-preserves-lookup* :
forall* {M1} {N1} {D} {N0} {M2} {N2}
forall {L1:lookup M1 N1 D} {S:shift N0 M1 M2}
{P:plus (s N0) N1 N2}
exists {L2:lookup M2 N2 D}
true.
- : shift-preserves-lookup* L1 S P L2
<- shift-preserves-lookup L1 S _ P' L2'
<- plus-deterministic P' P nat`eq/ nat`eq/ N2'=N2
<- lookup-respects-eq L2' eq/ N2'=N2 nat`eq/ L2.
%worlds () (shift-preserves-lookup* _ _ _ _).
%total { } (shift-preserves-lookup* _ _ _ _).
%theorem shift-preserves-lookup-converse :
forall* {M1} {N0} {D} {N2} {M2}
forall {L2:lookup M2 N2 D} {S:shift N0 M1 M2}
exists {N1} {P:plus (s N0) N1 N2} {L1:lookup M1 N1 D}
true.
- : shift-preserves-lookup-converse (lookup/= nat`eq/) (shift/+ N0+1+N1=N2) _
N0+1+N1=N2 (lookup/= nat`eq/).
- : shift-preserves-lookup-converse (lookup/> L N3+1+N2=N5) (shift/+ N0+1+N1=N2)
_ N0+1+N4=N5 (lookup/> L N3+1+N1=N4)
<- plus-commutative N0+1+N1=N2 N1+N0+1=N2
<- plus-associative-converse N1+N0+1=N2 N3+1+N2=N5 N4 N3+1+N1=N4 N4+N0+1=N5
<- plus-commutative N4+N0+1=N5 N0+1+N4=N5.
%worlds () (shift-preserves-lookup-converse _ _ _ _ _).
%total { } (shift-preserves-lookup-converse _ _ _ _ _).
%theorem shift-preserves-lookup-converse* :
forall* {M1} {N1} {D} {N2} {M2} {N0}
forall {L2:lookup M2 N2 D} {S:shift N0 M1 M2}
{P:plus (s N0) N1 N2}
exists {L1:lookup M1 N1 D}
true.
- : shift-preserves-lookup-converse* L2 S P L1
<- shift-preserves-lookup-converse L2 S _ P' L1'
<- plus-left-cancels P' P nat`eq/ nat`eq/ N1'=N1
<- lookup-respects-eq L1' eq/ N1'=N1 nat`eq/ L1.
%worlds () (shift-preserves-lookup-converse* _ _ _ _).
%total { } (shift-preserves-lookup-converse* _ _ _ _).
%theorem shift-preserves-update :
forall* {M1} {N1} {D} {M1'} {N0} {M2}
forall {U1:update M1 N1 D M1'}
{S:shift N0 M1 M2}
exists {N2} {M2'}
{P:plus (s N0) N1 N2}
{SS:shift N0 M1' M2'}
{U2:update M2 N2 D M2'}
true.
- : shift-preserves-update update/0 shift/0 _ _ P (shift/+ P) update/0
<- plus-total P.
- : shift-preserves-update (update/= nat`eq/) (shift/+ P) _ _ P (shift/+ P)
(update/= nat`eq/).
- : shift-preserves-update (update/< N4+1+N1=N3) (shift/+ N0+1+N3=N5) _ _
N0+1+N1=N2 (shift/+ N0+1+N1=N2)
(update/< N4+1+N2=N5)
<- plus-commutative N4+1+N1=N3 N1+N4+1=N3
<- plus-associative-converse N1+N4+1=N3 N0+1+N3=N5 _ N0+1+N1=N2 N2+N4+1=N5
<- plus-commutative N2+N4+1=N5 N4+1+N2=N5.
- : shift-preserves-update (update/> U N4+1+N3=N1) (shift/+ N0+1+N3=N5) _ _
N0+1+N1=N2 (shift/+ N0+1+N3=N5)
(update/> U N4+1+N5=N2)
<- plus-total N0+1+N1=N2
<- plus-commutative N4+1+N3=N1 N3+N4+1=N1
<- plus-associative-converse* N3+N4+1=N1 N0+1+N1=N2 N0+1+N3=N5 N5+N4+1=N2
<- plus-commutative N5+N4+1=N2 N4+1+N5=N2.
%worlds () (shift-preserves-update _ _ _ _ _ _ _).
%total { } (shift-preserves-update _ _ _ _ _ _ _).
%theorem shift-preserves-size :
forall* {M} {N1} {N2} {S2M}
forall {SZ:size M N1} {SH:shift N2 M S2M}
exists {SHSZ:size S2M N1}
true.
- : shift-preserves-size size/0 shift/0 size/0.
- : shift-preserves-size (size/+ SZ) (shift/+ _) (size/+ SZ).
%worlds () (shift-preserves-size _ _ _).
%total { } (shift-preserves-size _ _ _).
%%% Theorems about disjoint?
%theorem disjoint?-total* :
forall {M1} {M2}
exists {B} {D:disjoint? M1 M2 B}
true.
- : disjoint?-total* _ _ _ (disjoint?/yes disjoint/L).
- : disjoint?-total* _ _ _ (disjoint?/yes disjoint/R).
%theorem disjoint?-total*/+ :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {C}
forall {S1} {S2} {SZ1:size M1 S1} {SZ2:size M2 S2} {CMP:nat`compare N1 N2 C}
exists {B} {D:disjoint? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
%theorem disjoint?-total*/< :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0} {B1}
forall {P:plus (s N0) N1 N2}
{D?1:disjoint? M1 (map/+ N0 D2 M2) B1}
exists {B} {D:disjoint? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
%theorem disjoint?-total*/> :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3} {B1}
forall {P:plus (s N3) N2 N1}
{D?1:disjoint? (map/+ N3 D1 M1) M2 B1}
exists {B} {D:disjoint? (map/+ N1 D1 M1) (map/+ N2 D2 M2) B}
true.
- : disjoint?-total* _ _ _ D?
<- size-total SZ1
<- size-total SZ2
<- nat`compare-total CMP
<- disjoint?-total*/+ _ _ SZ1 SZ2 CMP _ D?.
- : disjoint?-total*/+ _ _ _ _ (nat`compare/=) _
(disjoint?/no (lookup/= nat`eq/) (lookup/= nat`eq/)).
- : disjoint?-total*/+ _ _ _ _ (nat`compare/< N2>N1) _ D?
<- gt-implies-plus N2>N1 _ N0+1+N1=N2
<- disjoint?-total*/< N0+1+N1=N2 (disjoint?/yes disjoint/L) _ D?.
- : disjoint?-total*/+ _ _ (size/+ SZ1) SZ2 (nat`compare/< N2>N1) _ D?
<- gt-implies-plus N2>N1 _ N0+1+N1=N2
<- nat`compare-total CMP
<- disjoint?-total*/+ _ _ SZ1 SZ2 CMP _ D?1
<- disjoint?-total*/< N0+1+N1=N2 D?1 _ D?.
- : disjoint?-total*/< N0+1+N1=N2 (disjoint?/yes M1*M022) _
(disjoint?/yes (disjoint/< M1*M022 N0+1+N1=N2)).
- : disjoint?-total*/< N0+1+N1=N2 (disjoint?/no M1^N3=D1 M022^N3=D2) _
(disjoint?/no (lookup/> M1^N3=D1 N3+1+N1=N4) M222^N4=D2)
<- plus-total N3+1+N1=N4
<- plus-swap-succ N3+1+N1=N4 N3+N1+1=N4
<- plus-commutative N3+N1+1=N4 N1+1+N3=N4
<- plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- plus-commutative N0+N1+1=N2 N1+1+N0=N2
<- shift-preserves-lookup* M022^N3=D2 (shift/+ N1+1+N0=N2) N1+1+N3=N4
M222^N4=D2.
%worlds () (disjoint?-total*/< _ _ _ _).
%total { } (disjoint?-total*/< _ _ _ _).
- : disjoint?-total*/+ _ _ _ _ (nat`compare/> N1>N2) _ D?
<- gt-implies-plus N1>N2 _ N3+1+N2=N1
<- disjoint?-total*/> N3+1+N2=N1 (disjoint?/yes disjoint/R) _ D?.
- : disjoint?-total*/+ _ _ SZ1 (size/+ SZ2) (nat`compare/> N1>N2) _ D?
<- gt-implies-plus N1>N2 _ N3+1+N2=N1
<- nat`compare-total CMP
<- disjoint?-total*/+ _ _ SZ1 SZ2 CMP _ D?1
<- disjoint?-total*/> N3+1+N2=N1 D?1 _ D?.
- : disjoint?-total*/> P (disjoint?/yes D) _ (disjoint?/yes (disjoint/> D P)).
- : disjoint?-total*/> N3+1+N2=N1 (disjoint?/no M311^N4=D1 M2^N4=D2) _
(disjoint?/no M111^N5=D1 (lookup/> M2^N4=D2 N4+1+N2=N5))
<- plus-total N4+1+N2=N5
<- plus-swap-succ N4+1+N2=N5 N4+N2+1=N5
<- plus-commutative N4+N2+1=N5 N2+1+N4=N5
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-commutative N3+N2+1=N1 N2+1+N3=N1
<- shift-preserves-lookup* M311^N4=D1 (shift/+ N2+1+N3=N1) N2+1+N4=N5
M111^N5=D1.
%worlds () (disjoint?-total*/> _ _ _ _).
%total { } (disjoint?-total*/> _ _ _ _).
%worlds () (disjoint?-total*/+ _ _ _ _ _ _ _).
%total [S1 S2] (disjoint?-total*/+ S1 S2 _ _ _ _ _).
%worlds () (disjoint?-total* _ _ _ _).
%total { } (disjoint?-total* _ _ _ _).
%abbrev disjoint?-total = disjoint?-total* _ _ _.
%%% Theorems about update
%theorem false-implies-update :
forall* {M} {N} {D} {M'}
forall {F:void}
exists {U:update M N D M'}
true.
%worlds () (false-implies-update _ %{=>}% M^N=D->M').
%total {} (false-implies-update _ _).
%theorem update-respects-eq :
forall* {M1} {N} {D} {M2} {M1P} {NP} {DP} {M2P}
forall {U:update M1 N D M2} {EM1:eq M1 M1P}
{EN:nat`eq N NP} {ED:nat`eq D DP} {EM2:eq M2 M2P}
exists {UP:update M1P NP DP M2P}
true.
- : update-respects-eq U eq/ nat`eq/ nat`eq/ eq/ U.
%worlds () (update-respects-eq M1^N=D->M2 M1=M1' N=N' D=D' M2=M2'
%{=>}% M1'^N'=D'->M2').
%total {} (update-respects-eq _ _ _ _ _ _).
%reduces U = U' (update-respects-eq U _ _ _ _ U').
%%% technical lemmas to help prove reduction arguments
update-eq : {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'}
update M1 N1 D1 M1' -> update M2 N2 D2 M2' -> type.
update-eq/ : update-eq M1 N1 D1 M1' M1 N1 D1 M1' U U.
%theorem false-implies-update-eq :
forall* {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'} {U} {U'}
forall {F:void}
exists {UE:update-eq M1 N1 D1 M1' M2 N2 D2 M2' U U'}
true.
%worlds () (false-implies-update-eq _ _).
%total { } (false-implies-update-eq _ _).
%theorem meta-update-eq :
forall* {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'}
forall {U} {U'} {UE:update-eq M1 N1 D1 M1' M2 N2 D2 M2' U U'}
true.
- : meta-update-eq U U (update-eq/).
%worlds () (meta-update-eq _ _ _).
%total { } (meta-update-eq _ _ _).
%reduces U = U' (meta-update-eq U U' _).
%%% inversion lemmas
%theorem update/=-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2}
forall {U:update (map/+ N1 D1 M1) N2 D2 M2} {E:nat`eq N1 N2}
exists {EM:eq (map/+ N2 D2 M1) M2}
true.
- : update/=-inversion (update/= nat`eq/) nat`eq/ eq/.
- : update/=-inversion (update/< N3+1+N=N) nat`eq/ E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update/=-inversion (update/> U1022 N3+1+N=N) nat`eq/ E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
%worlds () (update/=-inversion _ _ _).
%total { } (update/=-inversion _ _ _).
%theorem update/<-inversion:
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3}
forall {U:update (map/+ N1 D1 M1) N2 D2 M2} {P:plus (s N3) N2 N1}
exists {E:eq (map/+ N2 D2 (map/+ N3 D1 M1)) M2}
true.
- : update/<-inversion (update/= nat`eq/) N3+1+N=N E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update/<-inversion (update/< N3+1+N2=N1) N3P+1+N2=N1 E
<- nat`plus-right-cancels N3P+1+N2=N1 N3+1+N2=N1 nat`eq/ nat`eq/ N3P+1=N3+1
<- nat`succ-cancels N3P+1=N3+1 N3P=N3
<- map/+-preserves-eq N3P=N3 nat`eq/ eq/ M311P=M311
<- map/+-preserves-eq nat`eq/ nat`eq/ M311P=M311 E.
- : update/<-inversion (update/> _ N0+1+N1=N2) N3+1+N2=N1 E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (update/<-inversion _ _ _).
%total { } (update/<-inversion _ _ _).
%theorem update/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M} {N0}
forall {U:update (map/+ N1 D1 M1) N2 D2 M} {P:plus (s N0) N1 N2}
exists {M2} {UP:update M1 N0 D2 M2} {E:eq (map/+ N1 D1 M2) M}
true.
% a little more complex than might be expected
% because we want to prove reduction
- : update/>-inversion (update/= nat`eq/: update (map/+ N D1 M1) N D2
(map/+ N D2 M1))
N0+1+N=N M1 U' E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E
<- false-implies-update F U'
<- false-implies-update-eq F
(UE:update-eq (map/+ N D1 M1) N D2 (map/+ N D2 M1)
(map/+ N D1 M1) N D2 (map/+ N D1 M1) _ _)
<- meta-update-eq (update/= nat`eq/) (update/> U' N0+1+N=N) UE.
- : update/>-inversion (update/< N3+1+N2=N1: update (map/+ N1 D1 M1) _ _ _)
N0+1+N1=N2 M1 U' E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-update F U'
<- false-implies-eq F E
<- false-implies-update-eq F
(UE:update-eq (map/+ N1 D1 M1) N2 D2 (map/+ N2 D2 (map/+ N3 D1 M1))
(map/+ N1 D1 M1) N2 D2 (map/+ N1 D1 M1) _ _)
<- meta-update-eq (update/< N3+1+N2=N1) (update/> U' N0+1+N1=N2) UE.
- : update/>-inversion (update/> U N0+1+N1=N2) N0P+1+N1=N2 _ UP eq/
<- nat`plus-right-cancels N0+1+N1=N2 N0P+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0P+1
<- nat`succ-cancels N0+1=N0P+1 N0=N0P
<- update-respects-eq U eq/ N0=N0P nat`eq/ eq/ UP.
%worlds () (update/>-inversion _ _ _ _ _).
%total { } (update/>-inversion _ _ _ _ _).
%reduces U' < U (update/>-inversion U _ _ U' _).
%theorem update-deterministic :
forall* {M1} {N1} {D1} {M1'} {M2} {N2} {D2} {M2'}
forall {U1:update M1 N1 D1 M1'} {U2:update M2 N2 D2 M2'}
{EM:eq M1 M2} {EN:nat`eq N1 N2} {ED:nat`eq D1 D2}
exists {EM':eq M1' M2'}
true.
- : update-deterministic update/0 update/0 eq/ nat`eq/ nat`eq/ eq/.
- : update-deterministic (update/= nat`eq/) (update/= nat`eq/) eq/ nat`eq/ nat`eq/ eq/.
- : update-deterministic (update/< N3+1+N2=N1) (update/< N3'+1+N2=N1)
eq/ nat`eq/ nat`eq/ M1'=M2'
<- plus-right-cancels N3+1+N2=N1 N3'+1+N2=N1 nat`eq/ nat`eq/ SN3=SN3'
<- succ-cancels SN3=SN3' N3E
<- map/+-preserves-eq N3E nat`eq/ eq/ MM1=MM2
<- map/+-preserves-eq nat`eq/ nat`eq/ MM1=MM2 M1'=M2'.
- : update-deterministic (update/> F1^N0=D2->F2 N0+1+N1=N2)
(update/> F1^N0'=D2->F2' N0'+1+N1=N2)
eq/ nat`eq/ nat`eq/ M1'=M2'
<- plus-right-cancels N0+1+N1=N2 N0'+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0'
<- update-deterministic F1^N0=D2->F2 F1^N0'=D2->F2' eq/ N0=N0'
nat`eq/ F2=F2'
<- map/+-preserves-eq nat`eq/ nat`eq/ F2=F2' M1'=M2'.
%% contradiction cases:
- : update-deterministic (update/= nat`eq/) (update/< N3+1+N=N) eq/ nat`eq/ nat`eq/ E
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/= nat`eq/) (update/> _ N0+1+N=N) eq/ nat`eq/ nat`eq/ E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/< N3+1+N=N) (update/= nat`eq/) eq/ nat`eq/ nat`eq/ E
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/< N3+1+N2=N1) (update/> _ N0+1+N1=N2)
eq/ nat`eq/ nat`eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
- : update-deterministic (update/> _ N0+1+N=N) (update/= nat`eq/) eq/ nat`eq/ nat`eq/ E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : update-deterministic (update/> _ N0+1+N1=N2) (update/< N3+1+N2=N1)
eq/ nat`eq/ nat`eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (update-deterministic M1^N1=D1->M1' M2^N2=D2->M2' M1=M2 N1=N2 D1=D2
%{=>}% M1'=M2').
%total (U) (update-deterministic U _ _ _ _ _).
%theorem update-total* :
forall {M} {N} {D}
exists {M'} {U:update M N D M'}
true.
%% we need a mutually recursive lemma
%theorem update-map/+-total :
forall {N1} {D1} {M1} {N2} {D2} {C} {CMP:nat`compare N1 N2 C}
exists {M2} {U:update (map/+ N1 D1 M1) N2 D2 M2}
true.
- : update-total* map/0 N D (map/+ N D map/0) update/0.
- : update-total* (map/+ N1 D1 M1) N2 D2 M2 U
<- nat`compare-total* N1 N2 C CMP
<- update-map/+-total N1 D1 M1 N2 D2 C CMP M2 U.
- : update-map/+-total N1 D1 M1 N2 D2 equal CMP (map/+ N2 D2 M1) (update/= N1=N2)
<- equal-implies-eq CMP N1=N2.
- : update-map/+-total N1 D1 M1 N2 D2 less CMP (map/+ N1 D1 M1')
(update/> U1 N0+1+N1=N2)
<- less-implies-lt CMP N2>N1
<- gt-implies-plus N2>N1 N0 N0+1+N1=N2
<- update-total* M1 N0 D2 M1' U1.
- : update-map/+-total N1 D1 M1 N2 D2 greater CMP (map/+ N2 D2 (map/+ N3 D1 M1))
(update/< N3+1+N2=N1)
<- greater-implies-gt CMP N1>N2
<- gt-implies-plus N1>N2 N3 N3+1+N2=N1.
%worlds () (update-total* M N D %{=>}% M' M^N=D->M')
(update-map/+-total _ _ _ _ _ _ _ _ _).
%total (M1 M2) (update-total* M1 _ _ _ _) (update-map/+-total _ _ M2 _ _ _ _ _ _).
%abbrev update-total = update-total* _ _ _ _.
%theorem lookup-implies-update :
forall* {F} {N} {D}
forall {L:lookup F N D}
exists {U:update F N D F}
true.
- : lookup-implies-update (lookup/= nat`eq/) (update/= nat`eq/).
- : lookup-implies-update (lookup/> L P) (update/> U P)
<- lookup-implies-update L U.
%worlds () (lookup-implies-update _ _).
%total (L) (lookup-implies-update L _).
%theorem update-implies-lookup :
forall* {F} {N} {D} {F'}
forall {U:update F N D F'}
exists {L:lookup F' N D}
true.
- : update-implies-lookup update/0 (lookup/= nat`eq/).
- : update-implies-lookup (update/= nat`eq/) (lookup/= nat`eq/).
- : update-implies-lookup (update/< _) (lookup/= nat`eq/).
- : update-implies-lookup (update/> F^N0=D2->F' N0+1+N1=N2)
(lookup/> F'^N0=D2 N0+1+N1=N2)
<- update-implies-lookup F^N0=D2->F' F'^N0=D2.
%worlds () (update-implies-lookup F^N=D->F' %{=>}% F'^N=D).
%total (U) (update-implies-lookup U _).
%theorem update-preserves-lookup :
forall* {F} {N1} {D1} {F'} {N2} {D2}
forall {L:lookup F N2 D2} {U:update F N1 D1 F'} {X:nat`ne N2 N1}
exists {L':lookup F' N2 D2}
true.
%% update/0 is impossible
- : update-preserves-lookup (lookup/= nat`eq/) (update/= nat`eq/) N<>N L'
<- nat`ne-anti-reflexive N<>N FALSE
<- false-implies-lookup FALSE L'.
- : update-preserves-lookup (lookup/> L1 P1) (update/= nat`eq/) _ (lookup/> L1 P1).
- : update-preserves-lookup (lookup/= nat`eq/) (update/< N3+1+N2=N1) _
(lookup/> (lookup/= nat`eq/) N3+1+N2=N1).
- : update-preserves-lookup (lookup/> L N0+1+N1=N2') (update/< N3+1+N2=N1) _
(lookup/> (lookup/> L N0+1+N3=N4)
N4+1+N2=N2')
<- plus-left-decrease N3+1+N2=N1 N1-1 N1=N1-1+1 N3+N2=N1-1
<- plus-right-increase N3+N2=N1-1 N3+N2+1=N1-1+1
<- nat`eq-symmetric N1=N1-1+1 N1-1+1=N1
<- plus-respects-eq N3+N2+1=N1-1+1 nat`eq/ nat`eq/ N1-1+1=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 N0+1+N1=N2' N4 N0+1+N3=N4
N4+N2+1=N2'
<- plus-swap-succ-converse N4+N2+1=N2' N4+1+N2=N2'.
- : update-preserves-lookup (lookup/= nat`eq/) (update/> _ _) _ (lookup/= nat`eq/).
- : update-preserves-lookup (lookup/> L N0+1+N1=N2)
((update/> U N0'+1+N1=N2')
: update (map/+ N1 D1 M1) N2' D'
(map/+ N1 D1 M1'))
N2<>N2'
((lookup/> L' N0+1+N1=N2)
: lookup (map/+ N1 D1 M1') N2 D)
<- plus-right-cancels-ne N0+1+N1=N2 N0'+1+N1=N2' nat`eq/ N2<>N2' N0+1<>N0'+1
<- succ-preserves-ne-converse N0+1<>N0'+1 N0<>N0'
<- update-preserves-lookup L U N0<>N0' L'.
%worlds () (update-preserves-lookup F^N2=D2 F^N1=D1->F' N1<>N2 F'^N2=D2).
%total (L) (update-preserves-lookup L _ _ _).
%theorem update-preserves-lookup-converse :
forall* {F1} {N1} {D1} {F2} {N2} {D2}
forall {L2:lookup F2 N2 D2} {U:update F1 N1 D1 F2} {X:nat`ne N2 N1}
exists {L1:lookup F1 N2 D2}
true.
- : update-preserves-lookup-converse (lookup/= nat`eq/) update/0 N<>N L1
<- nat`ne-anti-reflexive N<>N F
<- false-implies-lookup F L1.
- : update-preserves-lookup-converse (lookup/= nat`eq/) (update/= nat`eq/) N<>N
L1
<- nat`ne-anti-reflexive N<>N F
<- false-implies-lookup F L1.
- : update-preserves-lookup-converse (lookup/= nat`eq/) (update/< N3+1+N2=N1)
N<>N L1
<- nat`ne-anti-reflexive N<>N F
<- false-implies-lookup F L1.
- : update-preserves-lookup-converse (lookup/= nat`eq/) (update/> _ _) _
(lookup/= nat`eq/).
- : update-preserves-lookup-converse (lookup/> L1 P) (update/= nat`eq/) _
(lookup/> L1 P).
- : update-preserves-lookup-converse (lookup/> (lookup/= nat`eq/) N3+1+N2=N4)
(update/< N3+1+N2=N1) _
(lookup/= N1=N4)
<- plus-deterministic N3+1+N2=N1 N3+1+N2=N4 nat`eq/ nat`eq/ N1=N4.
- : update-preserves-lookup-converse (lookup/> (lookup/> L1 N6+1+N3=N5)
N5+1+N2=N4)
(update/< N3+1+N2=N1) _
(lookup/> L1 N6+1+N1=N4)
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-swap-succ N5+1+N2=N4 N5+N2+1=N4
<- plus-associative* N6+1+N3=N5 N5+N2+1=N4 N3+N2+1=N1 N6+1+N1=N4.
- : update-preserves-lookup-converse (lookup/> L2 N5+1+N1=N4)
(update/> U1 N0+1+N1=N2) N4<>N2
(lookup/> L1 N5+1+N1=N4)
<- plus-right-cancels-ne N5+1+N1=N4 N0+1+N1=N2 nat`eq/ N4<>N2 N5+1<>N0+1
<- succ-preserves-ne-converse N5+1<>N0+1 N5<>N0
<- update-preserves-lookup-converse L2 U1 N5<>N0 L1.
%worlds () (update-preserves-lookup-converse _ _ _ _).
%total (L) (update-preserves-lookup-converse L _ _ _).
%theorem update-preserves-not-member :
forall* {M1} {N1} {N2} {D} {M2}
forall {F1:not-member M1 N1} {U:update M1 N2 D M2} {N:nat`ne N1 N2}
exists {F2:not-member M2 N1}
true.
- : update-preserves-not-member not-member/0 update/0 (nat`ne/< N>M) (not-member/< N>M).
- : update-preserves-not-member not-member/0 update/0 (nat`ne/> M>N)
(not-member/> not-member/0 M1+1+N=M)
<- gt-implies-plus M>N M1 M1+1+N=M.
- : update-preserves-not-member (not-member/< N>M) (update/= nat`eq/) _ (not-member/< N>M).
- : update-preserves-not-member (not-member/< N1>M) (update/< N3+1+N2=N1) (nat`ne/< N2>M)
(not-member/< N2>M).
- : update-preserves-not-member (not-member/< N1>M) (update/< N3+1+N2=N1) (nat`ne/> M>N2)
(not-member/> (not-member/< N3>M1) M1+1+N2=M)
<- gt-implies-plus M>N2 M1 M1+1+N2=M
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-swap-succ M1+1+N2=M M1+N2+1=M
<- plus-right-cancels-gt N3+N2+1=N1 M1+N2+1=M nat`eq/ N1>M N3>M1.
- : update-preserves-not-member (not-member/< N1>M) (update/> _ _) _ (not-member/< N1>M).
- : update-preserves-not-member (not-member/> F P) (update/= nat`eq/) _ (not-member/> F P).
- : update-preserves-not-member (not-member/> F M1+1+N1=M) (update/< N3+1+N2=N1) _
(not-member/> (not-member/> F M1+1+N3=MM) MM+1+N2=M)
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 M1+1+N1=M MM M1+1+N3=MM
MM+N2+1=M
<- plus-swap-succ-converse MM+N2+1=M MM+1+N2=M.
- : update-preserves-not-member (not-member/> F M1+1+N1=M) (update/> U N0+1+N1=N2) M<>N2
(not-member/> F' M1+1+N1=M)
<- plus-right-cancels-ne M1+1+N1=M N0+1+N1=N2 nat`eq/ M<>N2 M1+1<>N0+1
<- succ-preserves-ne-converse M1+1<>N0+1 M1<>N0
<- update-preserves-not-member F U M1<>N0 F'.
%worlds () (update-preserves-not-member N1-not-member-M1 M1^N2=D->M2 N1<>N2 N1-not-member-M2).
%total (F) (update-preserves-not-member F _ _ _).
%theorem update-preserves-not-member-converse :
forall* {M1} {N1} {N2} {D} {M2}
forall {F1:not-member M2 N1} {U:update M1 N2 D M2}
exists {F2:not-member M1 N1}
true.
%theorem update-preserves-not-member-converse-helper :
forall* {M1} {N1} {N2} {D} {M2} {B} {B2}
forall {F1:not-member M2 N1} {U:update M1 N2 D M2}
{D:member? M1 N1 B} {E:nat`eq? N1 N2 B2}
exists {F2:not-member M1 N1}
true.
- : update-preserves-not-member-converse-helper _ _ (member?/out F) _ F.
- : update-preserves-not-member-converse-helper F2 U (member?/in L1) (nat`eq?/no N) F1
<- update-preserves-lookup L1 U N L2
<- not-member-lookup-not-equal F2 L2 N<>N
<- nat`ne-anti-reflexive N<>N F
<- false-implies-not-member F F1.
- : update-preserves-not-member-converse-helper F2 U _ nat`eq?/yes F1
<- update-implies-lookup U L2
<- not-member-lookup-not-equal F2 L2 N<>N
<- nat`ne-anti-reflexive N<>N F
<- false-implies-not-member F F1.
%worlds () (update-preserves-not-member-converse-helper _ _ _ _ _).
%total { } (update-preserves-not-member-converse-helper _ _ _ _ _).
- : update-preserves-not-member-converse F2 U F1
<- member?-total D
<- nat`eq?-total E
<- update-preserves-not-member-converse-helper F2 U D E F1.
%worlds () (update-preserves-not-member-converse _ _ _).
%total { } (update-preserves-not-member-converse _ _ _).
%theorem update-is-cause-of-change :
forall* {M1} {N1} {N2} {M2} {D1} {D2}
forall {F:not-member M1 N1}
{U:update M1 N2 D2 M2}
{L:lookup M2 N1 D1}
exists {EN:nat`eq N1 N2} {ED:nat`eq D1 D2}
true.
%theorem update-is-cause-of-change/L :
forall* {M1} {N1} {N2} {M2} {D1} {D2} {B}
forall {F:not-member M1 N1}
{U:update M1 N2 D2 M2}
{L:lookup M2 N1 D1}
{E:nat`eq? N1 N2 B}
exists {EN:nat`eq N1 N2} {ED:nat`eq D1 D2}
true.
- : update-is-cause-of-change F U L EN ED
<- nat`eq?-total E?
<- update-is-cause-of-change/L F U L E? EN ED.
- : update-is-cause-of-change/L F U L (nat`eq?/yes) nat`eq/ ED
<- update-implies-lookup U L'
<- lookup-deterministic L L' eq/ nat`eq/ ED.
- : update-is-cause-of-change/L F U L (nat`eq?/no N1<>N2) EN ED
<- update-preserves-not-member F U N1<>N2 F'
<- not-member-lookup-not-equal F' L N1<>N1
<- nat`ne-anti-reflexive N1<>N1 V
<- nat`false-implies-eq V EN
<- nat`false-implies-eq V ED.
%worlds () (update-is-cause-of-change/L _ _ _ _ _ _).
%total { } (update-is-cause-of-change/L _ _ _ _ _ _).
%worlds () (update-is-cause-of-change _ _ _ _ _).
%total { } (update-is-cause-of-change _ _ _ _ _).
%theorem update-preserves-membership :
forall* {M1} {N1} {B} {N2} {D} {M2}
forall {MD1:member? M1 N1 B} {U:update M1 N2 D M2} {N:nat`ne N1 N2}
exists {MD2:member? M2 N1 B}
true.
- : update-preserves-membership (member?/in L) U NE (member?/in L')
<- update-preserves-lookup L U NE L'.
- : update-preserves-membership (member?/out F) U NE (member?/out F')
<- update-preserves-not-member F U NE F'.
%worlds () (update-preserves-membership _ _ _ _).
%total {} (update-preserves-membership _ _ _ _).
%theorem update-preserves-membership-converse :
forall* {M1} {N1} {B} {N2} {D} {M2}
forall {MD2:member? M2 N1 B} {U:update M1 N2 D M2} {N:nat`ne N1 N2}
exists {MD1:member? M1 N1 B}
true.
- : update-preserves-membership-converse (member?/in L2) U NE (member?/in L1)
<- update-preserves-lookup-converse L2 U NE L1.
- : update-preserves-membership-converse (member?/out F2) U NE (member?/out F1)
<- update-preserves-not-member-converse F2 U F1.
%worlds () (update-preserves-membership-converse _ _ _ _).
%total { } (update-preserves-membership-converse _ _ _ _).
%theorem lookup-update-preserves-membership :
forall* {M1} {N1} {B} {N2} {D1} {D2} {M2}
forall {MD1:member? M1 N1 B} {L:lookup M1 N2 D1} {U:update M1 N2 D2 M2}
exists {MD2:member? M2 N1 B}
true.
%theorem lookup-update-preserves-membership/L :
forall* {M1} {N1} {B} {N2} {D1} {D2} {M2} {B2}
forall {MD1:member? M1 N1 B} {L:lookup M1 N2 D1} {U:update M1 N2 D2 M2}
{EQ?:nat`eq? N1 N2 B2}
exists {MD2:member? M2 N1 B}
true.
- : lookup-update-preserves-membership/L MD1 _ Ux1 (nat`eq?/no N1<>N2) MD2
<- update-preserves-membership MD1 Ux1 N1<>N2 MD2.
- : lookup-update-preserves-membership/L
(member?/in _) _ U (nat`eq?/yes) (member?/in L2)
<- update-implies-lookup U L2.
- : lookup-update-preserves-membership/L
(member?/out F1) L1 _ nat`eq?/yes (member?/out F2)
<- not-member-lookup-not-equal F1 L1 NE
<- nat`ne-anti-reflexive NE F
<- false-implies-not-member F F2.
%worlds () (lookup-update-preserves-membership/L _ _ _ _ _).
%total { } (lookup-update-preserves-membership/L _ _ _ _ _).
- : lookup-update-preserves-membership MD1 L1 U MD2
<- nat`eq?-total EQ?
<- lookup-update-preserves-membership/L MD1 L1 U EQ? MD2.
%worlds () (lookup-update-preserves-membership _ _ _ _).
%total { } (lookup-update-preserves-membership _ _ _ _).
%theorem lookup-update-preserves-membership-converse :
forall* {M1} {N1} {B} {N2} {D1} {D2} {M2}
forall {MD1:member? M2 N1 B} {L:lookup M1 N2 D1} {U:update M1 N2 D2 M2}
exists {MD2:member? M1 N1 B}
true.
- : lookup-update-preserves-membership-converse MD2 ML MU MD1
<- member?-total MD1'
<- lookup-update-preserves-membership MD1' ML MU MD2'
<- member?-deterministic MD2' MD2 eq/ nat`eq/ B'=B
<- member?-respects-eq MD1' eq/ nat`eq/ B'=B MD1.
%worlds () (lookup-update-preserves-membership-converse _ _ _ _).
%total { } (lookup-update-preserves-membership-converse _ _ _ _).
%theorem update-preserves-in-member :
forall* {M1} {N1} {N2} {D} {M2}
forall {MD1:member? M1 N1 true} {U:update M1 N2 D M2}
exists {MD2:member? M2 N1 true}
true.
%theorem update-preserves-in-member/L :
forall* {M1} {N1} {N2} {D} {M2} {B}
forall {MD1:member? M1 N1 true} {U:update M1 N2 D M2}
{E: nat`eq? N1 N2 B}
exists {MD2:member? M2 N1 true}
true.
- : update-preserves-in-member/L
(member?/in ML1) U (nat`eq?/no N1<>N2) (member?/in ML2)
<- update-preserves-lookup ML1 U N1<>N2 ML2.
- : update-preserves-in-member/L _ U (nat`eq?/yes) (member?/in ML)
<- update-implies-lookup U ML.
%worlds () (update-preserves-in-member/L _ _ _ _).
%total { } (update-preserves-in-member/L _ _ _ _).
- : update-preserves-in-member MD1 U MD2
<- nat`eq?-total E
<- update-preserves-in-member/L MD1 U E MD2.
%worlds () (update-preserves-in-member _ _ _).
%total { } (update-preserves-in-member _ _ _).
%theorem update-overwrites :
forall* {M1} {N1} {D1} {M2} {N2} {D2} {M3}
forall {U1:update M1 N1 D1 M2} {U2:update M2 N2 D2 M3}
{E:nat`eq N1 N2}
exists {U12:update M1 N1 D2 M3}
true.
- : update-overwrites (update/0) (update/= nat`eq/) nat`eq/ (update/0).
- : update-overwrites (update/= nat`eq/) (update/= nat`eq/) nat`eq/ (update/= nat`eq/).
- : update-overwrites (update/< P) (update/= nat`eq/) nat`eq/ (update/< P).
- : update-overwrites (update/> U1 P) (update/> U2 P') nat`eq/ (update/> U3 P)
<- plus-right-cancels P P' nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0'
<- update-overwrites U1 U2 N0=N0' U3.
%% contradiction cases
- : update-overwrites (update/0) (update/< N3+1+N=N) nat`eq/ U
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/0) (update/> _ N0+1+N=N) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/= nat`eq/) (update/< N3+1+N=N) nat`eq/ U
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/= nat`eq/) (update/> _ N0+1+N=N) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/< _) (update/< N3+1+N=N) nat`eq/ U
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/< _) (update/> _ N0+1+N=N) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/> _ N0+1+N=N) (update/= nat`eq/) nat`eq/ U
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-update F U.
- : update-overwrites (update/> _ N0+1+N1=N2) (update/< N3+1+N2=N1) nat`eq/ U
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-update F U.
%worlds () (update-overwrites M1^N1=D1->M2 M2^N2=D2->M3 N1=N2
%{=>}% M1^N1=D2->M3).
%total (U) (update-overwrites U _ _ _).
%theorem update-overwrites-converse :
forall* {M1} {N1} {D1} {M2} {D2} {M3}
forall {U12:update M1 N1 D1 M3} {U1:update M1 N1 D2 M2}
exists {U2:update M2 N1 D1 M3}
true.
- : update-overwrites-converse U12 U1 U2
<- update-total U2P
<- update-overwrites U1 U2P nat`eq/ U12P
<- update-deterministic U12P U12 eq/ nat`eq/ nat`eq/ M2P=M2
<- update-respects-eq U2P eq/ nat`eq/ nat`eq/ M2P=M2 U2.
%worlds () (update-overwrites-converse _ _ _).
%total { } (update-overwrites-converse _ _ _).
%theorem update-may-have-no-effect :
forall* {M1} {N} {D} {M2}
forall {L:lookup M1 N D} {U:update M1 N D M2}
exists {E:eq M1 M2}
true.
- : update-may-have-no-effect (lookup/= nat`eq/) U E
<- update/=-inversion U nat`eq/ E.
- : update-may-have-no-effect (lookup/> L1 N0+1+N1=N2) U E
<- update/>-inversion U N0+1+N1=N2 _ U1 M112=M2
<- update-may-have-no-effect L1 U1 M1=M2
<- map/+-preserves-eq nat`eq/ nat`eq/ M1=M2 M111=M112
<- eq-transitive M111=M112 M112=M2 E.
%worlds () (update-may-have-no-effect _ _ _).
%total (L) (update-may-have-no-effect L _ _).
%theorem update-idempotent :
forall* {M1} {N1} {D1} {M2} {N2} {D2} {M3}
forall {U1:update M1 N1 D1 M2} {U2:update M2 N2 D2 M3}
{EN:nat`eq N1 N2} {ED:nat`eq D1 D2}
exists {EM:eq M2 M3}
true.
- : update-idempotent U1 U2 nat`eq/ nat`eq/ M2=M3
<- update-overwrites U1 U2 nat`eq/ M1^N=D->M3
<- update-deterministic U1 M1^N=D->M3 eq/ nat`eq/ nat`eq/ M2=M3.
%worlds () (update-idempotent M1^N1=D1->M2 M2^N2=D2->M3 N1=N2 D1=D2
%{=>}% M2=M3).
%total {} (update-idempotent _ _ _ _ _).
%theorem update-commutes :
forall* {M} {N1} {D1} {M1} {N2} {D2} {M12}
forall {U1:update M N1 D1 M1} {U12:update M1 N2 D2 M12}
{NE:nat`ne N1 N2}
exists {M2} {U2:update M N2 D2 M2} {U21:update M2 N1 D1 M12}
true.
- : update-commutes update/0 (update/= nat`eq/) N<>N map/0 U2 U21
<- nat`ne-anti-reflexive N<>N F
<- false-implies-update F U2
<- false-implies-update F U21.
- : update-commutes update/0 (update/< N'+1+N2=N1) _ _ update/0
(update/> update/0 N'+1+N2=N1).
- : update-commutes update/0 (update/> update/0 N'+1+N1=N2) _ _ update/0
(update/< N'+1+N1=N2).
- : update-commutes (update/= nat`eq/) (update/= nat`eq/) N<>N map/0 U2 U21
<- nat`ne-anti-reflexive N<>N F
<- false-implies-update F U2
<- false-implies-update F U21.
- : update-commutes (update/= nat`eq/) (update/< N'+1+N2=N1) _ _
(update/< N'+1+N2=N1) (update/> (update/= nat`eq/) N'+1+N2=N1).
- : update-commutes (update/= nat`eq/) (update/> U N'+1+N1=N2) _ _
(update/> U N'+1+N1=N2) (update/= nat`eq/).
- : update-commutes (update/< _) (update/= nat`eq/) N<>N map/0 U2 U21
<- nat`ne-anti-reflexive N<>N F
<- false-implies-update F U2
<- false-implies-update F U21.
- : update-commutes (update/< N1'+1+N1=N) (update/< N2'+1+N2=N1) _ _
(update/< N2''+1+N2=N)
(update/> (update/< N1'+1+N2'=N2'') N2'+1+N2=N1)
<- plus-swap-succ N2'+1+N2=N1 N2'+N2+1=N1
<- plus-associative-converse N2'+N2+1=N1 N1'+1+N1=N
N2'' N1'+1+N2'=N2'' N2''+N2+1=N
<- plus-swap-succ-converse N2''+N2+1=N N2''+1+N2=N.
- : update-commutes ((update/< N11+1+N1=N):update (map/+ N D M) _ _ _)
(update/> (update/= nat`eq/) N11+1+N1=N2) _
(map/+ N2 D2 M)
(update/= N=N2)
((update/< N11+1+N1=N2):update _ N1 D1 _)
<- plus-deterministic N11+1+N1=N N11+1+N1=N2 nat`eq/ nat`eq/ N=N2.
- : update-commutes (update/< N11+1+N1=N)
(update/> (update/< N2''+1+N2'=N11) N2'+1+N1=N2) _ _
(update/< N2''+1+N2=N) (update/< N2'+1+N1=N2)
<- plus-swap-succ N11+1+N1=N N11+N1+1=N
<- plus-swap-succ N2'+1+N1=N2 N2'+N1+1=N2
<- plus-associative* N2''+1+N2'=N11 N11+N1+1=N N2'+N1+1=N2
N2''+1+N2=N.
- : update-commutes (update/< N11+1+N1=N)
(update/> (update/> U N2''+1+N11=N2') N2'+1+N1=N2) _ _
(update/> U N2''+1+N=N2) (update/< N11+1+N1=N)
<- plus-swap-succ N11+1+N1=N N11+N1+1=N
<- plus-swap-succ N2'+1+N1=N2 N2'+N1+1=N2
<- plus-associative* N2''+1+N11=N2' N2'+N1+1=N2 N11+N1+1=N N2''+1+N=N2.
- : update-commutes (update/> U N11+1+N=N1) (update/= nat`eq/) _ _
(update/= nat`eq/) (update/> U N11+1+N=N1).
- : update-commutes (update/> U N11+1+N=N1) (update/< N2'+1+N2=N) _ _
(update/< N2'+1+N2=N)
(update/> (update/> U N11+1+N2'=N11') N11'+1+N2=N1)
<- plus-swap-succ N2'+1+N2=N N2'+N2+1=N
<- plus-associative-converse N2'+N2+1=N N11+1+N=N1
N11' N11+1+N2'=N11' N11'+N2+1=N1
<- plus-swap-succ-converse N11'+N2+1=N1 N11'+1+N2=N1.
- : update-commutes (update/> U1 N11+1+N=N1) (update/> U12 N2'+1+N=N2) N1<>N2
(map/+ N D M2)
(update/> U2 N2'+1+N=N2) (update/> U21 N11+1+N=N1)
<- plus-right-cancels-ne N11+1+N=N1 N2'+1+N=N2 nat`eq/ N1<>N2 N11+1<>N2'+1
<- succ-preserves-ne-converse N11+1<>N2'+1 N11<>N2'
<- update-commutes U1 U12 N11<>N2' M2 U2 U21.
%worlds () (update-commutes M^N1=D1->M1 M1^D2=N2->M12 N1<>N2
%{=>}% M2 M^N2=D2->M2 M2^N1=D1->M12).
%total (U1) (update-commutes U1 _ _ _ _ _).
%theorem update-commutes* :
forall* {M} {N1} {D1} {M1} {N2} {D2} {M12} {M2}
forall {U1:update M N1 D1 M1} {U12:update M1 N2 D2 M12}
{NE:nat`ne N1 N2} {U2:update M N2 D2 M2}
exists {U21:update M2 N1 D1 M12}
true.
- : update-commutes* M^N1=D1->M1 M1^D2=N2->M12 N1<>N2 M^N2=D2->M2 M2^N1=D1->M12
<- update-commutes M^N1=D1->M1 M1^D2=N2->M12 N1<>N2
M2' M^N2=D2->M2' M2'^N1=D1->M12
<- update-deterministic M^N2=D2->M2' M^N2=D2->M2 eq/ nat`eq/
nat`eq/ M2'=M2
<- update-respects-eq M2'^N1=D1->M12 M2'=M2 nat`eq/
nat`eq/ eq/ M2^N1=D1->M12.
%worlds () (update-commutes* M^N1=D1->M1 M1^D2=N2->M12 N1<>N2 M^N2=D2->M2
%{=>}% M2^N1=D1->M12).
%total {} (update-commutes* _ _ _ _ _).
%% The following theorem is needed if you want to iteratively
%% do something with a set. It says that you can take out an element
%% and (using the update-preserves-X-converse theorems) get a smaller set
%% that differs only for this element:
%theorem can-remove :
forall* {M} {S} {N} {D}
forall {SZ:size M S} {L:lookup M N D}
exists {M-} {S-} {SZ-:size M- S-} {E:nat`eq (s S-) S}
{U:update M- N D M} {F:not-member M- N}
true.
- : can-remove (size/+ _) (lookup/= _) _ _ size/0 nat`eq/ update/0 not-member/0.
- : can-remove (size/+ (size/+ SZ)) (lookup/= nat`eq/) _ _ (size/+ SZ) nat`eq/
(update/< N3+1+N2=N1) (not-member/< N1>N2)
<- plus-total N3+1+N2=N1
<- plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2.
- : can-remove (size/+ SZ) (lookup/> LK N0+1+N1=N2) _ _
(size/+ SZ2) E
(update/> U2 N0+1+N1=N2) (not-member/> F2 N0+1+N1=N2)
<- can-remove SZ LK M- S- SZ2 E2 U2 F2
<- succ-deterministic E2 E.
%worlds () (can-remove _ _ _ _ _ _ _ _).
%total (L) (can-remove _ L _ _ _ _ _ _).
%%%% Map comparison
%%% Definition of leq
leq : map -> map -> type.
leq/0 : leq map/0 M.
leq/= : leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`eq N1 N2
<- nat`leq D1 D2
<- leq M1 M2.
leq/> : leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)
<- nat`plus (s N3) N2 N1
<- leq (map/+ N3 D1 M1) M2.
%%% Theorems about leq
%theorem false-implies-leq :
forall* {M1} {M2}
forall {F:void}
exists {L:leq M1 M2}
true.
%worlds () (false-implies-leq _ _).
%total {} (false-implies-leq _ _).
%theorem leq-respects-eq :
forall* {M1} {M2} {M1'} {M2'}
forall {L:leq M1 M2} {E1:eq M1 M1'} {E2:eq M2 M2'}
exists {LP:leq M1' M2'}
true.
- : leq-respects-eq L eq/ eq/ L.
%worlds () (leq-respects-eq _ _ _ _).
%total {} (leq-respects-eq _ _ _ _).
%reduces L1 = L2 (leq-respects-eq L1 _ _ L2).
%theorem leq/0-inversion :
forall* {M1} {M2}
forall {L:leq M1 M2} {E2:eq M2 map/0}
exists {E1:eq M1 map/0}
true.
- : leq/0-inversion leq/0 eq/ eq/.
%worlds () (leq/0-inversion _ _ _).
%total { } (leq/0-inversion _ _ _).
%theorem leq/=-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2}
forall {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)} {EN:nat`eq N1 N2}
exists {ED:nat`leq D1 D2} {EM:leq M1 M2}
true.
- : leq/=-inversion (leq/= M1<=M2 D1<=D2 nat`eq/) nat`eq/ D1<=D2 M1<=M2.
- : leq/=-inversion (leq/> M311<=M2 N3+1+N=N) nat`eq/ ED M1<=M2
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- nat`false-implies-leq F ED
<- false-implies-eq F M311=M1
<- leq-respects-eq M311<=M2 M311=M1 eq/ M1<=M2.
%worlds () (leq/=-inversion _ _ _ _).
%total { } (leq/=-inversion _ _ _ _).
%reduces L1 < L (leq/=-inversion L _ _ L1).
%theorem leq/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3}
forall {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N3) N2 N1}
exists {EM:leq (map/+ N3 D1 M1) M2}
true.
- : leq/>-inversion (leq/= M1<=M2 D1<=D2 nat`eq/) N3+1+N=N M311<=M2
<- plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F M1=M311
<- leq-respects-eq M1<=M2 M1=M311 eq/ M311<=M2.
- : leq/>-inversion (leq/> M311'<=M2 N3P+1+N2=N1) N3+1+N2=N1 M311<=M2
<- plus-right-cancels N3P+1+N2=N1 N3+1+N2=N1 nat`eq/ nat`eq/ N3P+1=N3+1
<- succ-cancels N3P+1=N3+1 N3P=N3
<- map/+-preserves-eq N3P=N3 nat`eq/ eq/ M311'=M311
<- leq-respects-eq M311'<=M2 M311'=M311 eq/ M311<=M2.
%worlds () (leq/>-inversion _ _ _).
%total { } (leq/>-inversion _ _ _).
%reduces LP < L (leq/>-inversion L _ LP).
%theorem leq-contradiction :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0}
forall {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
{P:plus (s N0) N1 N2}
exists {F:void}
true.
- : leq-contradiction (leq/= _ _ nat`eq/) N0+1+N=N F
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F.
- : leq-contradiction (leq/> _ N3+1+N2=N1) N0+1+N1=N2 F
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F.
%worlds () (leq-contradiction _ _ _).
%total { } (leq-contradiction _ _ _).
%theorem leq-reflexive :
forall {M}
exists {L:leq M M}
true.
- : leq-reflexive map/0 leq/0.
- : leq-reflexive (map/+ N D M) (leq/= M<=M D<=D nat`eq/)
<- nat`leq-reflexive D D<=D
<- leq-reflexive M M<=M.
%worlds () (leq-reflexive _ _).
%total (M) (leq-reflexive M _).
%theorem leq-anti-symmetric :
forall* {M1} {M2}
forall {L1: leq M1 M2} {L2:leq M2 M1}
exists {E: eq M1 M2}
true.
- : leq-anti-symmetric leq/0 leq/0 eq/.
- : leq-anti-symmetric (leq/= M1<=M2 D1<=D2 nat`eq/)
(leq/= M2<=M1 D2<=D1 nat`eq/) E
<- nat`leq-anti-symmetric D1<=D2 D2<=D1 D1=D2
<- leq-anti-symmetric M1<=M2 M2<=M1 M1=M2
<- map/+-preserves-eq nat`eq/ D1=D2 M1=M2 E.
- : leq-anti-symmetric (leq/= _ _ nat`eq/) (leq/> _ N3+1+N=N) E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : leq-anti-symmetric (leq/> _ N3+1+N=N) (leq/= _ _ nat`eq/) E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : leq-anti-symmetric (leq/> _ N3+1+N2=N1) (leq/> _ N0+1+N1=N2) E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (leq-anti-symmetric _ _ _).
%total (L) (leq-anti-symmetric L _ _).
%theorem leq-transitive :
forall* {M1} {M2} {M3}
forall {L1:leq M1 M2} {L2:leq M2 M3}
exists {L3:leq M1 M3}
true.
- : leq-transitive leq/0 _ leq/0.
- : leq-transitive (leq/= M1<=M2 D1<=D2 nat`eq/) (leq/= M2<=M3 D2<=D3 nat`eq/)
(leq/= M1<=M3 D1<=D3 nat`eq/)
<- nat`leq-transitive D1<=D2 D2<=D3 D1<=D3
<- leq-transitive M1<=M2 M2<=M3 M1<=M3.
- : leq-transitive (leq/= M1<=M2 D1<=D2 nat`eq/) (leq/> M522<=M3 N5+1+N3=N2)
(leq/> M511<=M3 N5+1+N3=N2)
<- leq-transitive (leq/= M1<=M2 D1<=D2 nat`eq/) M522<=M3 M511<=M3.
- : leq-transitive (leq/> M011<=M2 N0+1+N=N1) (leq/= M2<=M3 D2<=D3 nat`eq/)
(leq/> M011<=M3 N0+1+N=N1)
<- leq-transitive M011<=M2 M2<=M3 M011<=M3.
- : leq-transitive (leq/> M011<=M2 N0+1+N2=N1) (leq/> M522<=M3 N5+1+N3=N2)
(leq/> M411<=M3 N4+1+N3=N1)
<- nat`plus-swap-succ N5+1+N3=N2 N5+N3+1=N2
<- nat`plus-associative-converse N5+N3+1=N2 N0+1+N2=N1 N4 N0+1+N5=N4
N4+N3+1=N1
<- nat`plus-swap-succ-converse N4+N3+1=N1 N4+1+N3=N1
<- leq-transitive (leq/> M011<=M2 N0+1+N5=N4) M522<=M3 M411<=M3.
%worlds () (leq-transitive _ _ _).
%total (L) (leq-transitive _ L _).
%theorem map/+-preserves-leq :
forall* {N1} {N2} {D1} {D2} {M1} {M2}
forall {E:nat`eq N1 N2} {LD:nat`leq D1 D2} {LM:leq M1 M2}
exists {L:leq (map/+ N1 D1 M1) (map/+ N2 D2 M2)}
true.
- : map/+-preserves-leq N1=N2 D1<=D2 M1<=M2 (leq/= M1<=M2 D1<=D2 N1=N2).
%worlds () (map/+-preserves-leq _ _ _ _).
%total { } (map/+-preserves-leq _ _ _ _).
%theorem lookup-respects-leq :
forall* {M} {N} {D} {MP}
forall {L:lookup M N D} {ME:leq M MP}
exists {DP} {L:lookup MP N DP} {DE:nat`leq D DP}
true.
- : lookup-respects-leq (lookup/= nat`eq/) (leq/= _ D1<=D2 nat`eq/)
_ (lookup/= nat`eq/) D1<=D2.
- : lookup-respects-leq (lookup/= nat`eq/) (leq/> M311<=M2 N3+1+N2=N1)
D2 (lookup/> L13 N3+1+N2=N1) D1<=D2
<- lookup-respects-leq (lookup/= nat`eq/) M311<=M2 D2 L13 D1<=D2.
- : lookup-respects-leq (lookup/> L13 N3+1+N2=N1) (leq/= M1<=M2 _ nat`eq/)
D2 (lookup/> L13' N3+1+N2=N1) D1<=D2
<- lookup-respects-leq L13 M1<=M2 D2 L13' D1<=D2.
- : lookup-respects-leq (lookup/> L10 N0+1+N1=N) (leq/> M311<=M2 N3+1+N2=N1)
D2 (lookup/> L14' N4+1+N2=N) D1<=D2
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- nat`plus-associative-converse N3+N2+1=N1 N0+1+N1=N
N4 N0+1+N3=N4 N4+N2+1=N
<- nat`plus-swap-succ-converse N4+N2+1=N N4+1+N2=N
<- lookup-respects-leq (lookup/> L10 N0+1+N3=N4) M311<=M2 D2 L14' D1<=D2.
%worlds () (lookup-respects-leq _ _ _ _ _).
%total (L) (lookup-respects-leq _ L _ _ _).
%theorem not-member-respects-geq :
forall* {M} {MP} {N}
forall {FP:not-member MP N} {L:leq M MP}
exists {F:not-member M N}
true.
- : not-member-respects-geq F leq/0 not-member/0.
- : not-member-respects-geq (not-member/< R) (leq/= _ _ nat`eq/) (not-member/< R).
- : not-member-respects-geq (not-member/< N2>N) (leq/> _ N3+1+N2=N1) (not-member/< N1>N)
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- gt-transitive N1>N2 N2>N N1>N.
- : not-member-respects-geq (not-member/> F20 N0+1+N2=N) (leq/= M1<=M2 _ nat`eq/)
(not-member/> F10 N0+1+N2=N)
<- not-member-respects-geq F20 M1<=M2 F10.
- : {F3110:not-member (map/+ N3 D1 M1) N0}
{N0+1+N2=N:plus (s N0) N2 N}
{N3+1+N2=N1:plus (s N3) N2 N1}
not-member-respects-geq
(not-member/> F20 N0+1+N2=N: not-member (map/+ N2 D2 M2) N)
(leq/> M311<=M2 N3+1+N2=N1) F'
<- not-member-respects-geq F20 M311<=M2 F3110
<- nat`plus-swap-succ N0+1+N2=N N0+N2+1=N
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-right-preserves-not-member* F3110 N3+N2+1=N1 N0+N2+1=N F'.
%worlds () (not-member-respects-geq _ _ _).
%total (F) (not-member-respects-geq F _ _).
%theorem leq-implies-size-le:
forall* {M1} {M2} {N1} {N2}
forall {L:leq M1 M2} {SZ1:size M1 N1} {SZ2:size M2 N2}
exists {G:ge N2 N1}
true.
- : leq-implies-size-le leq/0 size/0 N2=|M2| N2>=0
<- plus-commutative (plus/z:plus z N2 N2) N2+0=N2
<- plus-implies-ge N2+0=N2 N2>=0.
- : leq-implies-size-le (leq/= M1<=M2 _ _) (size/+ N1=|M1|) (size/+ N2=|M2|)
N2+1>=N1+1
<- leq-implies-size-le M1<=M2 N1=|M1| N2=|M2| N2>=N1
<- succ-preserves-ge N2>=N1 N2+1>=N1+1.
- : leq-implies-size-le (leq/> M311<=M2 _) (size/+ N1=|M1|) (size/+ N2=|M2|)
(ge/> N2+1>N1+1)
<- leq-implies-size-le M311<=M2 (size/+ N1=|M1|) N2=|M2| N2>=N1+1
<- succ-implies-gt nat`eq/ N2+1>N2
<- gt-transitive-ge N2+1>N2 N2>=N1+1 N2+1>N1+1.
%worlds () (leq-implies-size-le _ _ _ _).
%total (L) (leq-implies-size-le L _ _ _).
%theorem leq-implies-bound-le:
forall* {M1} {M2} {N1} {N2}
forall {L:leq M1 M2} {BD1:bound M1 N1} {BD2:bound M2 N2}
exists {G:ge N2 N1}
true.
- : leq-implies-bound-le leq/0 bound/0 _ N2>=0
<- plus-commutative plus/z N2+0=N2
<- plus-implies-ge N2+0=N2 N2>=0.
- : leq-implies-bound-le (leq/= M1<=M2 _ nat`eq/)
(bound/+ N+1+N1=N3 DM1=N3
<- leq-implies-bound-le M1<=M2 DM1=N1
<- plus-left-preserves-ge* N2>=N1 N+1+N2=N4 N+1+N1=N3 N4>=N3.
- : leq-implies-bound-le (leq/> M311<=M2 N3+1+N2=N1)
(bound/+ N1+1+N10=N11 DM1=N11
<- plus-total N3+1+N10=N13
<- leq-implies-bound-le M311<=M2 (bound/+ N3+1+N10=N13 DM1=N13
<- plus-swap-succ N1+1+N10=N11 N1+N10+1=N11
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-commutative N3+N2+1=N1 N2+1+N3=N1
<- plus-swap-succ N3+1+N10=N13 N3+N10+1=N13
<- plus-associative* N2+1+N3=N1 N1+N10+1=N11 N3+N10+1=N13 N2+1+N13=N11
<- plus-left-preserves-ge* N20>=N13 N2+1+N20=N22 N2+1+N13=N11 N22>=N11.
%worlds () (leq-implies-bound-le _ _ _ _).
%total (L) (leq-implies-bound-le L _ _ _).
%theorem shift-left-preserves-leq*:
forall* {M1} {M2} {N} {SM1} {D}
forall {L:leq M1 M2}
{S1:shift N M1 SM1}
exists {SL:leq SM1 (map/+ N D M2)}
true.
- : shift-left-preserves-leq* _ shift/0 leq/0.
- : shift-left-preserves-leq* M111<=M2 (shift/+ N+1+N1=N1')
(leq/> M111<=M2 N1+1+N=N1')
<- plus-swap-succ N+1+N1=N1' N+N1+1=N1'
<- plus-commutative N+N1+1=N1' N1+1+N=N1'.
%worlds () (shift-left-preserves-leq* _ _ _).
%total { } (shift-left-preserves-leq* _ _ _).
%theorem shift-preserves-leq*:
forall* {M1} {M2} {N} {SM1} {SM2}
forall {L:leq M1 M2}
{S1:shift N M1 SM1}
{S1:shift N M2 SM2}
exists {SL:leq SM1 SM2}
true.
- : shift-preserves-leq* _ shift/0 _ leq/0.
- : shift-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(shift/+ N+1+N1=N1')
(shift/+ N+1+N1=N2')
(leq/= M1<=M2 D1<=D2 N1'=N2')
<- plus-deterministic N+1+N1=N1' N+1+N1=N2' nat`eq/ nat`eq/ N1'=N2'.
- : shift-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(shift/+ N+1+N1=N1')
(shift/+ N+1+N2=N2')
(leq/> M311<=M2 N3+1+N2'=N1')
<- plus-commutative N3+1+N2=N1 N2+N3+1=N1
<- plus-associative-converse* N2+N3+1=N1 N+1+N1=N1' N+1+N2=N2' N2'+N3+1=N1'
<- plus-commutative N2'+N3+1=N1' N3+1+N2'=N1'.
%worlds () (shift-preserves-leq* _ _ _ _).
%total { } (shift-preserves-leq* _ _ _ _).
%theorem update-left-preserves-leq*:
forall* {M1} {M2} {N} {D} {M1'} {M2'}
forall {L:leq M1 M2}
{U1:update M1 N D M1'}
{U2:update M2 N D M2'}
exists {LP:leq M1' M2'}
true.
- : update-left-preserves-leq* leq/0 update/0 update/0 (leq/= leq/0 D<=D nat`eq/)
<- nat`leq-reflexive _ D<=D.
- : update-left-preserves-leq* leq/0 update/0 (update/= nat`eq/)
(leq/= leq/0 D<=D nat`eq/)
<- nat`leq-reflexive _ D<=D.
- : update-left-preserves-leq* leq/0 update/0 (update/< _)
(leq/= leq/0 D<=D nat`eq/)
<- nat`leq-reflexive _ D<=D.
- : update-left-preserves-leq* leq/0 update/0 (update/> U2505 N5+1+N2=N)
(leq/> M500<=M5 N5+1+N2=N)
<- update-left-preserves-leq* leq/0 update/0 U2505 M500<=M5.
- : update-left-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(update/= nat`eq/)
(U2:update (map/+ N D2 M2) N D M)
M001<=M
<- update/=-inversion U2 nat`eq/ M002=M
<- nat`leq-reflexive _ D<=D
<- leq-respects-eq (leq/= M1<=M2 D<=D nat`eq/) eq/ M002=M M001<=M.
- : update-left-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(update/< N3+1+N=N1)
(U2:update (map/+ N1 D2 M2) N D M)
M00M311<=M
<- update/<-inversion U2 N3+1+N=N1 M00M322=M
<- nat`leq-reflexive _ D<=D
<- leq-respects-eq (leq/= (leq/= M1<=M2 D1<=D2 nat`eq/) D<=D nat`eq/) eq/
M00M322=M M00M311<=M.
- : update-left-preserves-leq* (leq/= M1<=M2 D1<=D2 nat`eq/)
(update/> U1303 N3+1+N1=N)
(U2:update (map/+ N1 D2 M2) N D M)
M113<=M
<- update/>-inversion U2 N3+1+N1=N M4 U2304 M124=M
<- update-left-preserves-leq* M1<=M2 U1303 U2304 M3<=M4
<- leq-respects-eq (leq/= M3<=M4 D1<=D2 nat`eq/) eq/ M124=M M113<=M.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/= nat`eq/)
(U2:update (map/+ N2 D2 M2) N1 D M)
M101<=M
<- update/>-inversion U2 N3+1+N2=N1 M4 U2304 M224=M
<- update-left-preserves-leq* M311<=M2 (update/= nat`eq/) U2304 M301<=M4
<- leq-respects-eq (leq/> M301<=M4 N3+1+N2=N1) eq/ M224=M M101<=M.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N=N1)
(update/< N4+1+N=N1)
(update/= nat`eq/) %% hence N=N2
(leq/= M411<=M2 D<=D nat`eq/)
<- nat`plus-right-cancels N3+1+N=N1 N4+1+N=N1 nat`eq/ nat`eq/ N3+1=N4+1
<- nat`succ-cancels N3+1=N4+1 N3=N4
<- map/+-preserves-eq N3=N4 nat`eq/ eq/ M311=M411
<- leq-respects-eq M311<=M2 M311=M411 eq/ M411<=M2
<- nat`leq-reflexive _ D<=D.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/< N4+1+N=N1)
(update/< N5+1+N=N2)
(leq/= (leq/> M311<=M2 N3+1+N5=N4) D<=D nat`eq/)
<- nat`plus-swap-succ N5+1+N=N2 N5+N+1=N2
<- nat`plus-associative-converse N5+N+1=N2 N3+1+N2=N1
N4' N3+1+N5=N4' N4'+N+1=N1
<- nat`plus-swap-succ N4+1+N=N1 N4+N+1=N1
<- nat`plus-right-cancels N4'+N+1=N1 N4+N+1=N1 nat`eq/ nat`eq/ N4'=N4
<- nat`plus-respects-eq N3+1+N5=N4' nat`eq/ nat`eq/ N4'=N4 N3+1+N5=N4
<- nat`leq-reflexive _ D<=D.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/< N4+1+N=N1)
(update/> U2505 N5+1+N2=N)
(leq/> M50M411<=M5 N5+1+N2=N)
<- nat`plus-swap-succ N5+1+N2=N N5+N2+1=N
<- nat`plus-associative-converse N5+N2+1=N N4+1+N=N1
N3P N4+1+N5=N3P N3P+N2+1=N1
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- nat`plus-right-cancels N3P+N2+1=N1 N3+N2+1=N1 nat`eq/ nat`eq/ N3P=N3
<- nat`plus-respects-eq N4+1+N5=N3P nat`eq/ nat`eq/ N3P=N3 N4+1+N5=N3
<- update-left-preserves-leq* M311<=M2 (update/< N4+1+N5=N3) U2505
M50M411<=M5.
- : update-left-preserves-leq* (leq/> M311<=M2 N3+1+N2=N1)
(update/> U1404 N4+1+N1=N)
(U2:update (map/+ N2 D2 M2) N D M)
M114<=M
<- nat`plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- nat`plus-associative-converse N3+N2+1=N1 N4+1+N1=N
N5 N4+1+N3=N5 N5+N2+1=N
<- nat`plus-swap-succ-converse N5+N2+1=N N5+1+N2=N
<- update/>-inversion U2 N5+1+N2=N M5 U2505 M225=M
<- update-left-preserves-leq* M311<=M2 (update/> U1404 N4+1+N3=N5) U2505
M314<=M5
<- leq-respects-eq (leq/> M314<=M5 N3+1+N2=N1) eq/ M225=M M114<=M.
%worlds () (update-left-preserves-leq* _ _ _ _).
%total (U) (update-left-preserves-leq* _ _ U _).
%theorem update-right-preserves-leq*:
forall* {M} {N} {D1} {D2} {M1'} {M2'}
forall {L:nat`leq D1 D2}
{U1:update M N D1 M1'}
{U2:update M N D2 M2'}
exists {LP:leq M1' M2'}
true.
- : update-right-preserves-leq* D1<=D2 update/0 update/0
(leq/= leq/0 D1<=D2 nat`eq/).
- : update-right-preserves-leq* D1<=D2 (update/= nat`eq/) U2 L
<- update/=-inversion U2 nat`eq/ M221=M2'
<- leq-reflexive _ M1<=M1
<- leq-respects-eq (leq/= M1<=M1 D1<=D2 nat`eq/) eq/ M221=M2' L.
- : update-right-preserves-leq* D1<=D2 (update/< P) U2 L
<- update/<-inversion U2 P M22311=M2'
<- leq-reflexive _ M311<=M311
<- leq-respects-eq (leq/= M311<=M311 D1<=D2 nat`eq/) eq/ M22311=M2' L.
- : update-right-preserves-leq* D1<=D2 (update/> U1 P) U22 L
<- update/>-inversion U22 P M2' U2 M112=M
<- update-right-preserves-leq* D1<=D2 U1 U2 M1'<=M2'
<- nat`leq-reflexive _ D<=D
<- leq-respects-eq (leq/= M1'<=M2' D<=D nat`eq/) eq/ M112=M L.
%worlds () (update-right-preserves-leq* _ _ _ _).
%total (U) (update-right-preserves-leq* _ U _ _).
%theorem update-preserves-leq* :
forall* {M1} {M2} {N} {D1} {D2} {M1'} {M2'}
forall {L:leq M1 M2} {L:nat`leq D1 D2}
{U1:update M1 N D1 M1'}
{U2:update M2 N D2 M2'}
exists {LP:leq M1' M2'}
true.
- : update-preserves-leq* M1<=M2 D1<=D2 M1^N=D1->M1' M2^N=D2->M2' M1'<=M2'
<- update-total M2^N=D1->MM
<- update-left-preserves-leq* M1<=M2 M1^N=D1->M1' M2^N=D1->MM M1'<=MM
<- update-right-preserves-leq* D1<=D2 M2^N=D1->MM M2^N=D2->M2' MM<=M2'
<- leq-transitive M1'<=MM MM<=M2' M1'<=M2'.
%worlds () (update-preserves-leq* _ _ _ _ _).
%total { } (update-preserves-leq* _ _ _ _ _).
%theorem not-member-update-implies-leq :
forall* {M1} {N} {D} {M2}
forall {F:not-member M1 N} {U:update M1 N D M2}
exists {L:leq M1 M2}
true.
- : not-member-update-implies-leq not-member/0 U leq/0.
- : not-member-update-implies-leq (not-member/< N2 M311<=M311 N3+1+N2=N1) eq/ M22311=M2 L.
- : not-member-update-implies-leq (not-member/> F1 N0+1+N1=N2) U L
<- update/>-inversion U N0+1+N1=N2 _ U1 M112=M
<- not-member-update-implies-leq F1 U1 L1
<- nat`leq-reflexive _ DL
<- leq-respects-eq (leq/= L1 DL nat`eq/) eq/ M112=M L.
%worlds () (not-member-update-implies-leq _ _ _).
%total (F) (not-member-update-implies-leq F _ _).
%theorem lookup-update-preserves-leq :
forall* {M1} {N} {D1} {D2} {M2}
forall {L:lookup M1 N D1} {U:update M1 N D2 M2}
{L:nat`leq D1 D2}
exists {L:leq M1 M2}
true.
- : lookup-update-preserves-leq (lookup/= nat`eq/) U D1<=D2 L
<- update/=-inversion U nat`eq/ M221=M2
<- leq-reflexive _ M1<=M1
<- leq-respects-eq (leq/= M1<=M1 D1<=D2 nat`eq/) eq/ M221=M2 L.
- : lookup-update-preserves-leq (lookup/> L1 N0+1+N1=N2) U D1<=D2 L
<- update/>-inversion U N0+1+N1=N2 M2 U1 M112=M
<- lookup-update-preserves-leq L1 U1 D1<=D2 L1'
<- nat`leq-reflexive _ D1<=D1
<- leq-respects-eq (leq/= L1' D1<=D1 nat`eq/) eq/ M112=M L.
%worlds () (lookup-update-preserves-leq _ _ _ _).
%total (L) (lookup-update-preserves-leq L _ _ _).
%%%% Map addition
%%% Definition of union
union : map -> map -> map -> type.
union/L : union map/0 M M.
union/R : union M map/0 M.
union/= : union (map/+ N1 D1 M1) (map/+ N2 D2 M2) (map/+ N1 D3 M3)
<- nat`eq N1 N2
<- nat`union D1 D2 D3
<- union M1 M2 M3.
union/< : union (map/+ N1 D1 M1) (map/+ N2 D2 M2) (map/+ N1 D1 M3)
<- nat`plus (s N0) N1 N2
<- union M1 (map/+ N0 D2 M2) M3.
union/> : union (map/+ N1 D1 M1) (map/+ N2 D2 M2) (map/+ N2 D2 M3)
<- nat`plus (s N3) N2 N1
<- union (map/+ N3 D1 M1) M2 M3.
%%% Theorems about union
%theorem false-implies-union :
forall* {M1} {M2} {M3}
forall {F:void}
exists {D:union M1 M2 M3}
true.
%worlds () (false-implies-union _ _).
%total {} (false-implies-union _ _).
%theorem union-respects-eq :
forall* {M1} {M2} {M3} {M1P} {M2P} {M3P}
forall {A:union M1 M2 M3} {E1:eq M1 M1P} {E2:eq M2 M2P} {E3:eq M3 M3P}
exists {AP:union M1P M2P M3P}
true.
- : union-respects-eq A eq/ eq/ eq/ A.
%worlds () (union-respects-eq _ _ _ _ _).
%total {} (union-respects-eq _ _ _ _ _).
%reduces A = AP (union-respects-eq A _ _ _ AP).
%% Inversion lemmas for union
%theorem union/=-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {M}
forall {A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M}
{G:nat`eq N1 N2}
exists {D3} {M3}
{D:nat`union D1 D2 D3}
{AP:union M1 M2 M3}
{E:eq M (map/+ N1 D3 M3)}
true.
- : union/=-inversion (union/= MM DD nat`eq/) _ _ _ DD MM eq/.
- : union/=-inversion (union/< (JP:union _ (map/+ N0 D2 M2) M3) N0+1+N=N) nat`eq/
D2 M3 DJ MJ ME
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- nat`false-implies-union F DJ
<- false-implies-eq F (M022=M2:eq (map/+ N0 D2 M2) M2)
<- union-respects-eq JP eq/ M022=M2 eq/ MJ
<- false-implies-eq F ME.
- : union/=-inversion (union/> (JP:union (map/+ _ D1 M1) M2 M3) N3+1+N=N) nat`eq/
D1 M3 DJ MJ ME
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- nat`gt-anti-reflexive N>N F
<- nat`false-implies-union F DJ
<- false-implies-eq F (M311=M1:eq (map/+ N3 D1 M1) M1)
<- union-respects-eq JP M311=M1 eq/ eq/ MJ
<- false-implies-eq F ME.
%worlds () (union/=-inversion _ _ _ _ _ _ _).
%total {} (union/=-inversion _ _ _ _ _ _ _).
%reduces JP < J (union/=-inversion J _ _ _ _ JP _).
%theorem union/<-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {M} {N0}
forall {A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M}
{P:plus (s N0) N1 N2}
exists {M3}
{AP:union M1 (map/+ N0 D2 M2) M3}
{E:eq M (map/+ N1 D1 M3)}
true.
- : union/<-inversion (union/< J P) P' _ J' eq/
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0P
<- map/+-preserves-eq N0=N0P nat`eq/ eq/ M022=M022'
<- union-respects-eq J eq/ M022=M022' eq/ J'.
- : union/<-inversion (union/= J' _ nat`eq/) N0+1+N=N M3 J E
<- plus-implies-gt N0+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F M2=M022
<- union-respects-eq J' eq/ M2=M022 eq/ J
<- false-implies-eq F E.
- : union/<-inversion (union/> J' N3+1+N2=N1) N0+1+N1=N2 M3 J E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M311=M1
<- false-implies-eq F M2=M022
<- union-respects-eq J' M311=M1 M2=M022 eq/ J
<- false-implies-eq F E.
%worlds () (union/<-inversion _ _ _ _ _).
%total {} (union/<-inversion _ _ _ _ _).
%reduces JP < J (union/<-inversion J _ _ JP _).
%theorem union/>-inversion :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N3} {M}
forall {A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M}
{P:plus (s N3) N2 N1}
exists {M3}
{AP:union (map/+ N3 D1 M1) M2 M3}
{E:eq M (map/+ N2 D2 M3)}
true.
- : union/>-inversion (union/> J P) P' _ J' eq/
<- nat`plus-right-cancels P P' nat`eq/ nat`eq/ N3+1=N3'+1
<- succ-cancels N3+1=N3'+1 N3=N3P
<- map/+-preserves-eq N3=N3P nat`eq/ eq/ M311=M311'
<- union-respects-eq J M311=M311' eq/ eq/ J'.
- : union/>-inversion (union/= J' _ nat`eq/) N3+1+N=N M3 J E
<- nat`plus-implies-gt N3+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F M1=M311
<- union-respects-eq J' M1=M311 eq/ eq/ J
<- false-implies-eq F E.
- : union/>-inversion (union/< J' N0+1+N1=N2) N3+1+N2=N1 M3 J E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F M1=M311
<- false-implies-eq F M022=M2
<- union-respects-eq J' M1=M311 M022=M2 eq/ J
<- false-implies-eq F E.
%worlds () (union/>-inversion _ _ _ _ _).
%total {} (union/>-inversion _ _ _ _ _).
%reduces JP < J (union/>-inversion J _ _ JP _).
%theorem union-deterministic :
forall* {M1} {M2} {M3} {M1P} {M2P} {M3P}
forall {A:union M1 M2 M3} {AP:union M1P M2P M3P}
{E1:eq M1 M1P} {E2:eq M2 M2P}
exists {E3:eq M3 M3P}
true.
- : union-deterministic union/L union/L eq/ eq/ eq/.
- : union-deterministic union/L union/R eq/ eq/ eq/.
- : union-deterministic union/R union/L eq/ eq/ eq/.
- : union-deterministic union/R union/R eq/ eq/ eq/.
- : union-deterministic (union/= M1+M2=M3 D1+D2=D3 nat`eq/)
(union/= M1+M2=M3' D1+D2=D3P nat`eq/)
eq/ eq/ M=M'
<- nat`union-deterministic D1+D2=D3 D1+D2=D3P nat`eq/ nat`eq/ D3=D3'
<- union-deterministic M1+M2=M3 M1+M2=M3' eq/ eq/ M3=M3'
<- map/+-preserves-eq nat`eq/ D3=D3' M3=M3' M=M'.
- : union-deterministic (union/< M1+MT=M3 N0+1+N1=N2)
(union/< M1+MT'=M3' N0'+1+N1=N2)
eq/ eq/ M=M'
<- plus-right-cancels N0+1+N1=N2 N0'+1+N1=N2 nat`eq/ nat`eq/ N0+1=N0'+1
<- succ-cancels N0+1=N0'+1 N0=N0P
<- map/+-preserves-eq N0=N0P nat`eq/ eq/ MT=MT'
<- union-deterministic M1+MT=M3 M1+MT'=M3' eq/ MT=MT' M3=M3'
<- map/+-preserves-eq nat`eq/ nat`eq/ M3=M3' M=M'.
- : union-deterministic (union/> MT+M2=M3 N3+1+N2=N1)
(union/> MT'+M2=M3' N3'+1+N2=N1) eq/ eq/ E
<- plus-right-cancels N3+1+N2=N1 N3'+1+N2=N1 nat`eq/ nat`eq/ N3+1=N3'+1
<- succ-cancels N3+1=N3'+1 N3=N3P
<- map/+-preserves-eq N3=N3P nat`eq/ eq/ MT=MT'
<- union-deterministic MT+M2=M3 MT'+M2=M3' MT=MT' eq/ M3=M3'
<- map/+-preserves-eq nat`eq/ nat`eq/ M3=M3' E.
%% contradiction cases:
- : union-deterministic (union/= _ _ nat`eq/) (union/< _ N'+1+N=N) eq/ eq/ E
<- plus-implies-gt N'+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/= _ _ nat`eq/) (union/> _ N'+1+N=N) eq/ eq/ E
<- plus-implies-gt N'+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/< _ NP+1+N=N) (union/= _ _ nat`eq/) eq/ eq/ E
<- plus-implies-gt NP+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/< _ N0+1+N1=N2) (union/> _ N3+1+N2=N1) eq/ eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
- : union-deterministic (union/> _ NP+1+N=N) (union/= _ _ nat`eq/) eq/ eq/ E
<- plus-implies-gt NP+1+N=N nat`eq/ N>N
<- gt-anti-reflexive N>N F
<- false-implies-eq F E.
- : union-deterministic (union/> _ N3+1+N2=N1) (union/< _ N0+1+N1=N2) eq/ eq/ E
<- nat`plus-implies-gt N3+1+N2=N1 nat`eq/ N1>N2
<- nat`plus-implies-gt N0+1+N1=N2 nat`eq/ N2>N1
<- nat`gt-anti-symmetric N1>N2 N2>N1 F
<- false-implies-eq F E.
%worlds () (union-deterministic _ _ _ _ _).
%total (A) (union-deterministic A _ _ _ _).
%theorem union-total* :
forall {M1} {M2}
exists {M3} {A:union M1 M2 M3}
true.
%% we need some lemmas
%% We need them to ensure termination because
%% union substitutes new maps on recursive calls which
%% makes it hard to prove the arguments get smaller.
%theorem union-map/+-M-total* :
forall {N1} {D1} {M1} {M2}
exists {M3} {A:union (map/+ N1 D1 M1) M2 M3}
true.
%theorem union-M-map/+-total* :
forall {M1} {N2} {D2} {M2}
exists {M3} {A:union M1 (map/+ N2 D2 M2) M3}
true.
%theorem union-map/+-map/+-total* :
forall {N1} {D1} {M1} {N2} {D2} {M2} {C} {CMP:nat`compare N1 N2 C}
exists {M3}
{A:union (map/+ N1 D1 M1) (map/+ N2 D2 M2) M3}
true.
- : union-total* map/0 M M union/L.
- : union-total* M map/0 M union/R.
- : union-total* (map/+ N1 D1 M1) (map/+ N2 D2 M2) M3 A
<- nat`compare-total* N1 N2 C CMP
<- union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 C CMP M3 A.
- : union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 equal CMP (map/+ N1 D3 M3)
(union/= M1+M2=M3 D1+D2=D3 N1=N2)
<- equal-implies-eq CMP N1=N2
<- nat`union-total* D1 D2 D3 D1+D2=D3
<- union-total* M1 M2 M3 M1+M2=M3.
- : union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 less CMP (map/+ N1 D1 M3)
(union/< M1+T=M3 N0+1+N1=N2)
<- less-implies-lt CMP N2>N1
<- gt-implies-plus N2>N1 _ N0+1+N1=N2
<- union-M-map/+-total* M1 N0 D2 M2 M3 M1+T=M3.
- : union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 greater CMP (map/+ N2 D2 M3)
(union/> T+M2=M3 N3+1+N2=N1)
<- greater-implies-gt CMP N1>N2
<- gt-implies-plus N1>N2 _ N3+1+N2=N1
<- union-map/+-M-total* N3 D1 M1 M2 M3 T+M2=M3.
- : union-M-map/+-total* map/0 N2 D2 M2 (map/+ N2 D2 M2) union/L.
- : union-M-map/+-total* (map/+ N1 D1 M1) N2 D2 M2 M3 A
<- nat`compare-total* N1 N2 C CMP
<- union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 C CMP M3 A.
- : union-map/+-M-total* N1 D1 M1 map/0 (map/+ N1 D1 M1) union/R.
- : union-map/+-M-total* N1 D1 M1 (map/+ N2 D2 M2) M3 A
<- nat`compare-total* N1 N2 C CMP
<- union-map/+-map/+-total* N1 D1 M1 N2 D2 M2 C CMP M3 A.
%worlds () (union-total* _ _ _ _)
(union-M-map/+-total* _ _ _ _ _ _)
(union-map/+-M-total* _ _ _ _ _ _)
(union-map/+-map/+-total* _ _ _ _ _ _ _ _ _ _).
%total [ (M1a M1b M1c M1d) (M2a M2b M2c M2d) ]
(union-total* M1d M2d _ _)
(union-M-map/+-total* M1c _ _ M2c _ _)
(union-map/+-M-total* _ _ M1b M2b _ _)
(union-map/+-map/+-total* _ _ M1a _ _ M2a _ _ _ _).
%abbrev union-total = union-total* _ _ _.
%theorem disjoint-union-total :
forall* {M1} {M2}
forall {D:disjoint M1 M2}
exists {M3} {A:union M1 M2 M3}
true.
- : disjoint-union-total disjoint/L _ union/L.
- : disjoint-union-total disjoint/R _ union/R.
- : disjoint-union-total (disjoint/< D P) _ (union/< J P)
<- disjoint-union-total D _ J.
- : disjoint-union-total (disjoint/> D P) _ (union/> J P)
<- disjoint-union-total D _ J.
%worlds () (disjoint-union-total _ _ _).
%total (D) (disjoint-union-total D _ _).
%theorem union-empty-implies-empty :
forall* {M1} {M2}
forall {A:union M1 M2 map/0}
exists {E1:eq M1 map/0} {E2:eq M2 map/0}
true.
- : union-empty-implies-empty union/L eq/ eq/.
- : union-empty-implies-empty union/R eq/ eq/.
%worlds () (union-empty-implies-empty _ _ _).
%total { } (union-empty-implies-empty _ _ _).
%theorem union-preserves-disjoint* :
forall* {M1} {M2} {M3} {M4}
forall {D1:disjoint M1 M4} {D2:disjoint M2 M4}
{A:union M1 M2 M3}
exists {D3:disjoint M3 M4}
true.
% a lemma that counts the size of maps to help prove termination
%theorem union-preserves-disjoint*/L :
forall* {M1} {M2} {M3} {M4}
forall {S1} {S2} {SZ1:size M1 S1} {SZ2:size M2 S2}
{D1:disjoint M1 M4} {D2:disjoint M2 M4}
{A:union M1 M2 M3}
exists {D3:disjoint M3 M4}
true.
- : union-preserves-disjoint* D1 D2 J D3
<- size-total SZ1
<- size-total SZ2
<- union-preserves-disjoint*/L _ _ SZ1 SZ2 D1 D2 J D3.
- : union-preserves-disjoint*/L _ _ _ _ disjoint/R _ _ disjoint/R.
- : union-preserves-disjoint*/L _ _ _ _ _ disjoint/R _ disjoint/R.
- : union-preserves-disjoint*/L _ _ _ _ _ D union/L D.
- : union-preserves-disjoint*/L _ _ _ _ D _ union/R D.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/< D1 N5+1+N1=N4) D2X
(union/= J _ nat`eq/)
(disjoint/< D3 N5+1+N1=N4)
<- disjoint/<-inversion D2X N5+1+N1=N4 D2
<- union-preserves-disjoint*/L S1 S2 SZ1 SZ2 D1 D2 J D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/< D1 N5+1+N1=N4) D2X
(union/> J N3+1+N2=N1)
(disjoint/< D3 N6+1+N2=N4)
<- plus-swap-succ N3+1+N2=N1 N3+N2+1=N1
<- plus-associative-converse N3+N2+1=N1 N5+1+N1=N4 N6 N5+1+N3=N6 N6+N2+1=N4
<- plus-swap-succ-converse N6+N2+1=N4 N6+1+N2=N4
<- disjoint/<-inversion D2X N6+1+N2=N4 D2
<- plus-swap-succ N5+1+N3=N6 N5+N3+1=N6
<- plus-commutative N5+N3+1=N6 N3+1+N5=N6
<- shift-right-preserves-disjoint D1 (shift/+ N3+1+N5=N6) D1< D1 N5+1+N4=N1) D2X
(union/= J DJ nat`eq/)
(disjoint/> D3 N5+1+N4=N1)
<- disjoint/>-inversion D2X N5+1+N4=N1 D2
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) (size/+ SZ2)
D1 D2 (union/= J DJ nat`eq/) D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/> D1 N5+1+N4=N1) D2X
(union/< J N0+1+N1=N2)
(disjoint/> D3 N5+1+N4=N1)
<- plus-swap-succ N5+1+N4=N1 N5+N4+1=N1
<- plus-associative-converse N5+N4+1=N1 N0+1+N1=N2 N6 N0+1+N5=N6 N6+N4+1=N2
<- plus-swap-succ-converse N6+N4+1=N2 N6+1+N4=N2
<- disjoint/>-inversion D2X N6+1+N4=N2 D2
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) (size/+ SZ2)
D1 D2 (union/< J N0+1+N5=N6) D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
D1X (disjoint/< D2 N6+1+N2=N4)
(union/< J N0+1+N1=N2)
(disjoint/< D3 N5+1+N1=N4)
<- plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- plus-associative-converse N0+N1+1=N2 N6+1+N2=N4 N5 N6+1+N0=N5 N5+N1+1=N4
<- plus-swap-succ-converse N5+N1+1=N4 N5+1+N1=N4
<- disjoint/<-inversion D1X N5+1+N1=N4 D1
<- plus-swap-succ N6+1+N0=N5 N6+N0+1=N5
<- plus-commutative N6+N0+1=N5 N0+1+N6=N5
<- shift-right-preserves-disjoint D2 (shift/+ N0+1+N6=N5) D2< D2 N6+1+N4=N2)
(union/> J N3+1+N2=N1)
(disjoint/> D3 N6+1+N4=N2)
<- plus-swap-succ N6+1+N4=N2 N6+N4+1=N2
<- plus-associative-converse N6+N4+1=N2 N3+1+N2=N1 N5 N3+1+N6=N5 N5+N4+1=N1
<- plus-swap-succ-converse N5+N4+1=N1 N5+1+N4=N1
<- disjoint/>-inversion D1X N5+1+N4=N1 D1
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) (size/+ SZ2)
D1 D2 (union/> J N3+1+N6=N5) D3.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/< D1 N5+1+N1=N4)
(disjoint/> D2 N6+1+N4=N2) JX D3X
<- plus-swap-succ N5+1+N1=N4 N5+N1+1=N4
<- plus-associative-converse N5+N1+1=N4 N6+1+N4=N2 N0 N6+1+N5=N0 N0+N1+1=N2
<- plus-swap-succ-converse N0+N1+1=N2 N0+1+N1=N2
<- union/<-inversion JX N0+1+N1=N2 _ J M=M113
<- eq-symmetric M=M113 M113=M
<- union-preserves-disjoint*/L S1 (s S2) SZ1 (size/+ SZ2)
D1 (disjoint/> D2 N6+1+N5=N0) J D3
<- disjoint-respects-eq (disjoint/< D3 N5+1+N1=N4) M113=M eq/ D3X.
- : union-preserves-disjoint*/L (s S1) (s S2) (size/+ SZ1) (size/+ SZ2)
(disjoint/> D1 N5+1+N4=N1)
(disjoint/< D2 N6+1+N2=N4) JX D3X
<- plus-swap-succ N6+1+N2=N4 N6+N2+1=N4
<- plus-associative-converse N6+N2+1=N4 N5+1+N4=N1 N3 N5+1+N6=N3 N3+N2+1=N1
<- plus-swap-succ-converse N3+N2+1=N1 N3+1+N2=N1
<- union/>-inversion JX N3+1+N2=N1 _ J M=M223
<- eq-symmetric M=M223 M223=M
<- union-preserves-disjoint*/L _ _ (size/+ SZ1) SZ2
(disjoint/> D1 N5+1+N6=N3) D2 J D3
<- disjoint-respects-eq (disjoint/< D3 N6+1+N2=N4) M223=M eq/ D3X.
%worlds () (union-preserves-disjoint*/L _ _ _ _ _ _ _ _).
%total {S1 S2 D1} (union-preserves-disjoint*/L S1 S2 _ _ D1 _ _ _).
%worlds () (union-preserves-disjoint* _ _ _ _).
%total { } (union-preserves-disjoint* _ _ _ _).
%theorem shift-left-preserves-union :
forall* {N} {D} {M1} {M2} {M3} {SM1}
forall {A:union M1 M2 M3} {S1:shift N M1 SM1}
exists {SA:union SM1 (map/+ N D M2) (map/+ N D M3)}
true.
- : shift-left-preserves-union union/L shift/0 union/L.
- : shift-left-preserves-union union/R shift/0 union/L.
- : shift-left-preserves-union M111+M2=M3 (shift/+ N+1+N1=N1')
(union/> M111+M2=M3 N1+1+N=N1')
<- plus-swap-succ N+1+N1=N1' N+N1+1=N1'
<- plus-commutative N+N1+1=N1' N1+1+N=N1'.
%worlds () (shift-left-preserves-union _ _ _).
%total { } (shift-left-preserves-union _ _ _).
%theorem shift-left-preserves-union-converse :
forall* {N} {D} {M1} {M2} {SM1} {SM3}
forall {SA:union SM1 (map/+ N D M2) SM3} {S1:shift N M1 SM1}
exists {M3} {A:union M1 M2 M3} {E:eq (map/+ N D M3) SM3}
true.
- : shift-left-preserves-union-converse union/L shift/0 _ union/L eq/.
- : shift-left-preserves-union-converse M111+M222=SM3 (shift/+ N2+1+N3=N1) M3
M311+M2=M3 M223=SM3
<- plus-swap-succ N2+1+N3=N1 N2+N3+1=N1
<- plus-commutative N2+N3+1=N1 N3+1+N2=N1
<- union/>-inversion M111+M222=SM3 N3+1+N2=N1 M3 M311+M2=M3 SM3=M223
<- eq-symmetric SM3=M223 M223=SM3.
%worlds () (shift-left-preserves-union-converse _ _ _ _ _).
%total { } (shift-left-preserves-union-converse _ _ _ _ _).
%theorem shift-right-preserves-union :
forall* {N} {D} {M1} {M2} {M3} {SM2}
forall {A:union M1 M2 M3} {S2:shift N M2 SM2}
exists {SA:union (map/+ N D M1) SM2 (map/+ N D M3)}
true.
- : shift-right-preserves-union union/L shift/0 union/R.
- : shift-right-preserves-union union/R shift/0 union/R.
- : shift-right-preserves-union M1+M222=M3 (shift/+ N+1+N2=N2')
(union/< M1+M222=M3 N2+1+N=N2')
<- plus-swap-succ N+1+N2=N2' N+N2+1=N2'
<- plus-commutative N+N2+1=N2' N2+1+N=N2'.
%worlds () (shift-right-preserves-union _ _ _).
%total { } (shift-right-preserves-union _ _ _).
%theorem shift-right-preserves-union-converse :
forall* {N} {D} {M1} {M2} {SM2} {SM3}
forall {SA:union (map/+ N D M1) SM2 SM3} {S2:shift N M2 SM2}
exists {M3} {A:union M1 M2 M3} {E:eq (map/+ N D M3) SM3}
true.
- : shift-right-preserves-union-converse union/R shift/0 _ union/R eq/.
- : shift-right-preserves-union-converse M111+M322=SM3 (shift/+ N1+1+N2=N3)
M3 M1+M222=M3 M133=SM3
<- plus-swap-succ N1+1+N2=N3 N1+N2+1=N3
<- plus-commutative N1+N2+1=N3 N2+1+N1=N3
<- union/<-inversion M111+M322=SM3 N2+1+N1=N3 M3 M1+M222=M3 SM3=M133
<- eq-symmetric SM3=M133 M133=SM3.
%worlds () (shift-right-preserves-union-converse _ _ _ _ _).
%total { } (shift-right-preserves-union-converse _ _ _ _ _).
%theorem shift-preserves-union :
forall* {N} {M1} {M2} {M3} {SM1} {SM2} {SM3}
forall {A:union M1 M2 M3}
{S1:shift N M1 SM1} {S2:shift N M2 SM2} {S3:shift N M3 SM3}
exists {SA:union SM1 SM2 SM3}
true.
- : shift-preserves-union union/L shift/0 M2< M311+M2=M3 N3+1+N2=N1)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5)
(shift/+ N+1+N2=N6) M411+M522=M623
<- plus-deterministic N+1+N2=N5 N+1+N2=N6 nat`eq/ nat`eq/ N5=N6
<- plus-swap-succ N+1+N2=N5 N+N2+1=N5
<- plus-commutative N+N2+1=N5 N2+1+N=N5
<- plus-commutative N3+1+N2=N1 N2+N3+1=N1
<- plus-associative-converse* N2+N3+1=N1 N+1+N1=N4 N+1+N2=N5 N5+N3+1=N4
<- plus-commutative N5+N3+1=N4 N3+1+N5=N4
<- map/+-preserves-eq N5=N6 nat`eq/ eq/ M523=M623
<- union-respects-eq (union/> M311+M2=M3 N3+1+N5=N4) eq/ eq/ M523=M623
M411+M522=M623.
%worlds () (shift-preserves-union _ _ _ _ _).
%total { } (shift-preserves-union _ _ _ _ _).
%theorem shift-preserves-union-converse :
forall* {N} {M1} {M2} {SM1} {SM2} {SM3}
forall {SA:union SM1 SM2 SM3}
{S1:shift N M1 SM1} {S2:shift N M2 SM2}
exists {M3} {A:union M1 M2 M3} {S3:shift N M3 SM3}
true.
- : shift-preserves-union-converse union/L shift/0 M2< M611+M2=M3 N6+1+N5=N4)
(shift/+ N+1+N1=N4) (shift/+ N+1+N2=N5) _
(union/> M611+M2=M3 N6+1+N2=N1)
(shift/+ N+1+N2=N5)
<- plus-commutative N+1+N2=N5 N2+N+1=N5
<- plus-swap-succ-converse N2+N+1=N5 N2+1+N=N5
<- plus-associative-converse N2+N+1=N5 N6+1+N5=N4 N1' N6+1+N2=N1' N1'+N+1=N4
<- plus-commutative N+1+N1=N4 N1+N+1=N4
<- plus-right-cancels N1'+N+1=N4 N1+N+1=N4 nat`eq/ nat`eq/ N1'=N1
<- plus-respects-eq N6+1+N2=N1' nat`eq/ nat`eq/ N1'=N1 N6+1+N2=N1.
%worlds () (shift-preserves-union-converse _ _ _ _ _ _).
%total { } (shift-preserves-union-converse _ _ _ _ _ _).
%theorem union-commutative :
forall* {M1} {M2} {M3}
forall {A:union M1 M2 M3}
exists {AP:union M2 M1 M3}
true.
- : union-commutative union/L union/R.
- : union-commutative union/R union/L.
- : union-commutative (union/= M1+M2=M3 D1+D2=D3 nat`eq/)
(union/= M2+M1=M3 D2+D1=D3 nat`eq/)
<- nat`union-commutative D1+D2=D3 D2+D1=D3
<- union-commutative M1+M2=M3 M2+M1=M3.
- : union-commutative (union/< M1+MT=M3 N0+1+N1=N2) (union/> MT+M1=M3 N0+1+N1=N2)
<- union-commutative M1+MT=M3 MT+M1=M3.
- : union-commutative (union/> MT+M2=M3 N3+1+N2=N1) (union/< M2+MT=M3 N3+1+N2=N1)
<- union-commutative MT+M2=M3 M2+MT=M3.
%worlds () (union-commutative _ _).
%total (A) (union-commutative A _).
%theorem union-associative :
forall* {M1} {M2} {M3} {M4} {M7}
forall {A12:union M1 M2 M3} {A34:union M3 M4 M7}
exists {M6} {A24:union M2 M4 M6} {A16:union M1 M6 M7}
true.
%% a lemma
%theorem union-associative-union/<-union/< :
forall* {N1} {D1} {M1} {N2} {D2} {M2} {N0} {N5} {N4} {D4} {M4} {M6} {M7}
forall {PLUS012:nat`plus (s N0) N1 N2}
{PLUS514:nat`plus (s N5) N1 N4}
{JOIN246:union (map/+ N0 D2 M2) (map/+ N5 D4 M4) M6}
{JOIN167:union M1 M6 M7}
exists {M} {JOIN24: union (map/+ N2 D2 M2) (map/+ N4 D4 M4) M}
{JOIN:union (map/+ N1 D1 M1) M (map/+ N1 D1 M7)}
true.
- : union-associative union/L A _ A union/L.
- : union-associative A union/R _ union/R A.
- : union-associative union/R A _ union/L A.
- : union-associative (union/= M1+M2=M3 D1+D2=D3 nat`eq/)
(union/= M3+M4=M7 D3+D4=D7 nat`eq/) (map/+ _ D6 M6)
(union/= M2+M4=M6 D2+D4=D6 nat`eq/)
(union/= M1+M6=M7 D1+D6=D7 nat`eq/)
<- nat`union-associative D1+D2=D3 D3+D4=D7 D6 D2+D4=D6 D1+D6=D7
<- union-associative M1+M2=M3 M3+M4=M7 M6 M2+M4=M6 M1+M6=M7.
- : union-associative (union/= M1+M2=M3 D1+D2=D3 nat`eq/)
(union/< M3+M044=M7 N0+1+N3=N4) (map/+ _ _ M6)
(union/< M2+M044=M6 N0+1+N3=N4)
(union/= M1+M6=M7 D1+D2=D3 nat`eq/)
<- union-associative M1+M2=M3 M3+M044=M7 M6 M2+M044=M6 M1+M6=M7.
- : union-associative (union/= M1+M2=M3 D1+D2=D3 nat`eq/)
(union/> M533+M4=M7 N5+1+N4=N3) (map/+ _ _ M6)
(union/> M522+M4=M6 N5+1+N4=N3)
(union/> M511+M6=M7 N5+1+N4=N3)
<- union-associative (union/= M1+M2=M3 D1+D2=D3 nat`eq/) M533+M4=M7
M6 M522+M4=M6 M511+M6=M7.
- : union-associative (union/< M1+M022=M3 N0+1+N1=N2)
(union/= M3+M4=M7 D1+D4=D7 nat`eq/) (map/+ _ _ M6)
(union/> M022+M3=M6 N0+1+N1=N2)
(union/= M1+M6=M7 D1+D4=D7 nat`eq/)
<- union-associative M1+M022=M3 M3+M4=M7 M6 M022+M3=M6 M1+M6=M7.
%% the hardest of all 11 cases!
- : {M111+M=M117: union (map/+ N1 D1 M1) M (map/+ N1 D1 M7)}
{M3+M544=M7: union M3 (map/+ N5 D4 M4) M7}
{M1+M022=M3: union M1 (map/+ N0 D2 M2) M3}
{M1+M6=M7: union M1 M6 M7}
union-associative (union/< M1+M022=M3 N0+1+N1=N2)
(union/< M3+M544=M7 N5+1+N1=N4)
M M222+M444=M M111+M=M117
<- union-associative M1+M022=M3 M3+M544=M7 M6 M022+M544=M6 M1+M6=M7
<- union-associative-union/<-union/<
N0+1+N1=N2 N5+1+N1=N4 M022+M544=M6 M1+M6=M7
M M222+M444=M M111+M=M117.
- : union-associative-union/<-union/< N+1+N1=N2 N+1+N1=N4
(union/= M2+M4=M6 D2+D4=D6 nat`eq/)
M1+M066=M7 (map/+ N2 D6 M6)
(union/= M2+M4=M6 D2+D4=D6 N2=N4)
(union/< M1+M066=M7 N+1+N1=N2)
<- nat`plus-deterministic N+1+N1=N2 N+1+N1=N4 nat`eq/ nat`eq/ N2=N4.
- : union-associative-union/<-union/< N0+1+N1=N2 N5+1+N1=N4
(union/< M2+M744=M6 N7+1+N0=N5)
M1+M026=M7 (map/+ N2 D2 M6)
(union/< M2+M744=M6 N7+1+N2=N4)
(union/< M1+M026=M7 N0+1+N1=N2)
<- nat`plus-swap-succ N5+1+N1=N4 N5+N1+1=N4
<- nat`plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- nat`plus-associative* N7+1+N0=N5 N5+N1+1=N4 N0+N1+1=N2 N7+1+N2=N4.
- : union-associative-union/<-union/< N0+1+N1=N2 N5+1+N1=N4
(union/> M722+M4=M6 N7+1+N5=N0)
M1+M546=M7 (map/+ N4 D4 M6)
(union/> M722+M4=M6 N7+1+N4=N2)
(union/< M1+M546=M7 N5+1+N1=N4)
<- nat`plus-swap-succ N0+1+N1=N2 N0+N1+1=N2
<- nat`plus-swap-succ N5+1+N1=N4 N5+N1+1=N4
<- nat`plus-associative* N7+1+N5=N0 N0+N1+1=N2 N5+N1+1=N4 N7+1+N4=N2.
%% and now we return to the main theorem
- : union-associative (union/< M1+M022=M3 N0+1+N1=N2)
(union/> M513+M4=M7 N5+1+N3=N1) (map/+ _ _ M6)
(union/> M622+M4=M6 N6+1+N3=N2)
(union/> M511+M6=M7 N5+1+N3=N1)
<- nat`plus-swap-succ N5+1+N3=N1 N5+N3+1=N1
<- nat`plus-associative-converse N5+N3+1=N1 N0+1+N1=N2 N6
N0+1+N5=N6 N6+N3+1=N2
<- nat`plus-swap-succ-converse N6+N3+1=N2 N6+1+N3=N2
<- union-associative (union/< M1+M022=M3 N0+1+N5=N6) M513+M4=M7
M6 M622+M4=M6 M511+M6=M7.
- : union-associative (union/> M311+M2=M3 N3+1+N2=N1)
(union/= M3+M4=M7 D2+D4=D7 nat`eq/) (map/+ _ _ M6)
(union/= M2+M4=M6 D2+D4=D7 nat`eq/)
(union/> M311+M6=M7 N3+1+N2=N1)
<- union-associative M311+M2=M3 M3+M4=M7 M6 M2+M4=M6 M311+M6=M7.
- : union-associative (union/> M311+M2=M3 N3+1+N2=N1)
(union/< M3+M044=M7 N0+1+N2=N4) (map/+ _ _ M6)
(union/< M2+M044=M6 N0+1+N2=N4)
(union/> M311+M6=M7 N3+1+N2=N1)
<- union-associative M311+M2=M3 M3+M044=M7 M6 M2+M044=M6 M311+M6=M7.
- : union-associative (union/> M311+M2=M3 N3+1+N2=N1)
(union/> M523+M4=M7 N5+1+N4=N2) (map/+ _ _ M6)
(union/> M522+M4=M6 N5+1+N4=N2)
(union/> M711+M6=M7 N7+1+N4=N1)
<- nat`plus-swap-succ N5+1+N4=N2 N5+N4+1=N2
<- nat`plus-associative-converse N5+N4+1=N2 N3+1+N2=N1
N7 N3+1+N5=N7 N7+N4+1=N1
<- nat`plus-swap-succ-converse N7+N4+1=N1 N7+1+N4=N1
<- union-associative (union/> M311+M2=M3 N3+1+N5=N7) M523+M4=M7
M6 M522+M4=M6 M711+M6=M7.
%worlds () (union-associative-union/<-union/< _ _ _ _ _ _ _).
%total {} (union-associative-union/<-union/< _ _ _ _ _ _ _).
%worlds () (union-associative _ _ _ _ _).
%total (J) (un