Gates: 16 declarations
On this page · Permalink · Source line 406
L001 write_same
On this page · Permalink · Source line 408
Source. CircuitObstructions/Gates.lean:17
Block. 01 Axioms. propext
CircuitObstructions.write_same {W : Type} [DecidableEq W] (s : CircuitObstructions.State W) (t : W) (b : Bool) :
CircuitObstructions.write s t b t = bL002 write_other
On this page · Permalink · Source line 418
Source. CircuitObstructions/Gates.lean:20
Block. 01 Axioms. propext
CircuitObstructions.write_other {W : Type} [DecidableEq W] (s : CircuitObstructions.State W) (t i : W) (b : Bool)
(h : i ≠ t) : CircuitObstructions.write s t b i = s iL003 xor_cancel_right
On this page · Permalink · Source line 428
Source. CircuitObstructions/Gates.lean:23
Block. 01 Axioms. none
CircuitObstructions.xor_cancel_right (a b : Bool) : (a ^^ b ^^ b) = aL004 xor_cancel_left
On this page · Permalink · Source line 437
Source. CircuitObstructions/Gates.lean:26
Block. 01 Axioms. none
CircuitObstructions.xor_cancel_left (a b : Bool) : (a ^^ (a ^^ b)) = bL005 xor_commute
On this page · Permalink · Source line 446
Source. CircuitObstructions/Gates.lean:29
Block. 01 Axioms. none
CircuitObstructions.xor_commute (a b : Bool) : (a ^^ b) = (b ^^ a)L006 xor_true_iff_ne
On this page · Permalink · Source line 455
Source. CircuitObstructions/Gates.lean:32
Block. 01 Axioms. none
CircuitObstructions.xor_true_iff_ne (a b : Bool) : (a ^^ b) = true ↔ a ≠ bL007 eval_involutive
On this page · Permalink · Source line 464
Source. CircuitObstructions/Gates.lean:48
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.Gate.eval_involutive {W : Type} [DecidableEq W] (g : CircuitObstructions.Gate W)
(s : CircuitObstructions.State W) : g.eval (g.eval s) = sL008 eval_injective
On this page · Permalink · Source line 474
Source. CircuitObstructions/Gates.lean:67
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.Gate.eval_injective {W : Type} [DecidableEq W] (g : CircuitObstructions.Gate W)
{s t : CircuitObstructions.State W} (h : g.eval s = g.eval t) : s = tL009 run_nil
On this page · Permalink · Source line 484
Source. CircuitObstructions/Gates.lean:78
Block. 01 Axioms. none
CircuitObstructions.run_nil {W : Type} [DecidableEq W] (s : CircuitObstructions.State W) :
CircuitObstructions.run [] s = sL010 run_cons
On this page · Permalink · Source line 494
Source. CircuitObstructions/Gates.lean:81
Block. 01 Axioms. none
CircuitObstructions.run_cons {W : Type} [DecidableEq W] (g : CircuitObstructions.Gate W)
(gs : CircuitObstructions.Circuit W) (s : CircuitObstructions.State W) :
CircuitObstructions.run (g :: gs) s = CircuitObstructions.run gs (g.eval s)L011 run_append
On this page · Permalink · Source line 505
Source. CircuitObstructions/Gates.lean:84
Block. 01 Axioms. none
CircuitObstructions.run_append {W : Type} [DecidableEq W] (p q : CircuitObstructions.Circuit W)
(s : CircuitObstructions.State W) :
CircuitObstructions.run (p ++ q) s = CircuitObstructions.run q (CircuitObstructions.run p s)L012 run_reverse_run
On this page · Permalink · Source line 516
Source. CircuitObstructions/Gates.lean:90
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.run_reverse_run {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
(s : CircuitObstructions.State W) : CircuitObstructions.run (List.reverse c) (CircuitObstructions.run c s) = sL013 run_run_reverse
On this page · Permalink · Source line 526
Source. CircuitObstructions/Gates.lean:98
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.run_run_reverse {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
(s : CircuitObstructions.State W) : CircuitObstructions.run c (CircuitObstructions.run (List.reverse c) s) = sL014 run_injective
On this page · Permalink · Source line 536
Source. CircuitObstructions/Gates.lean:102
Block. 01 Axioms. propext, Quot.sound
CircuitObstructions.run_injective {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
{s t : CircuitObstructions.State W} (h : CircuitObstructions.run c s = CircuitObstructions.run c t) : s = tL015 toffoliCount_append
On this page · Permalink · Source line 546
Source. CircuitObstructions/Gates.lean:114
Block. 01 Axioms. propext
CircuitObstructions.toffoliCount_append {W : Type} (p q : CircuitObstructions.Circuit W) :
CircuitObstructions.toffoliCount (p ++ q) = CircuitObstructions.toffoliCount p + CircuitObstructions.toffoliCount qL016 toffoliCount_reverse
On this page · Permalink · Source line 556
Source. CircuitObstructions/Gates.lean:118
Block. 01 Axioms. propext
CircuitObstructions.toffoliCount_reverse {W : Type} (c : CircuitObstructions.Circuit W) :
CircuitObstructions.toffoliCount (List.reverse c) = CircuitObstructions.toffoliCount c