From Coq Require Import Bool.Bool Lists.List ZArith Lia. From Coq Require Import Ring. Import ListNotations. Open Scope Z_scope. Definition bool_and (a b : bool) := andb a b. Definition bool_or (a b : bool) := orb a b. Record DoctrineUnit := { value : Z; coherent : bool; lawful : bool }. Definition affirmedG6 (u : DoctrineUnit) : DoctrineUnit := {| value := value u; coherent := true; lawful := true |}. Definition necessary {World : Type} (access : World -> World -> Prop) (claim : World -> Prop) (w : World) : Prop := forall v : World, access w v -> claim v. Record LogicalGround := { lgIdentity : forall (A : Type) (a : A), a = a; lgNoncontradiction : forall p : Prop, p -> (p -> False) -> False; lgImplication : forall p q : Prop, p -> (p -> q) -> q; lgExcludedMiddle : forall b : bool, b = true \/ b = false }. Definition constructiveLogos : LogicalGround := {| lgIdentity := fun _ a => eq_refl a; lgNoncontradiction := fun _ hp hn => hn hp; lgImplication := fun _ _ hp h => h hp; lgExcludedMiddle := fun b => if b as x return x = true \/ x = false then or_introl eq_refl else or_intror eq_refl |}. Fixpoint iterations {A : Type} (step : A -> option A) (fuel : nat) (s : A) : nat := match fuel with | O => O | S n => match step s with | None => O | Some t => S (iterations step n t) end end. Definition signedIntegerPower (n : Z) : Z := if Z.even n then 1 else -1. Definition dominantValue (a b : Z) : Z := if Z.ltb (Z.abs a) (Z.abs b) then b else a. Inductive MCBExpr : Type := | mcbBalance : Z -> MCBExpr | mcbBase : Z -> MCBExpr | mcbNest : Z -> MCBExpr -> MCBExpr | mcbPower : MCBExpr -> MCBExpr. Definition MCBProgram := MCBExpr. Definition MCBData := MCBExpr. Inductive MCBKey : Type := | keyBalance : Z -> MCBKey | keyBase : Z -> MCBKey | keyNest : Z -> MCBKey -> MCBKey | keyPower : MCBKey -> MCBKey. Fixpoint quoteMCB (e : MCBExpr) : MCBKey := match e with | mcbBalance n => keyBalance n | mcbBase n => keyBase n | mcbNest n child => keyNest n (quoteMCB child) | mcbPower child => keyPower (quoteMCB child) end. Fixpoint unquoteMCB (d : MCBKey) : MCBExpr := match d with | keyBalance n => mcbBalance n | keyBase n => mcbBase n | keyNest n child => mcbNest n (unquoteMCB child) | keyPower child => mcbPower (unquoteMCB child) end. Definition phaseMCB (n : Z) : Z := if Z.eqb (Z.modulo n 2) 0 then 1 else -1. Fixpoint evalMCB (e : MCBExpr) : Z := match e with | mcbBalance n => n | mcbBase n => phaseMCB n | mcbNest n child => phaseMCB n + evalMCB child | mcbPower child => phaseMCB (evalMCB child) end. Definition evalMCBData (d : MCBKey) : Z := evalMCB (unquoteMCB d). Fixpoint reweightMCB (f : Z -> Z) (e : MCBExpr) : MCBExpr := match e with | mcbBalance n => mcbBalance (f n) | mcbBase n => mcbBase (f n) | mcbNest n child => mcbNest (f n) (reweightMCB f child) | mcbPower child => mcbPower (reweightMCB f child) end. Fixpoint reweightMCBData (f : Z -> Z) (d : MCBKey) : MCBKey := match d with | keyBalance n => keyBalance (f n) | keyBase n => keyBase (f n) | keyNest n child => keyNest (f n) (reweightMCBData f child) | keyPower child => keyPower (reweightMCBData f child) end. Fixpoint mcbContributions (e : MCBExpr) : list Z := match e with | mcbBalance n => [n] | mcbBase n => [phaseMCB n] | mcbNest n child => phaseMCB n :: mcbContributions child | mcbPower child => [phaseMCB (evalMCB child)] end. Fixpoint sumMCBData (xs : list Z) : Z := match xs with | [] => 0 | n :: rest => n + sumMCBData rest end. Definition normalizeMCB (e : MCBExpr) : MCBExpr := mcbBalance (evalMCB e). Definition mcbInitProgram : MCBExpr := mcbNest (-1) (mcbNest 0 (mcbNest 1 (mcbNest 2 (mcbNest 3 (mcbNest 4 (mcbNest 5 (mcbBase 6))))))). Definition mcbInitialization : MCBExpr := mcbPower mcbInitProgram. Definition compiledMCBInitBalance : Z := 0. Inductive Role := roleGround | roleRuntime. Definition signed (b : bool) : Z := if b then 1 else -1. Definition nativeNand (p q : bool) : Z := Z.pow (-1) (Z.of_nat (Z.to_nat (((1 + signed p) * (1 + signed q)) / 4))). Fixpoint sourceConjunction (xs : list bool) : bool := match xs with | [] => true | x :: rest => andb x (sourceConjunction rest) end. Lemma fold_preserves_source : forall (xs : list bool) (acc : bool), fold_left andb xs acc = andb acc (sourceConjunction xs). Proof. intro xs; induction xs as [|x xs IH]; intros acc; simpl. - destruct acc; reflexivity. - rewrite IH. destruct acc, x; reflexivity. Qed. Definition encode (role : Role) (value : Z) : option bool := match role with | roleGround => if Z.eqb value (-1) then Some true else None | roleRuntime => if Z.eqb value 1 then Some true else if Z.eqb value (-1) then Some false else None end. Definition cycleSigned (b : bool) : Z := if b then 1 else -1. Record ValidCycleUnit := { cycleValue : Z; cycleState : bool; cycleDepth : nat; cycleCoherent : bool; cycleLawful : bool; cycleLogosCoherence : cycleCoherent = true; cycleLogosLawful : cycleLawful = true }. Definition sevenChecks (u : ValidCycleUnit) : Prop := cycleValue u = cycleValue u /\ ~ (cycleSigned (cycleState u) = 1 /\ cycleSigned (cycleState u) = -1) /\ (cycleSigned (cycleState u) = 1 \/ cycleSigned (cycleState u) = -1) /\ (cycleCoherent u = true /\ cycleLawful u = true) /\ cycleSigned (cycleState u) = cycleSigned (cycleState u) /\ (cycleSigned (cycleState u) = 1 \/ cycleSigned (cycleState u) = -1) /\ (0 <= cycleDepth u)%nat. Lemma cycle_bivalence : forall b, cycleSigned b = 1 \/ cycleSigned b = -1. Proof. intro b; destruct b; [left|right]; reflexivity. Qed. Lemma cycle_noncontradiction : forall b, ~ (cycleSigned b = 1 /\ cycleSigned b = -1). Proof. intro b; destruct b; simpl; intros [H1 H2]; discriminate. Qed. Definition signatureSigned (b : bool) : Z := if b then 1 else -1. Fixpoint signatureValue (bs : list bool) : Z := match bs with [] => 1 | b :: rest => signatureSigned b * signatureValue rest end. Record LogicalSignature := { signatureSequence : list bool; signatureDepth : nat; signatureValueField : Z }. Definition generatedSignature (values : list Z) (parity : Z -> bool) : LogicalSignature := let sequence := map parity values in {| signatureSequence := sequence; signatureDepth := length sequence; signatureValueField := signatureValue sequence |}. Definition signatureInvariants (s : LogicalSignature) : Prop := signatureDepth s = length (signatureSequence s) /\ signatureValueField s = signatureValue (signatureSequence s) /\ forall b, In b (signatureSequence s) -> (signatureSigned b = 1 \/ signatureSigned b = -1). Fixpoint evenNat (n : nat) : bool := match n with O => true | S n => negb (evenNat n) end. Lemma even_add : forall a b, evenNat (a + b)%nat = Bool.eqb (evenNat a) (evenNat b). Proof. intros a b; induction b as [|b IH]. - rewrite Nat.add_0_r; simpl; destruct (evenNat a); reflexivity. - rewrite Nat.add_succ_r; simpl; rewrite IH; destruct (evenNat a), (evenNat b); reflexivity. Qed. Definition natAbs (a : Z) : nat := Z.to_nat (Z.abs a). Definition exponentXorState (a b : Z) : Z := if evenNat (natAbs a + natAbs b)%nat then 1 else -1. Definition statement_node0 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2)) (orb (negb v2) v0))) (andb (andb v0 v1) v2)) = true. Definition statement_node1 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (Bool.eqb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node2 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) v1)) (andb v0 v1)) = true. Definition statement_node3 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node4 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node5 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node6 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node7 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node8 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (orb (negb (orb (negb v0) v1)) (orb (negb v2) v3))) = true. Definition statement_node9 : Prop := forall (v0 : bool), (orb (negb (andb v0 (orb (negb v0) v0))) v0) = true. Definition statement_node10 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node11 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb (andb (andb v0 v1) v2)) v3))) v3) = true. Definition statement_node12 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (orb (negb v0) v1))) (andb v0 v1)) = true. Definition statement_node13 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb v0) (Bool.eqb v2 v1))) = true. Definition statement_node14 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node15 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node16 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node17 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (Bool.eqb v2 (andb v0 v1)))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node18 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (andb v0 v1)) (andb v0 v2)) (andb v0 v3)) v4)) (Bool.eqb (orb (negb v4) (andb (andb v0 v1) v2)) v3)) = true. Definition statement_node19 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node20 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node21 : Prop := forall (v0 : bool), (orb (negb v0) v0) = true. Definition statement_node22 : Prop := forall (v0 : bool), (orb (negb v0) v0) = true. Definition statement_node23 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) v1) (orb (negb v1) v0))) (andb v0 v1)) = true. Definition statement_node24 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb (andb v1 (Bool.eqb v1 v0)) v0) (orb (negb v0) v1))) (andb v1 v0)) = true. Definition statement_node25 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) v1)) (andb (Bool.eqb (negb v0) (negb v1)) (Bool.eqb v0 v1))) = true. Definition statement_node26 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v0))) (orb (negb v2) (andb v0 v1))) = true. Definition statement_node27 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node28 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v0) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node29 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node30 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb (andb v0 v1)) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node31 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (orb (negb v0) v1))) (orb (negb (orb (negb v0) v0)) (orb (negb v1) v1))) = true. Definition statement_node32 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v0))) (andb v0 v1)) = true. Definition statement_node33 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v0) v2))) (orb (negb v0) (Bool.eqb (orb (negb v1) v2) (orb (negb v2) v1)))) = true. Definition statement_node34 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node35 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node36 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb v0) (Bool.eqb v2 v1))) = true. Definition statement_node37 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node38 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node39 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node40 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node41 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (Bool.eqb v2 (andb v0 v1)))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node42 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node43 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node44 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (Bool.eqb v4 v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node45 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node46 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node47 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (orb (negb (andb v0 v1)) (orb (negb v2) v3))) = true. Definition statement_node48 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node49 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (orb (negb (andb v0 v1)) v2))) (orb (negb v2) (andb v0 v1))) = true. Definition statement_node50 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (orb (negb v0) v1))) (orb (negb (Bool.eqb v0 (orb (negb v0) (negb (orb (negb v0) (negb v0)))))) (Bool.eqb v1 v0))) = true. Definition statement_node51 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node52 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (orb (negb v0) v1))) (orb (negb (Bool.eqb v0 (orb (negb v0) (negb (orb (negb v0) (negb v0)))))) (Bool.eqb v1 v0))) = true. Definition statement_node53 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node54 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) v2) (orb (negb v2) v1))) (orb (negb (andb v0 v2)) v1)) = true. Definition statement_node55 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (Bool.eqb v1 v2)) (orb (negb v2) v0)) (orb (negb v0) v3)) (orb (negb v3) v4))) (andb (andb (andb (andb v0 v1) v2) v3) v4)) = true. Definition statement_node56 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node57 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) v2) = true. Definition statement_node58 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node59 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (orb (negb v0) v1) (orb (negb v0) v2))) (orb (negb v0) (Bool.eqb (orb (negb v1) v2) (orb (negb v2) v1)))) = true. Definition statement_node60 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (orb (negb (andb v0 v1)) (andb v2 v3))) = true. Definition statement_node61 : Prop := forall (v0 : bool), (orb (negb (Bool.eqb v0 v0)) (andb (andb (orb v0 (negb v0)) (Bool.eqb v0 (negb (negb v0)))) (andb (orb (negb v0) v0) (orb (negb (negb v0)) (negb v0))))) = true. Definition statement_node62 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node63 : Prop := forall (v0 : bool), (orb (negb (Bool.eqb v0 v0)) (orb v0 (negb v0))) = true. Definition statement_node64 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node65 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node66 : Prop := forall (v0 : bool), (orb (negb (andb v0 (andb v0 (negb (negb v0))))) (orb (negb v0) (Bool.eqb v0 (negb (andb v0 (negb v0)))))) = true. Definition statement_node67 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (orb (negb v1) v2)) v0)) = true. Definition statement_node68 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (orb (negb v0) v1) (orb (negb (andb v0 v1)) v2))) (orb (negb v0) (orb (negb v0) (Bool.eqb v1 v2)))) = true. Definition statement_node69 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) v2) (orb (negb v2) v1))) (Bool.eqb (negb v1) (negb (andb v0 v2)))) = true. Definition statement_node70 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (orb (negb (andb v0 v1)) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node71 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) (orb (negb v4) v5)) (Bool.eqb v0 v4)) (orb (negb v0) v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node72 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node73 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (Bool.eqb (Bool.eqb v3 v2) (Bool.eqb v1 v0))) = true. Definition statement_node74 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) (orb (negb v0) v1)) (orb (negb v0) (negb v2)))) (orb (negb (andb (andb v0 v1) (negb (andb v0 (negb v1))))) (negb v2))) = true. Definition statement_node75 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node76 : Prop := forall (A : Type) (condition : bool) (t e : A), (if condition then t else e) = t \/ (if condition then t else e) = e. Definition statement_node77 : Prop := forall (A : Type) (condition : bool) (t e : A), (if condition then t else e) = t \/ (if condition then t else e) = e. Definition statement_node78 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (orb (negb (Bool.eqb (andb (andb v0 v1) v2) v3)) v4)) = true. Definition statement_node79 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v1 (orb (negb v1) v2)) (orb (negb v2) v0))) (andb (andb v1 v2) v0)) = true. Definition statement_node80 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (negb v1) (orb (negb (negb v1)) (negb v2))) (orb (negb (negb v2)) (negb v0)))) (andb (andb (negb v1) (negb v2)) (negb v0))) = true. Definition statement_node81 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (andb (andb v0 v1) v2)) = true. Definition statement_node82 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5)) (orb (negb v5) v0))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node83 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5) v6)) (andb (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5) v6)) = true. Definition statement_node84 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node85 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node86 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node87 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb (andb v0 v1) v2) v3) v4)) = true. Definition statement_node88 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node89 : Prop := forall (World : Type) (access : World -> World -> Prop) (w : World) (unfixed : list Prop), necessary access (fun _ => exists _ : LogicalGround, True) w. Definition statement_node90 : Prop := forall (World : Type) (access : World -> World -> Prop) (w : World) (unfixed : list Prop), necessary access (fun _ => exists _ : LogicalGround, True) w. Definition statement_node91 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node92 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (orb (negb v0) (andb (andb v1 v2) v3))) = true. Definition statement_node93 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (Bool.eqb v2 (andb v0 v1)))) (andb (andb v0 v1) v2)) = true. Definition statement_node94 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node95 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node96 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) v3) v4)) (Bool.eqb (orb (negb (andb v0 v1)) (andb v2 v3)) v4)) = true. Definition statement_node97 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (Bool.eqb (Bool.eqb v0 v1) (Bool.eqb v1 v0))) = true. Definition statement_node98 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node99 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v1) (orb (negb v2) (Bool.eqb v0 v1)))) = true. Definition statement_node100 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (Bool.eqb v2 v3))) (orb (negb (andb v0 v1)) (andb v2 v3))) = true. Definition statement_node101 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) (Bool.eqb v0 v1)) (Bool.eqb v1 v0)) v1) v0)) (Bool.eqb (andb v0 v1) (andb v1 v0))) = true. Definition statement_node102 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (orb (negb v0) v1))) (andb v0 v1)) = true. Definition statement_node103 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node104 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node105 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (orb (negb (andb v0 v1)) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node106 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (orb (negb v0) v0)) (andb (orb (negb v0) v0) (andb (orb (negb v1) v1) (orb (negb v2) v2)))) = true. Definition statement_node107 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v2)) v1)) = true. Definition statement_node108 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool) (v7 : bool) (v8 : bool) (v9 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5) v6) v7) v8) v9)) (andb (andb (andb (andb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5) v6) v7) v8) v9)) = true. Definition statement_node109 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node110 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node111 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 v1) v2) (andb (orb (negb v0) v1) v2))) (Bool.eqb (andb v1 v2) v0)) = true. Definition statement_node112 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node113 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (Bool.eqb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node114 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node115 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node116 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (orb (negb v2) (Bool.eqb v1 v0))) = true. Definition statement_node117 : Prop := forall u : DoctrineUnit, (affirmedG6 u).(coherent) = true /\ (affirmedG6 u).(lawful) = true. Definition statement_node118 : Prop := forall u : DoctrineUnit, (affirmedG6 u).(coherent) = true /\ (affirmedG6 u).(lawful) = true. Definition statement_node119 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) v3)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node120 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node121 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node122 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (Bool.eqb (Bool.eqb (andb v0 v1) (andb v2 v3)) (andb v4 v5))) = true. Definition statement_node123 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node124 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (Bool.eqb v2 (andb v0 v1)))) (andb (orb (negb v2) v0) (orb (negb v0) v1))) = true. Definition statement_node125 : Prop := forall (v0 : bool), (orb (negb (andb v0 (Bool.eqb v0 v0))) (Bool.eqb v0 (orb (negb v0) (negb (orb (negb v0) (negb v0)))))) = true. Definition statement_node126 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v2 (orb (negb v2) v1)) (orb (negb (andb v2 v1)) v3)) (orb (negb v3) v0))) v0) = true. Definition statement_node127 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (Bool.eqb v0 v1))) (andb v0 v1)) = true. Definition statement_node128 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node129 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node130 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node131 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 v1) v2) (orb (negb v2) (negb (andb v0 v1))))) (orb (negb v0) (andb v1 v2))) = true. Definition statement_node132 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) v2) (orb (negb v2) v1)) v1)) (andb (andb v0 v1) v2)) = true. Definition statement_node133 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node134 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) v4) = true. Definition statement_node135 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node136 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node137 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node138 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (Bool.eqb (Bool.eqb v3 v2) (Bool.eqb v1 v0))) = true. Definition statement_node139 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) v3) (Bool.eqb v0 v4)) (orb (negb v4) v3))) (orb (negb v4) (andb (andb v0 v1) (andb v2 v3)))) = true. Definition statement_node140 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) v2) (orb (negb v2) (andb v0 v1)))) v1) = true. Definition statement_node141 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node142 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node143 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (Bool.eqb v1 v0)) v2)) = true. Definition statement_node144 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node145 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node146 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (Bool.eqb v1 v0) (negb v0)) (orb (negb (negb v0)) v2)) (Bool.eqb v2 v3))) (andb (andb (negb v0) (negb v1)) (andb v2 v3))) = true. Definition statement_node147 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node148 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) v2) (orb (negb v2) v0)) v3) (orb (negb v3) v0))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node149 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v2) v1)) (Bool.eqb (Bool.eqb v0 v2) v1)) = true. Definition statement_node150 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (Bool.eqb v0 v1) v2)) = true. Definition statement_node151 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node152 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) v2) (orb (negb v2) v0)) (orb (negb v2) v1)) v1)) (andb (andb v0 v1) v2)) = true. Definition statement_node153 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) v1)) (andb v0 v1)) = true. Definition statement_node154 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node155 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node156 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node157 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node158 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node159 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node160 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node161 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node162 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v0)) (orb (negb (orb (negb v0) v0)) (negb (orb (negb v1) v0)))) (orb (negb v0) v2))) (andb (andb v0 (negb v1)) v2)) = true. Definition statement_node163 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node164 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (andb (andb v0 v1) v2)) = true. Definition statement_node165 : Prop := forall (v0 : bool), (orb (negb v0) v0) = true. Definition statement_node166 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (orb (negb (andb v0 v1)) v2))) (Bool.eqb v2 (andb v0 v1))) = true. Definition statement_node167 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (orb (negb (andb v0 v1)) (andb v2 v3))) = true. Definition statement_node168 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node169 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (orb (negb (andb v0 v1)) v2)) (orb (negb v0) (orb (negb v1) v2))) = true. Definition statement_node170 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v2) v1)) = true. Definition statement_node171 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v2) v1)) = true. Definition statement_node172 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node173 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) v2) = true. Definition statement_node174 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) v1)) (andb v0 v1)) = true. Definition statement_node175 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) v1)) (andb v0 v1)) = true. Definition statement_node176 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (Bool.eqb v0 (Bool.eqb v1 v2))) = true. Definition statement_node177 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) v3) v4)) (andb (andb (andb (andb v0 v1) v2) v3) v4)) = true. Definition statement_node178 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node179 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb v0) (negb (negb (andb (andb v0 v1) v2))))) = true. Definition statement_node180 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node181 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node182 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node183 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node184 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (orb (negb (andb v0 v1)) (andb v2 v3))) = true. Definition statement_node185 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node186 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node187 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node188 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node189 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 v1) v2) (orb (negb v2) (orb (negb v1) v0)))) (orb (negb (Bool.eqb v2 (orb (negb v2) (negb (orb (negb v2) (negb v2)))))) (orb (negb v1) v0))) = true. Definition statement_node190 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (Bool.eqb v0 v1))) (andb v0 v1)) = true. Definition statement_node191 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (Bool.eqb v3 v4))) (Bool.eqb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node192 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node193 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node194 : Prop := forall (v0 : bool), (orb (negb (Bool.eqb v0 v0)) (Bool.eqb v0 v0)) = true. Definition statement_node195 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (Bool.eqb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node196 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v0))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node197 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (Bool.eqb v3 v0))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node198 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node199 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) v1)) (andb v0 v1)) = true. Definition statement_node200 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v4 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (Bool.eqb (Bool.eqb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node201 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node202 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node203 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v3 v1) v2) v0)) (Bool.eqb (andb (orb (negb v3) v1) (orb (negb v2) v1)) v0)) = true. Definition statement_node204 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v2) v1)) (andb (andb v0 v2) v1)) = true. Definition statement_node205 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node206 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v0) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node207 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node208 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) v2)) (Bool.eqb v0 (andb v1 v2))) = true. Definition statement_node209 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node210 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node211 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v0))) (andb v0 v1)) = true. Definition statement_node212 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node213 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node214 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node215 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (orb (negb (andb v0 v1)) v2))) (Bool.eqb v0 v2)) = true. Definition statement_node216 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node217 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (orb (negb v0) v1)) (orb (negb v0) v1)) = true. Definition statement_node218 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb v2) (andb v0 v1))) = true. Definition statement_node219 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node220 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node221 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb v0 (orb (negb v0) (orb (negb v1) v2)))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node222 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 v1) (orb (negb v0) v1)) (orb (negb v1) v0)) v2) (orb (negb v2) v0)) (orb (negb v2) v1))) (andb (andb v0 v1) v2)) = true. Definition statement_node223 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node224 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v1 v0)) (Bool.eqb v2 v0))) (Bool.eqb v2 (Bool.eqb v1 v0))) = true. Definition statement_node225 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (orb (negb v1) v2))) (Bool.eqb (andb v0 v2) v1)) = true. Definition statement_node226 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) (andb v0 v1))) (orb (negb (andb v0 v1)) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node227 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node228 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v1 v2) v0)) (orb v1 v2)) = true. Definition statement_node229 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (orb (negb (andb v0 v1)) (andb v2 v3))) = true. Definition statement_node230 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node231 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node232 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (Bool.eqb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node233 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v0))) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node234 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node235 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (Bool.eqb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node236 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (Bool.eqb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node237 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node238 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) v3) = true. Definition statement_node239 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) (Bool.eqb v1 v2))) (Bool.eqb (Bool.eqb v2 v1) v2))) (Bool.eqb (Bool.eqb v0 v1) v2)) = true. Definition statement_node240 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) v2) = true. Definition statement_node241 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (Bool.eqb (andb v2 v1) v0)) = true. Definition statement_node242 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 (negb v3))) (negb v3))) (andb (andb v0 v1) (andb v2 (negb v3)))) = true. Definition statement_node243 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb (negb v0) (Bool.eqb (negb v0) (negb v1))) (Bool.eqb (negb v1) (negb v2))) (Bool.eqb (negb v2) v3)) v3)) (andb (negb (andb v0 v1)) (andb (negb v2) v3))) = true. Definition statement_node244 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node245 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (Bool.eqb v1 v2)) (orb (negb v1) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node246 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node247 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (Bool.eqb v2 (Bool.eqb v1 v0))) = true. Definition statement_node248 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v2)) (orb (negb v2) v1))) (Bool.eqb v2 (orb (negb (orb (negb v2) (negb (Bool.eqb v0 (negb v2))))) v1))) = true. Definition statement_node249 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v2)) (orb (negb v2) v1))) (Bool.eqb v2 (orb (negb (orb (negb v2) (negb (Bool.eqb v0 (negb v2))))) v1))) = true. Definition statement_node250 : Prop := forall (A : Type) (step : A -> option A) (fuel : nat) (s : A), (iterations step fuel s <= fuel)%nat. Definition statement_node251 : Prop := forall (A : Type) (step : A -> option A) (fuel : nat) (s : A), (iterations step fuel s <= fuel)%nat. Definition statement_node252 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (orb (negb (orb (negb (andb v0 v1)) (andb v2 v3))) v4)) = true. Definition statement_node253 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (orb (negb v5) (andb (andb (andb v0 v1) (andb v2 v3)) v4))) = true. Definition statement_node254 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (orb (negb (orb (negb v3) v2)) (orb (negb v1) v0))) = true. Definition statement_node255 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v0)) (Bool.eqb v0 (negb v1)))) (andb v0 (negb v1))) = true. Definition statement_node256 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node257 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node258 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node259 : Prop := forall n : Z, signedIntegerPower n = 1 \/ signedIntegerPower n = -1. Definition statement_node260 : Prop := forall n : Z, signedIntegerPower n = 1 \/ signedIntegerPower n = -1. Definition statement_node261 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (orb (negb v4) (orb (negb (orb (negb v3) v2)) (orb (negb v1) v0)))) = true. Definition statement_node262 : Prop := forall b : bool, (if b then (1:Z) else -1) = 1 \/ (if b then (1:Z) else -1) = -1. Definition statement_node263 : Prop := forall b : bool, (if b then (1:Z) else -1) = 1 \/ (if b then (1:Z) else -1) = -1. Definition statement_node264 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 v1) (orb (negb v1) v0))) (orb (negb v1) (andb v0 (negb (negb v0))))) = true. Definition statement_node265 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v0)) (orb (negb (andb v3 v0)) v4))) (orb (negb v3) (andb v0 v4))) = true. Definition statement_node266 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node267 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) v1)) (andb v0 v1)) = true. Definition statement_node268 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node269 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (orb (negb (Bool.eqb (Bool.eqb v2 v1) v0)) v3)) = true. Definition statement_node270 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node271 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 (negb v2)))) (andb (andb v0 v1) (negb v2))) = true. Definition statement_node272 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (orb (negb (orb (negb (andb v0 v1)) (andb v2 v3))) v4)) = true. Definition statement_node273 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node274 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v0 v2)) v1) (orb (negb v1) v0)) v0) (orb (negb v1) v2)) v2) (orb (negb v2) v3)) v4)) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node275 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb v1 (Bool.eqb v1 v2)) (Bool.eqb v2 v0)) (Bool.eqb v0 v0)) v0)) (andb (andb (Bool.eqb v1 v2) (andb v1 v2)) v0)) = true. Definition statement_node276 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb v3 (Bool.eqb v3 v5)) (Bool.eqb v3 v2)) (Bool.eqb v5 v4)) (Bool.eqb v2 v4)) (Bool.eqb v2 v5)) (Bool.eqb v3 v4)) (Bool.eqb v3 v5)) (Bool.eqb v5 v0)) (Bool.eqb v3 v0)) (Bool.eqb v0 v1)) (Bool.eqb v1 v1)) v3) v2) v5) v4) v0) v1)) (andb (andb (andb (andb v3 v5) (andb v2 v4)) v0) v1)) = true. Definition statement_node277 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node278 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5) v6)) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node279 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node280 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node281 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node282 : Prop := forall (v0 : bool), (orb (negb v0) v0) = true. Definition statement_node283 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v2 v0) v1)) (andb (Bool.eqb v2 v0) v1)) = true. Definition statement_node284 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v3 v1) v2) v0)) (Bool.eqb (Bool.eqb v3 v1) (Bool.eqb v1 v0))) = true. Definition statement_node285 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (Bool.eqb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node286 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node287 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (orb (negb v0) v1))) (Bool.eqb v0 v1)) = true. Definition statement_node288 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node289 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node290 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (Bool.eqb v1 v2))) (orb (negb (orb (negb v2) v0)) v1)) = true. Definition statement_node291 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (orb (negb v4) (Bool.eqb (andb v0 v1) (andb v2 v3)))) = true. Definition statement_node292 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node293 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (orb (negb (andb v0 v1)) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node294 : Prop := forall value : Z, - (- value) = value. Definition statement_node295 : Prop := forall value : Z, - (- value) = value. Definition statement_node296 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node297 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (Bool.eqb v2 (andb v0 v1)))) (andb (andb v0 v1) v2)) = true. Definition statement_node298 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) v1)) (andb v0 v1)) = true. Definition statement_node299 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (orb (negb v0) v1)) v2)) = true. Definition statement_node300 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (andb v0 v1)) (orb (negb v1) v2)) (Bool.eqb v0 v3))) (orb (negb (orb (negb v3) (andb v0 v1))) v2)) = true. Definition statement_node301 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node302 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v0))) (andb (andb v0 v1) v2)) = true. Definition statement_node303 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node304 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (andb (andb (orb (negb v0) v1) (Bool.eqb v1 v2)) (orb (negb v1) v2))) = true. Definition statement_node305 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node306 : Prop := forall a b : Z, Z.abs a <> Z.abs b -> dominantValue a b = dominantValue b a. Definition statement_node307 : Prop := forall a b : Z, Z.abs a <> Z.abs b -> dominantValue a b = dominantValue b a. Definition statement_node308 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (Bool.eqb v2 v3)) (orb (negb v3) v4))) (Bool.eqb v4 (andb (Bool.eqb v3 v2) (Bool.eqb v1 v0)))) = true. Definition statement_node309 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) (Bool.eqb v0 v1)) (orb (negb v2) (andb v0 v1)))) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node310 : Prop := forall (v0 : bool), (orb (negb v0) v0) = true. Definition statement_node311 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (Bool.eqb v1 v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node312 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v1 (orb (negb v1) v2)) (Bool.eqb v2 v3)) (orb (negb v3) v0))) (andb (andb v1 v2) (andb v3 v0))) = true. Definition statement_node313 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v2 (orb (negb v2) v3)) (Bool.eqb v3 v0)) (orb (negb v0) v1))) (andb (andb v2 v3) (andb v0 v1))) = true. Definition statement_node314 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v3 (orb (negb v3) v0)) (Bool.eqb v0 v1)) (orb (negb v1) v2))) (andb (andb v3 v0) (andb v1 v2))) = true. Definition statement_node315 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node316 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (Bool.eqb v1 v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node317 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v1 (orb (negb v1) v2)) (Bool.eqb v2 v3)) (orb (negb v3) v0))) (andb (andb v1 v2) (andb v3 v0))) = true. Definition statement_node318 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v2 (orb (negb v2) v3)) (Bool.eqb v3 v0)) (orb (negb v0) v1))) (andb (andb v2 v3) (andb v0 v1))) = true. Definition statement_node319 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v3 (orb (negb v3) v0)) (Bool.eqb v0 v1)) (orb (negb v1) v2))) (andb (andb v3 v0) (andb v1 v2))) = true. Definition statement_node320 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node321 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node322 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node323 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) v1)) (andb v0 v1)) = true. Definition statement_node324 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) v3) v4)) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node325 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node326 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node327 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node328 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node329 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node330 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node331 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb (andb v0 v1) v2) v3) v4)) = true. Definition statement_node332 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node333 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v3 (orb (negb v3) v0)) (andb v0 v1)) (orb (negb v3) v2))) (Bool.eqb (orb (negb (andb v0 v1)) v2) v3)) = true. Definition statement_node334 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (andb v1 v2)) (orb (negb v0) v3))) (Bool.eqb (orb (negb (andb v0 v1)) v2) v3)) = true. Definition statement_node335 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v2) v0)) (orb (negb v2) v1))) (orb (negb v2) (andb v0 v1))) = true. Definition statement_node336 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node337 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node338 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) v3) v4)) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node339 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (Bool.eqb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node340 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node341 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v6))) (andb (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5) v6)) = true. Definition statement_node342 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node343 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node344 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node345 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node346 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node347 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb (andb v0 v1)) v2)) v3) (orb (negb v3) v4)) (orb (negb (andb v3 v4)) v5))) v5) = true. Definition statement_node348 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 v1) (negb (negb (andb v0 v1))))) (andb (andb v0 (negb (negb v0))) (andb v1 (negb (negb v1))))) = true. Definition statement_node349 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb (andb (Bool.eqb v0 v1) v1) (orb (negb v1) v0)) v0)) (andb v0 v1)) = true. Definition statement_node350 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb (andb v0 v1) v2) (Bool.eqb v0 v1)) (Bool.eqb v0 v2)) (Bool.eqb v1 v0)) (Bool.eqb v1 v2)) (Bool.eqb v2 v0)) (Bool.eqb v2 v1)) (Bool.eqb v0 v0)) (Bool.eqb v1 v1)) (Bool.eqb v2 v2)) v0) v1) v2)) (andb (andb v0 v1) v2)) = true. Definition statement_node351 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb v0 v1) v2) (Bool.eqb v0 v0)) (Bool.eqb v1 v1)) (Bool.eqb v2 v2)) v0) v1) v2)) (andb (andb v0 v1) v2)) = true. Definition statement_node352 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (Bool.eqb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node353 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5)) (orb (negb v5) v6))) (andb (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5) v6)) = true. Definition statement_node354 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node355 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node356 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (orb (negb (orb (negb v3) v2)) (orb (negb v1) v0))) = true. Definition statement_node357 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (orb (negb (orb (negb v2) v1)) v0)) = true. Definition statement_node358 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node359 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node360 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node361 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5)) v5)) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node362 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node363 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node364 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node365 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node366 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node367 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node368 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node369 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v0) v2)) (orb (negb v0) (Bool.eqb v1 v2))) v3) (orb (negb v3) v4)) (orb (negb v4) (andb (andb v0 v1) v2)))) (Bool.eqb v0 (Bool.eqb v1 v2))) = true. Definition statement_node370 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (Bool.eqb v2 v0) (Bool.eqb v1 v0))) = true. Definition statement_node371 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb v0 (orb (negb v0) (andb v1 v2)))) v2) = true. Definition statement_node372 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (orb (negb v0) v2) (orb (negb v2) v1))) (orb (negb (andb v0 v2)) v1)) = true. Definition statement_node373 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v2 (orb (negb v2) v1)) (orb (negb (orb (negb v2) v1)) v0))) (orb (negb v2) (negb (andb v2 (negb (andb v1 v0)))))) = true. Definition statement_node374 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node375 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node376 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) v3) (orb (negb v3) v0)) v0) v1) v2)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node377 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 v1)) (andb v0 v1)) = true. Definition statement_node378 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node379 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node380 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (orb (negb v2) (Bool.eqb v1 v0))) = true. Definition statement_node381 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node382 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (orb (negb v0) (andb v0 v1))) (andb v0 (andb v1 v2)))) = true. Definition statement_node383 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node384 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) (orb (negb v2) v0)) (orb (negb v2) v1))) (orb (negb v2) (andb v0 v1))) = true. Definition statement_node385 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) v2) (orb (negb v2) v0)) (orb (negb v2) v1)) v3) (orb (negb v3) v5)) v4) (orb (negb v4) v5)) v5)) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node386 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node387 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5)) (Bool.eqb v5 v0))) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node388 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5)) (Bool.eqb v5 v0))) (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) = true. Definition statement_node389 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node390 : Prop := forall u : ValidCycleUnit, sevenChecks u. Definition statement_node391 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node392 : Prop := forall u : ValidCycleUnit, sevenChecks u. Definition statement_node393 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node394 : Prop := forall (values : list Z) (parity : Z -> bool), signatureInvariants (generatedSignature values parity). Definition statement_node395 : Prop := forall (values : list Z) (parity : Z -> bool), signatureInvariants (generatedSignature values parity). Definition statement_node396 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) v1)) (andb v0 v1)) = true. Definition statement_node397 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node398 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node399 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb v0 (Bool.eqb v0 v1))) (Bool.eqb v1 v0)) = true. Definition statement_node400 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb v0 (orb (negb v0) (andb v1 v2)))) (Bool.eqb v2 (andb v1 v0))) = true. Definition statement_node401 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 v1) (Bool.eqb v0 v1))) (andb (andb v0 v1) (negb (negb (andb v0 v1))))) = true. Definition statement_node402 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (orb (negb v2) (Bool.eqb v1 v0))) = true. Definition statement_node403 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node404 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node405 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node406 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node407 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node408 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (Bool.eqb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node409 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node410 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (orb (negb (orb (negb v3) v2)) (orb (negb v1) v0))) = true. Definition statement_node411 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node412 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (orb (negb v0) v1)) (orb (negb (orb (negb v0) v0)) (orb (negb v1) v1))) = true. Definition statement_node413 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node414 : Prop := forall (v0 : bool), (orb (negb (andb v0 (Bool.eqb v0 (negb (orb (negb v0) (andb v0 (negb v0))))))) (andb v0 (negb (negb v0)))) = true. Definition statement_node415 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node416 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3))) (orb (andb (andb v0 v1) (andb v2 v3)) (negb (andb (andb v0 v1) (andb v2 v3))))) = true. Definition statement_node417 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) v2) v3) v4) v5)) (Bool.eqb (andb (andb v0 v1) (andb v2 v3)) (andb v4 v5))) = true. Definition statement_node418 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (Bool.eqb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node419 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (Bool.eqb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node420 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (orb (negb (andb (andb v0 v1) v2)) v3)) = true. Definition statement_node421 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node422 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node423 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (orb (negb (andb (andb v0 v1) v2)) v3)) = true. Definition statement_node424 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node425 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node426 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node427 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) (orb (negb (andb v0 v1)) v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node428 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb (andb (andb (andb v0 v1) (orb (negb v0) v1)) (orb (negb v1) v0)) (Bool.eqb v0 v1)) (andb v0 v1))) (andb (andb (orb (negb v0) v1) (orb (negb v1) v0)) (andb v0 v1))) = true. Definition statement_node429 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (orb (negb v0) v1) (orb (negb v0) v2))) (orb (negb v0) (andb v1 v2))) = true. Definition statement_node430 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (andb v0 v1)) (andb v1 v2)) (andb v2 v3))) (Bool.eqb (Bool.eqb v0 v1) (Bool.eqb v2 v3))) = true. Definition statement_node431 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node432 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node433 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node434 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (orb (negb (orb (negb v0) v0)) v1) (orb (negb v1) v2))) (andb (orb (negb (orb (negb (orb (negb v0) v0)) v1)) v2) (orb (negb (orb (negb (orb (negb v0) v0)) (negb v1))) (negb v2)))) = true. Definition statement_node435 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node436 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (Bool.eqb (andb (andb v0 v1) v2) v3)) = true. Definition statement_node437 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node438 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node439 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 v1) v2)) (Bool.eqb (Bool.eqb (Bool.eqb v0 v1) (Bool.eqb v1 v2)) (Bool.eqb v2 v0))) = true. Definition statement_node440 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node441 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool) (v7 : bool) (v8 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4)) (Bool.eqb v4 v5)) (Bool.eqb v5 v6)) (Bool.eqb v6 v7)) (Bool.eqb v7 v8))) (andb (andb (andb (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5) v6) v7) v8)) = true. Definition statement_node442 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v1)) v2)) = true. Definition statement_node443 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node444 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) v2) = true. Definition statement_node445 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (orb (negb v0) v0)) (orb (negb (orb (negb v0) v0)) (andb (orb (negb v1) v1) (orb (negb v2) v2)))) = true. Definition statement_node446 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (Bool.eqb (andb v0 v1) v2)) = true. Definition statement_node447 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node448 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v2)) v1)) = true. Definition statement_node449 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (orb (negb (orb (negb v2) v1)) v0)) = true. Definition statement_node450 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2)) (orb (negb v0) v3)) (Bool.eqb v3 v4)) v3)) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node451 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) v4)) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node452 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2))) (andb (andb v0 v1) v2)) = true. Definition statement_node453 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (orb (negb (orb (negb v3) v2)) (orb (negb v1) v0))) = true. Definition statement_node454 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node455 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb v0 (orb (negb v0) v0))) (andb (orb v1 (negb v1)) (negb (andb v2 (negb v2))))) = true. Definition statement_node456 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v0))) (andb (Bool.eqb v1 v0) (orb (negb v2) v2))) = true. Definition statement_node457 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v0)) (Bool.eqb v0 (negb v1)))) (andb v0 (negb v1))) = true. Definition statement_node458 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) = true. Definition statement_node459 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node460 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool) (v6 : bool), (orb (negb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v6))) (andb (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5) v6)) = true. Definition statement_node461 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node462 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node463 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node464 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v0)) (Bool.eqb v0 (negb v1)))) (andb v0 (negb v1))) = true. Definition statement_node465 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) = true. Definition statement_node466 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node467 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node468 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node469 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node470 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node471 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) (andb v1 v2))) (orb (negb (andb v1 v2)) v3)) (orb (negb v0) v0))) (andb v3 (orb (negb v3) v3))) = true. Definition statement_node472 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (orb (negb v0) v1) (orb (negb v1) v0))) (andb (orb (negb v0) v1) (Bool.eqb v1 v0))) = true. Definition statement_node473 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 v1) v2) v3)) (Bool.eqb (Bool.eqb v0 v1) (andb v2 v3))) = true. Definition statement_node474 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (orb (negb v2) (Bool.eqb v1 v0))) = true. Definition statement_node475 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2))) (orb (negb (andb v0 v2)) v1)) = true. Definition statement_node476 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) (andb v1 v2))) (orb (negb (andb v1 v2)) v3)) (orb (negb v0) v0))) (andb v3 (orb (negb v3) v3))) = true. Definition statement_node477 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (andb (andb v0 (negb (negb v1))) (Bool.eqb v0 v1))) (andb v0 v1)) = true. Definition statement_node478 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node479 : Prop := forall (v0 : bool) (v1 : bool), (orb (negb (Bool.eqb v0 v1)) (Bool.eqb v0 v1)) = true. Definition statement_node480 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node481 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node482 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (Bool.eqb v0 v1)) (orb (negb v1) v2))) (orb (negb (andb (andb v0 v1) v2)) (negb (andb (andb (andb v0 v1) v2) (negb (andb (andb v0 v1) v2)))))) = true. Definition statement_node483 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (andb (andb (andb v0 v1) (andb v2 v3)) v4)) = true. Definition statement_node484 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node485 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb v0 (orb (negb v0) (andb v1 v2)))) (orb (negb v0) (negb (orb (negb v0) (negb (andb v1 v2)))))) = true. Definition statement_node486 : Prop := forall (v0 : bool), (orb (negb v0) v0) = true. Definition statement_node487 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node488 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb v0 (Bool.eqb v0 v1)) (Bool.eqb v1 v2)) (Bool.eqb v2 v3))) (andb (andb v0 v1) (andb v2 v3))) = true. Definition statement_node489 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb v0 (orb (negb v0) (negb v1))) (orb (negb (andb v1 v2)) v4)) (orb (negb (andb v2 v3)) v3))) (andb (orb (negb v3) (negb (andb v1 v4))) (orb (negb v3) v0))) = true. Definition statement_node490 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (Bool.eqb v0 v1) (Bool.eqb v1 v2))) (orb (negb v2) (Bool.eqb v1 v0))) = true. Definition statement_node491 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool), (orb (negb (andb (andb (andb (andb v0 v1) v2) (orb (negb (andb v0 v1)) v3)) (orb (negb (andb v1 v2)) v3))) (Bool.eqb v3 v1)) = true. Definition statement_node492 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node493 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool) (v5 : bool), (orb (negb (andb (andb (andb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (orb (negb v2) v3)) (orb (negb v3) v4)) (orb (negb v4) v5)) (orb (negb v5) v0)) (negb (andb (andb (andb (andb (andb (negb v0) (negb v1)) (negb v2)) (negb v3)) (negb v4)) (negb v5))))) (andb (andb (andb (andb v0 v1) (andb v2 v3)) v4) v5)) = true. Definition statement_node494 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool) (v3 : bool) (v4 : bool), (orb (negb (andb (andb (andb (andb v0 (orb (negb v0) v1)) (orb (negb v1) v2)) (Bool.eqb v2 v3)) (Bool.eqb v3 v4))) (Bool.eqb (andb (andb v4 v3) (andb v2 v1)) v0)) = true. Definition statement_node495 : Prop := forall (A : Type) (a : A), a = a. Definition statement_node496 : Prop := forall a : Z, exponentXorState a a = 1. Definition statement_node497 : Prop := forall a : Z, exponentXorState a a = 1. Definition statement_node498 : Prop := forall (v0 : bool) (v1 : bool) (v2 : bool), (orb (negb (andb (andb v0 (orb (negb v0) v1)) (Bool.eqb v2 v0))) (andb (andb v0 v1) v2)) = true. Definition statement_node499 : Prop := MCBProgram = MCBData. Definition statement_node500 : Prop := forall e : MCBExpr, unquoteMCB (quoteMCB e) = e. Definition statement_node501 : Prop := forall d : MCBKey, quoteMCB (unquoteMCB d) = d. Definition statement_node502 : Prop := forall n : Z, phaseMCB n = 1 \/ phaseMCB n = -1. Definition statement_node503 : Prop := forall n : Z, Z.modulo n 2 = 0 -> phaseMCB n = 1. Definition statement_node504 : Prop := forall e : MCBExpr, evalMCBData (quoteMCB e) = evalMCB e. Definition statement_node505 : Prop := forall (f : Z -> Z) (e : MCBExpr), quoteMCB (reweightMCB f e) = reweightMCBData f (quoteMCB e). Definition statement_node506 : Prop := forall e : MCBExpr, evalMCB e = sumMCBData (mcbContributions e). Definition statement_node507 : Prop := forall e : MCBExpr, evalMCB (normalizeMCB e) = evalMCB e. Definition statement_node508 : Prop := forall e : MCBExpr, normalizeMCB (normalizeMCB e) = normalizeMCB e. Definition statement_node509 : Prop := forall e : MCBExpr, exists v : Z, evalMCB e = v /\ forall w : Z, evalMCB e = w -> w = v. Definition statement_node510 : Prop := forall e : MCBExpr, forall v : Z, ~ (evalMCB e = v /\ evalMCB e <> v). Definition statement_node511 : Prop := mcbContributions mcbInitProgram = [-1; 1; -1; 1; -1; 1; -1; 1]. Definition statement_node512 : Prop := evalMCB mcbInitProgram = 0. Definition statement_node513 : Prop := normalizeMCB mcbInitProgram = mcbBalance 0. Definition statement_node514 : Prop := phaseMCB (evalMCB mcbInitProgram) = 1. Definition statement_node515 : Prop := normalizeMCB mcbInitialization = mcbBalance 1. Definition statement_node516 : Prop := evalMCB mcbInitProgram = compiledMCBInitBalance. Definition statement_node517 : Prop := compiledMCBInitBalance = 0. Definition statement_node518 : Prop := evalMCB mcbInitProgram <> -1. Definition statement_node519 : Prop := forall p q : bool, nativeNand p q = signed (negb (andb p q)). Definition statement_node520 : Prop := forall xs : list bool, fold_left andb xs true = sourceConjunction xs. Definition statement_node521 : Prop := encode roleGround (-1) = Some true. Definition statement_node522 : Prop := encode roleRuntime (-1) = Some false. Definition statement_node523 : Prop := forall b : bool, encode roleRuntime (signed b) = Some b. Theorem node0 : statement_node0. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node1 : statement_node1. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node2 : statement_node2. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node3 : statement_node3. Proof. intros A a; reflexivity. Qed. Theorem node4 : statement_node4. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node5 : statement_node5. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node6 : statement_node6. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node7 : statement_node7. Proof. intros A a; reflexivity. Qed. Theorem node8 : statement_node8. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node9 : statement_node9. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node10 : statement_node10. Proof. intros A a; reflexivity. Qed. Theorem node11 : statement_node11. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node12 : statement_node12. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node13 : statement_node13. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node14 : statement_node14. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node15 : statement_node15. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node16 : statement_node16. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node17 : statement_node17. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node18 : statement_node18. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node19 : statement_node19. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node20 : statement_node20. Proof. intros A a; reflexivity. Qed. Theorem node21 : statement_node21. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node22 : statement_node22. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node23 : statement_node23. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node24 : statement_node24. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node25 : statement_node25. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node26 : statement_node26. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node27 : statement_node27. Proof. intros A a; reflexivity. Qed. Theorem node28 : statement_node28. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node29 : statement_node29. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node30 : statement_node30. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node31 : statement_node31. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node32 : statement_node32. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node33 : statement_node33. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node34 : statement_node34. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node35 : statement_node35. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node36 : statement_node36. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node37 : statement_node37. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node38 : statement_node38. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node39 : statement_node39. Proof. intros A a; reflexivity. Qed. Theorem node40 : statement_node40. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node41 : statement_node41. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node42 : statement_node42. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node43 : statement_node43. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node44 : statement_node44. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node45 : statement_node45. Proof. intros A a; reflexivity. Qed. Theorem node46 : statement_node46. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node47 : statement_node47. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node48 : statement_node48. Proof. intros A a; reflexivity. Qed. Theorem node49 : statement_node49. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node50 : statement_node50. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node51 : statement_node51. Proof. intros A a; reflexivity. Qed. Theorem node52 : statement_node52. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node53 : statement_node53. Proof. intros A a; reflexivity. Qed. Theorem node54 : statement_node54. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node55 : statement_node55. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node56 : statement_node56. Proof. intros A a; reflexivity. Qed. Theorem node57 : statement_node57. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node58 : statement_node58. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node59 : statement_node59. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node60 : statement_node60. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node61 : statement_node61. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node62 : statement_node62. Proof. intros A a; reflexivity. Qed. Theorem node63 : statement_node63. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node64 : statement_node64. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node65 : statement_node65. Proof. intros A a; reflexivity. Qed. Theorem node66 : statement_node66. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node67 : statement_node67. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node68 : statement_node68. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node69 : statement_node69. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node70 : statement_node70. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node71 : statement_node71. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node72 : statement_node72. Proof. intros A a; reflexivity. Qed. Theorem node73 : statement_node73. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node74 : statement_node74. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node75 : statement_node75. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node76 : statement_node76. Proof. intros A condition t e; destruct condition; [left|right]; reflexivity. Qed. Theorem node77 : statement_node77. Proof. intros A condition t e; destruct condition; [left|right]; reflexivity. Qed. Theorem node78 : statement_node78. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node79 : statement_node79. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node80 : statement_node80. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node81 : statement_node81. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node82 : statement_node82. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node83 : statement_node83. Proof. intros v0 v1 v2 v3 v4 v5 v6; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; destruct v6; reflexivity. Qed. Theorem node84 : statement_node84. Proof. intros A a; reflexivity. Qed. Theorem node85 : statement_node85. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node86 : statement_node86. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node87 : statement_node87. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node88 : statement_node88. Proof. intros A a; reflexivity. Qed. Theorem node89 : statement_node89. Proof. intros World access w unfixed v reachable; exists constructiveLogos; exact I. Qed. Theorem node90 : statement_node90. Proof. intros World access w unfixed v reachable; exists constructiveLogos; exact I. Qed. Theorem node91 : statement_node91. Proof. intros A a; reflexivity. Qed. Theorem node92 : statement_node92. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node93 : statement_node93. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node94 : statement_node94. Proof. intros A a; reflexivity. Qed. Theorem node95 : statement_node95. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node96 : statement_node96. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node97 : statement_node97. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node98 : statement_node98. Proof. intros A a; reflexivity. Qed. Theorem node99 : statement_node99. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node100 : statement_node100. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node101 : statement_node101. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node102 : statement_node102. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node103 : statement_node103. Proof. intros A a; reflexivity. Qed. Theorem node104 : statement_node104. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node105 : statement_node105. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node106 : statement_node106. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node107 : statement_node107. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node108 : statement_node108. Proof. intros v0 v1 v2 v3 v4 v5 v6 v7 v8 v9; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; destruct v6; destruct v7; destruct v8; destruct v9; reflexivity. Qed. Theorem node109 : statement_node109. Proof. intros A a; reflexivity. Qed. Theorem node110 : statement_node110. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node111 : statement_node111. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node112 : statement_node112. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node113 : statement_node113. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node114 : statement_node114. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node115 : statement_node115. Proof. intros A a; reflexivity. Qed. Theorem node116 : statement_node116. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node117 : statement_node117. Proof. intros u; split; reflexivity. Qed. Theorem node118 : statement_node118. Proof. intros u; split; reflexivity. Qed. Theorem node119 : statement_node119. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node120 : statement_node120. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node121 : statement_node121. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node122 : statement_node122. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node123 : statement_node123. Proof. intros A a; reflexivity. Qed. Theorem node124 : statement_node124. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node125 : statement_node125. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node126 : statement_node126. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node127 : statement_node127. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node128 : statement_node128. Proof. intros A a; reflexivity. Qed. Theorem node129 : statement_node129. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node130 : statement_node130. Proof. intros A a; reflexivity. Qed. Theorem node131 : statement_node131. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node132 : statement_node132. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node133 : statement_node133. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node134 : statement_node134. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node135 : statement_node135. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node136 : statement_node136. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node137 : statement_node137. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node138 : statement_node138. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node139 : statement_node139. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node140 : statement_node140. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node141 : statement_node141. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node142 : statement_node142. Proof. intros A a; reflexivity. Qed. Theorem node143 : statement_node143. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node144 : statement_node144. Proof. intros A a; reflexivity. Qed. Theorem node145 : statement_node145. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node146 : statement_node146. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node147 : statement_node147. Proof. intros A a; reflexivity. Qed. Theorem node148 : statement_node148. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node149 : statement_node149. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node150 : statement_node150. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node151 : statement_node151. Proof. intros A a; reflexivity. Qed. Theorem node152 : statement_node152. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node153 : statement_node153. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node154 : statement_node154. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node155 : statement_node155. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node156 : statement_node156. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node157 : statement_node157. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node158 : statement_node158. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node159 : statement_node159. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node160 : statement_node160. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node161 : statement_node161. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node162 : statement_node162. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node163 : statement_node163. Proof. intros A a; reflexivity. Qed. Theorem node164 : statement_node164. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node165 : statement_node165. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node166 : statement_node166. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node167 : statement_node167. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node168 : statement_node168. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node169 : statement_node169. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node170 : statement_node170. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node171 : statement_node171. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node172 : statement_node172. Proof. intros A a; reflexivity. Qed. Theorem node173 : statement_node173. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node174 : statement_node174. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node175 : statement_node175. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node176 : statement_node176. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node177 : statement_node177. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node178 : statement_node178. Proof. intros A a; reflexivity. Qed. Theorem node179 : statement_node179. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node180 : statement_node180. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node181 : statement_node181. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node182 : statement_node182. Proof. intros A a; reflexivity. Qed. Theorem node183 : statement_node183. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node184 : statement_node184. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node185 : statement_node185. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node186 : statement_node186. Proof. intros A a; reflexivity. Qed. Theorem node187 : statement_node187. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node188 : statement_node188. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node189 : statement_node189. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node190 : statement_node190. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node191 : statement_node191. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node192 : statement_node192. Proof. intros A a; reflexivity. Qed. Theorem node193 : statement_node193. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node194 : statement_node194. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node195 : statement_node195. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node196 : statement_node196. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node197 : statement_node197. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node198 : statement_node198. Proof. intros A a; reflexivity. Qed. Theorem node199 : statement_node199. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node200 : statement_node200. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node201 : statement_node201. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node202 : statement_node202. Proof. intros A a; reflexivity. Qed. Theorem node203 : statement_node203. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node204 : statement_node204. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node205 : statement_node205. Proof. intros A a; reflexivity. Qed. Theorem node206 : statement_node206. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node207 : statement_node207. Proof. intros A a; reflexivity. Qed. Theorem node208 : statement_node208. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node209 : statement_node209. Proof. intros A a; reflexivity. Qed. Theorem node210 : statement_node210. Proof. intros A a; reflexivity. Qed. Theorem node211 : statement_node211. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node212 : statement_node212. Proof. intros A a; reflexivity. Qed. Theorem node213 : statement_node213. Proof. intros A a; reflexivity. Qed. Theorem node214 : statement_node214. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node215 : statement_node215. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node216 : statement_node216. Proof. intros A a; reflexivity. Qed. Theorem node217 : statement_node217. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node218 : statement_node218. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node219 : statement_node219. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node220 : statement_node220. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node221 : statement_node221. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node222 : statement_node222. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node223 : statement_node223. Proof. intros A a; reflexivity. Qed. Theorem node224 : statement_node224. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node225 : statement_node225. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node226 : statement_node226. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node227 : statement_node227. Proof. intros A a; reflexivity. Qed. Theorem node228 : statement_node228. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node229 : statement_node229. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node230 : statement_node230. Proof. intros A a; reflexivity. Qed. Theorem node231 : statement_node231. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node232 : statement_node232. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node233 : statement_node233. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node234 : statement_node234. Proof. intros A a; reflexivity. Qed. Theorem node235 : statement_node235. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node236 : statement_node236. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node237 : statement_node237. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node238 : statement_node238. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node239 : statement_node239. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node240 : statement_node240. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node241 : statement_node241. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node242 : statement_node242. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node243 : statement_node243. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node244 : statement_node244. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node245 : statement_node245. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node246 : statement_node246. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node247 : statement_node247. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node248 : statement_node248. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node249 : statement_node249. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node250 : statement_node250. Proof. intros A step fuel; induction fuel as [|n IH]; intros s; simpl; [lia|]; destruct (step s) as [t|]; simpl; [apply le_n_S; apply IH|lia]. Qed. Theorem node251 : statement_node251. Proof. intros A step fuel; induction fuel as [|n IH]; intros s; simpl; [lia|]; destruct (step s) as [t|]; simpl; [apply le_n_S; apply IH|lia]. Qed. Theorem node252 : statement_node252. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node253 : statement_node253. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node254 : statement_node254. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node255 : statement_node255. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node256 : statement_node256. Proof. intros A a; reflexivity. Qed. Theorem node257 : statement_node257. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node258 : statement_node258. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node259 : statement_node259. Proof. intro n; unfold signedIntegerPower; destruct (Z.even n); [left|right]; reflexivity. Qed. Theorem node260 : statement_node260. Proof. intro n; unfold signedIntegerPower; destruct (Z.even n); [left|right]; reflexivity. Qed. Theorem node261 : statement_node261. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node262 : statement_node262. Proof. intro b; destruct b; [left|right]; reflexivity. Qed. Theorem node263 : statement_node263. Proof. intro b; destruct b; [left|right]; reflexivity. Qed. Theorem node264 : statement_node264. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node265 : statement_node265. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node266 : statement_node266. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node267 : statement_node267. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node268 : statement_node268. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node269 : statement_node269. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node270 : statement_node270. Proof. intros A a; reflexivity. Qed. Theorem node271 : statement_node271. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node272 : statement_node272. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node273 : statement_node273. Proof. intros A a; reflexivity. Qed. Theorem node274 : statement_node274. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node275 : statement_node275. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node276 : statement_node276. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node277 : statement_node277. Proof. intros A a; reflexivity. Qed. Theorem node278 : statement_node278. Proof. intros v0 v1 v2 v3 v4 v5 v6; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; destruct v6; reflexivity. Qed. Theorem node279 : statement_node279. Proof. intros A a; reflexivity. Qed. Theorem node280 : statement_node280. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node281 : statement_node281. Proof. intros A a; reflexivity. Qed. Theorem node282 : statement_node282. Proof. intros v0; destruct v0; reflexivity. Qed. Theorem node283 : statement_node283. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node284 : statement_node284. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node285 : statement_node285. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node286 : statement_node286. Proof. intros v0 v1 v2 v3 v4 v5; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; destruct v5; reflexivity. Qed. Theorem node287 : statement_node287. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node288 : statement_node288. Proof. intros A a; reflexivity. Qed. Theorem node289 : statement_node289. Proof. intros A a; reflexivity. Qed. Theorem node290 : statement_node290. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node291 : statement_node291. Proof. intros v0 v1 v2 v3 v4; destruct v0; destruct v1; destruct v2; destruct v3; destruct v4; reflexivity. Qed. Theorem node292 : statement_node292. Proof. intros A a; reflexivity. Qed. Theorem node293 : statement_node293. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node294 : statement_node294. Proof. intro value; ring. Qed. Theorem node295 : statement_node295. Proof. intro value; ring. Qed. Theorem node296 : statement_node296. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node297 : statement_node297. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node298 : statement_node298. Proof. intros v0 v1; destruct v0; destruct v1; reflexivity. Qed. Theorem node299 : statement_node299. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node300 : statement_node300. Proof. intros v0 v1 v2 v3; destruct v0; destruct v1; destruct v2; destruct v3; reflexivity. Qed. Theorem node301 : statement_node301. Proof. intros A a; reflexivity. Qed. Theorem node302 : statement_node302. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node303 : statement_node303. Proof. intros A a; reflexivity. Qed. Theorem node304 : statement_node304. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node305 : statement_node305. Proof. intros v0 v1 v2; destruct v0; destruct v1; destruct v2; reflexivity. Qed. Theorem node306 : statement_node306. Proof. intros a b H; unfold dominantValue. destruct (Z_lt_dec (Z.abs a) (Z.abs b)) as [Hlt|Hge]. - assert (Z.abs a Prop := | certified_nil : Certified [] | certified_cons : forall (p : Prop) (ps : list Prop), p -> Certified ps -> Certified (p :: ps). Theorem certified_member : forall ps, Certified ps -> forall p, In p ps -> p. Proof. intros ps proof; induction proof as [|p ps hp rest IH]. - intros q H; inversion H. - intros q H; simpl in H; destruct H as [H|H]. + subst q; exact hp. + exact (IH q H). Qed. Definition allStatements : list Prop := [statement_node0; statement_node1; statement_node2; statement_node3; statement_node4; statement_node5; statement_node6; statement_node7; statement_node8; statement_node9; statement_node10; statement_node11; statement_node12; statement_node13; statement_node14; statement_node15; statement_node16; statement_node17; statement_node18; statement_node19; statement_node20; statement_node21; statement_node22; statement_node23; statement_node24; statement_node25; statement_node26; statement_node27; statement_node28; statement_node29; statement_node30; statement_node31; statement_node32; statement_node33; statement_node34; statement_node35; statement_node36; statement_node37; statement_node38; statement_node39; statement_node40; statement_node41; statement_node42; statement_node43; statement_node44; statement_node45; statement_node46; statement_node47; statement_node48; statement_node49; statement_node50; statement_node51; statement_node52; statement_node53; statement_node54; statement_node55; statement_node56; statement_node57; statement_node58; statement_node59; statement_node60; statement_node61; statement_node62; statement_node63; statement_node64; statement_node65; statement_node66; statement_node67; statement_node68; statement_node69; statement_node70; statement_node71; statement_node72; statement_node73; statement_node74; statement_node75; statement_node76; statement_node77; statement_node78; statement_node79; statement_node80; statement_node81; statement_node82; statement_node83; statement_node84; statement_node85; statement_node86; statement_node87; statement_node88; statement_node89; statement_node90; statement_node91; statement_node92; statement_node93; statement_node94; statement_node95; statement_node96; statement_node97; statement_node98; statement_node99; statement_node100; statement_node101; statement_node102; statement_node103; statement_node104; statement_node105; statement_node106; statement_node107; statement_node108; statement_node109; statement_node110; statement_node111; statement_node112; statement_node113; statement_node114; statement_node115; statement_node116; statement_node117; statement_node118; statement_node119; statement_node120; statement_node121; statement_node122; statement_node123; statement_node124; statement_node125; statement_node126; statement_node127; statement_node128; statement_node129; statement_node130; statement_node131; statement_node132; statement_node133; statement_node134; statement_node135; statement_node136; statement_node137; statement_node138; statement_node139; statement_node140; statement_node141; statement_node142; statement_node143; statement_node144; statement_node145; statement_node146; statement_node147; statement_node148; statement_node149; statement_node150; statement_node151; statement_node152; statement_node153; statement_node154; statement_node155; statement_node156; statement_node157; statement_node158; statement_node159; statement_node160; statement_node161; statement_node162; statement_node163; statement_node164; statement_node165; statement_node166; statement_node167; statement_node168; statement_node169; statement_node170; statement_node171; statement_node172; statement_node173; statement_node174; statement_node175; statement_node176; statement_node177; statement_node178; statement_node179; statement_node180; statement_node181; statement_node182; statement_node183; statement_node184; statement_node185; statement_node186; statement_node187; statement_node188; statement_node189; statement_node190; statement_node191; statement_node192; statement_node193; statement_node194; statement_node195; statement_node196; statement_node197; statement_node198; statement_node199; statement_node200; statement_node201; statement_node202; statement_node203; statement_node204; statement_node205; statement_node206; statement_node207; statement_node208; statement_node209; statement_node210; statement_node211; statement_node212; statement_node213; statement_node214; statement_node215; statement_node216; statement_node217; statement_node218; statement_node219; statement_node220; statement_node221; statement_node222; statement_node223; statement_node224; statement_node225; statement_node226; statement_node227; statement_node228; statement_node229; statement_node230; statement_node231; statement_node232; statement_node233; statement_node234; statement_node235; statement_node236; statement_node237; statement_node238; statement_node239; statement_node240; statement_node241; statement_node242; statement_node243; statement_node244; statement_node245; statement_node246; statement_node247; statement_node248; statement_node249; statement_node250; statement_node251; statement_node252; statement_node253; statement_node254; statement_node255; statement_node256; statement_node257; statement_node258; statement_node259; statement_node260; statement_node261; statement_node262; statement_node263; statement_node264; statement_node265; statement_node266; statement_node267; statement_node268; statement_node269; statement_node270; statement_node271; statement_node272; statement_node273; statement_node274; statement_node275; statement_node276; statement_node277; statement_node278; statement_node279; statement_node280; statement_node281; statement_node282; statement_node283; statement_node284; statement_node285; statement_node286; statement_node287; statement_node288; statement_node289; statement_node290; statement_node291; statement_node292; statement_node293; statement_node294; statement_node295; statement_node296; statement_node297; statement_node298; statement_node299; statement_node300; statement_node301; statement_node302; statement_node303; statement_node304; statement_node305; statement_node306; statement_node307; statement_node308; statement_node309; statement_node310; statement_node311; statement_node312; statement_node313; statement_node314; statement_node315; statement_node316; statement_node317; statement_node318; statement_node319; statement_node320; statement_node321; statement_node322; statement_node323; statement_node324; statement_node325; statement_node326; statement_node327; statement_node328; statement_node329; statement_node330; statement_node331; statement_node332; statement_node333; statement_node334; statement_node335; statement_node336; statement_node337; statement_node338; statement_node339; statement_node340; statement_node341; statement_node342; statement_node343; statement_node344; statement_node345; statement_node346; statement_node347; statement_node348; statement_node349; statement_node350; statement_node351; statement_node352; statement_node353; statement_node354; statement_node355; statement_node356; statement_node357; statement_node358; statement_node359; statement_node360; statement_node361; statement_node362; statement_node363; statement_node364; statement_node365; statement_node366; statement_node367; statement_node368; statement_node369; statement_node370; statement_node371; statement_node372; statement_node373; statement_node374; statement_node375; statement_node376; statement_node377; statement_node378; statement_node379; statement_node380; statement_node381; statement_node382; statement_node383; statement_node384; statement_node385; statement_node386; statement_node387; statement_node388; statement_node389; statement_node390; statement_node391; statement_node392; statement_node393; statement_node394; statement_node395; statement_node396; statement_node397; statement_node398; statement_node399; statement_node400; statement_node401; statement_node402; statement_node403; statement_node404; statement_node405; statement_node406; statement_node407; statement_node408; statement_node409; statement_node410; statement_node411; statement_node412; statement_node413; statement_node414; statement_node415; statement_node416; statement_node417; statement_node418; statement_node419; statement_node420; statement_node421; statement_node422; statement_node423; statement_node424; statement_node425; statement_node426; statement_node427; statement_node428; statement_node429; statement_node430; statement_node431; statement_node432; statement_node433; statement_node434; statement_node435; statement_node436; statement_node437; statement_node438; statement_node439; statement_node440; statement_node441; statement_node442; statement_node443; statement_node444; statement_node445; statement_node446; statement_node447; statement_node448; statement_node449; statement_node450; statement_node451; statement_node452; statement_node453; statement_node454; statement_node455; statement_node456; statement_node457; statement_node458; statement_node459; statement_node460; statement_node461; statement_node462; statement_node463; statement_node464; statement_node465; statement_node466; statement_node467; statement_node468; statement_node469; statement_node470; statement_node471; statement_node472; statement_node473; statement_node474; statement_node475; statement_node476; statement_node477; statement_node478; statement_node479; statement_node480; statement_node481; statement_node482; statement_node483; statement_node484; statement_node485; statement_node486; statement_node487; statement_node488; statement_node489; statement_node490; statement_node491; statement_node492; statement_node493; statement_node494; statement_node495; statement_node496; statement_node497; statement_node498; statement_node499; statement_node500; statement_node501; statement_node502; statement_node503; statement_node504; statement_node505; statement_node506; statement_node507; statement_node508; statement_node509; statement_node510; statement_node511; statement_node512; statement_node513; statement_node514; statement_node515; statement_node516; statement_node517; statement_node518; statement_node519; statement_node520; statement_node521; statement_node522; statement_node523]. Definition networkConjunction : Prop := (((((((((statement_node0 /\ statement_node1) /\ (statement_node2 /\ statement_node3)) /\ ((statement_node4 /\ statement_node5) /\ (statement_node6 /\ statement_node7))) /\ (((statement_node8 /\ statement_node9) /\ (statement_node10 /\ statement_node11)) /\ ((statement_node12 /\ statement_node13) /\ (statement_node14 /\ statement_node15)))) /\ ((((statement_node16 /\ statement_node17) /\ (statement_node18 /\ statement_node19)) /\ ((statement_node20 /\ statement_node21) /\ (statement_node22 /\ statement_node23))) /\ (((statement_node24 /\ statement_node25) /\ (statement_node26 /\ statement_node27)) /\ ((statement_node28 /\ statement_node29) /\ (statement_node30 /\ statement_node31))))) /\ (((((statement_node32 /\ statement_node33) /\ (statement_node34 /\ statement_node35)) /\ ((statement_node36 /\ statement_node37) /\ (statement_node38 /\ statement_node39))) /\ (((statement_node40 /\ statement_node41) /\ (statement_node42 /\ statement_node43)) /\ ((statement_node44 /\ statement_node45) /\ (statement_node46 /\ statement_node47)))) /\ ((((statement_node48 /\ statement_node49) /\ (statement_node50 /\ statement_node51)) /\ ((statement_node52 /\ statement_node53) /\ (statement_node54 /\ statement_node55))) /\ (((statement_node56 /\ statement_node57) /\ (statement_node58 /\ statement_node59)) /\ ((statement_node60 /\ statement_node61) /\ (statement_node62 /\ (statement_node63 /\ statement_node64))))))) /\ ((((((statement_node65 /\ statement_node66) /\ (statement_node67 /\ statement_node68)) /\ ((statement_node69 /\ statement_node70) /\ (statement_node71 /\ statement_node72))) /\ (((statement_node73 /\ statement_node74) /\ (statement_node75 /\ statement_node76)) /\ ((statement_node77 /\ statement_node78) /\ (statement_node79 /\ statement_node80)))) /\ ((((statement_node81 /\ statement_node82) /\ (statement_node83 /\ statement_node84)) /\ ((statement_node85 /\ statement_node86) /\ (statement_node87 /\ statement_node88))) /\ (((statement_node89 /\ statement_node90) /\ (statement_node91 /\ statement_node92)) /\ ((statement_node93 /\ statement_node94) /\ (statement_node95 /\ (statement_node96 /\ statement_node97)))))) /\ (((((statement_node98 /\ statement_node99) /\ (statement_node100 /\ statement_node101)) /\ ((statement_node102 /\ statement_node103) /\ (statement_node104 /\ statement_node105))) /\ (((statement_node106 /\ statement_node107) /\ (statement_node108 /\ statement_node109)) /\ ((statement_node110 /\ statement_node111) /\ (statement_node112 /\ statement_node113)))) /\ ((((statement_node114 /\ statement_node115) /\ (statement_node116 /\ statement_node117)) /\ ((statement_node118 /\ statement_node119) /\ (statement_node120 /\ statement_node121))) /\ (((statement_node122 /\ statement_node123) /\ (statement_node124 /\ statement_node125)) /\ ((statement_node126 /\ statement_node127) /\ (statement_node128 /\ (statement_node129 /\ statement_node130)))))))) /\ (((((((statement_node131 /\ statement_node132) /\ (statement_node133 /\ statement_node134)) /\ ((statement_node135 /\ statement_node136) /\ (statement_node137 /\ statement_node138))) /\ (((statement_node139 /\ statement_node140) /\ (statement_node141 /\ statement_node142)) /\ ((statement_node143 /\ statement_node144) /\ (statement_node145 /\ statement_node146)))) /\ ((((statement_node147 /\ statement_node148) /\ (statement_node149 /\ statement_node150)) /\ ((statement_node151 /\ statement_node152) /\ (statement_node153 /\ statement_node154))) /\ (((statement_node155 /\ statement_node156) /\ (statement_node157 /\ statement_node158)) /\ ((statement_node159 /\ statement_node160) /\ (statement_node161 /\ statement_node162))))) /\ (((((statement_node163 /\ statement_node164) /\ (statement_node165 /\ statement_node166)) /\ ((statement_node167 /\ statement_node168) /\ (statement_node169 /\ statement_node170))) /\ (((statement_node171 /\ statement_node172) /\ (statement_node173 /\ statement_node174)) /\ ((statement_node175 /\ statement_node176) /\ (statement_node177 /\ statement_node178)))) /\ ((((statement_node179 /\ statement_node180) /\ (statement_node181 /\ statement_node182)) /\ ((statement_node183 /\ statement_node184) /\ (statement_node185 /\ statement_node186))) /\ (((statement_node187 /\ statement_node188) /\ (statement_node189 /\ statement_node190)) /\ ((statement_node191 /\ statement_node192) /\ (statement_node193 /\ (statement_node194 /\ statement_node195))))))) /\ ((((((statement_node196 /\ statement_node197) /\ (statement_node198 /\ statement_node199)) /\ ((statement_node200 /\ statement_node201) /\ (statement_node202 /\ statement_node203))) /\ (((statement_node204 /\ statement_node205) /\ (statement_node206 /\ statement_node207)) /\ ((statement_node208 /\ statement_node209) /\ (statement_node210 /\ statement_node211)))) /\ ((((statement_node212 /\ statement_node213) /\ (statement_node214 /\ statement_node215)) /\ ((statement_node216 /\ statement_node217) /\ (statement_node218 /\ statement_node219))) /\ (((statement_node220 /\ statement_node221) /\ (statement_node222 /\ statement_node223)) /\ ((statement_node224 /\ statement_node225) /\ (statement_node226 /\ (statement_node227 /\ statement_node228)))))) /\ (((((statement_node229 /\ statement_node230) /\ (statement_node231 /\ statement_node232)) /\ ((statement_node233 /\ statement_node234) /\ (statement_node235 /\ statement_node236))) /\ (((statement_node237 /\ statement_node238) /\ (statement_node239 /\ statement_node240)) /\ ((statement_node241 /\ statement_node242) /\ (statement_node243 /\ statement_node244)))) /\ ((((statement_node245 /\ statement_node246) /\ (statement_node247 /\ statement_node248)) /\ ((statement_node249 /\ statement_node250) /\ (statement_node251 /\ statement_node252))) /\ (((statement_node253 /\ statement_node254) /\ (statement_node255 /\ statement_node256)) /\ ((statement_node257 /\ statement_node258) /\ (statement_node259 /\ (statement_node260 /\ statement_node261))))))))) /\ ((((((((statement_node262 /\ statement_node263) /\ (statement_node264 /\ statement_node265)) /\ ((statement_node266 /\ statement_node267) /\ (statement_node268 /\ statement_node269))) /\ (((statement_node270 /\ statement_node271) /\ (statement_node272 /\ statement_node273)) /\ ((statement_node274 /\ statement_node275) /\ (statement_node276 /\ statement_node277)))) /\ ((((statement_node278 /\ statement_node279) /\ (statement_node280 /\ statement_node281)) /\ ((statement_node282 /\ statement_node283) /\ (statement_node284 /\ statement_node285))) /\ (((statement_node286 /\ statement_node287) /\ (statement_node288 /\ statement_node289)) /\ ((statement_node290 /\ statement_node291) /\ (statement_node292 /\ statement_node293))))) /\ (((((statement_node294 /\ statement_node295) /\ (statement_node296 /\ statement_node297)) /\ ((statement_node298 /\ statement_node299) /\ (statement_node300 /\ statement_node301))) /\ (((statement_node302 /\ statement_node303) /\ (statement_node304 /\ statement_node305)) /\ ((statement_node306 /\ statement_node307) /\ (statement_node308 /\ statement_node309)))) /\ ((((statement_node310 /\ statement_node311) /\ (statement_node312 /\ statement_node313)) /\ ((statement_node314 /\ statement_node315) /\ (statement_node316 /\ statement_node317))) /\ (((statement_node318 /\ statement_node319) /\ (statement_node320 /\ statement_node321)) /\ ((statement_node322 /\ statement_node323) /\ (statement_node324 /\ (statement_node325 /\ statement_node326))))))) /\ ((((((statement_node327 /\ statement_node328) /\ (statement_node329 /\ statement_node330)) /\ ((statement_node331 /\ statement_node332) /\ (statement_node333 /\ statement_node334))) /\ (((statement_node335 /\ statement_node336) /\ (statement_node337 /\ statement_node338)) /\ ((statement_node339 /\ statement_node340) /\ (statement_node341 /\ statement_node342)))) /\ ((((statement_node343 /\ statement_node344) /\ (statement_node345 /\ statement_node346)) /\ ((statement_node347 /\ statement_node348) /\ (statement_node349 /\ statement_node350))) /\ (((statement_node351 /\ statement_node352) /\ (statement_node353 /\ statement_node354)) /\ ((statement_node355 /\ statement_node356) /\ (statement_node357 /\ (statement_node358 /\ statement_node359)))))) /\ (((((statement_node360 /\ statement_node361) /\ (statement_node362 /\ statement_node363)) /\ ((statement_node364 /\ statement_node365) /\ (statement_node366 /\ statement_node367))) /\ (((statement_node368 /\ statement_node369) /\ (statement_node370 /\ statement_node371)) /\ ((statement_node372 /\ statement_node373) /\ (statement_node374 /\ statement_node375)))) /\ ((((statement_node376 /\ statement_node377) /\ (statement_node378 /\ statement_node379)) /\ ((statement_node380 /\ statement_node381) /\ (statement_node382 /\ statement_node383))) /\ (((statement_node384 /\ statement_node385) /\ (statement_node386 /\ statement_node387)) /\ ((statement_node388 /\ statement_node389) /\ (statement_node390 /\ (statement_node391 /\ statement_node392)))))))) /\ (((((((statement_node393 /\ statement_node394) /\ (statement_node395 /\ statement_node396)) /\ ((statement_node397 /\ statement_node398) /\ (statement_node399 /\ statement_node400))) /\ (((statement_node401 /\ statement_node402) /\ (statement_node403 /\ statement_node404)) /\ ((statement_node405 /\ statement_node406) /\ (statement_node407 /\ statement_node408)))) /\ ((((statement_node409 /\ statement_node410) /\ (statement_node411 /\ statement_node412)) /\ ((statement_node413 /\ statement_node414) /\ (statement_node415 /\ statement_node416))) /\ (((statement_node417 /\ statement_node418) /\ (statement_node419 /\ statement_node420)) /\ ((statement_node421 /\ statement_node422) /\ (statement_node423 /\ statement_node424))))) /\ (((((statement_node425 /\ statement_node426) /\ (statement_node427 /\ statement_node428)) /\ ((statement_node429 /\ statement_node430) /\ (statement_node431 /\ statement_node432))) /\ (((statement_node433 /\ statement_node434) /\ (statement_node435 /\ statement_node436)) /\ ((statement_node437 /\ statement_node438) /\ (statement_node439 /\ statement_node440)))) /\ ((((statement_node441 /\ statement_node442) /\ (statement_node443 /\ statement_node444)) /\ ((statement_node445 /\ statement_node446) /\ (statement_node447 /\ statement_node448))) /\ (((statement_node449 /\ statement_node450) /\ (statement_node451 /\ statement_node452)) /\ ((statement_node453 /\ statement_node454) /\ (statement_node455 /\ (statement_node456 /\ statement_node457))))))) /\ ((((((statement_node458 /\ statement_node459) /\ (statement_node460 /\ statement_node461)) /\ ((statement_node462 /\ statement_node463) /\ (statement_node464 /\ statement_node465))) /\ (((statement_node466 /\ statement_node467) /\ (statement_node468 /\ statement_node469)) /\ ((statement_node470 /\ statement_node471) /\ (statement_node472 /\ statement_node473)))) /\ ((((statement_node474 /\ statement_node475) /\ (statement_node476 /\ statement_node477)) /\ ((statement_node478 /\ statement_node479) /\ (statement_node480 /\ statement_node481))) /\ (((statement_node482 /\ statement_node483) /\ (statement_node484 /\ statement_node485)) /\ ((statement_node486 /\ statement_node487) /\ (statement_node488 /\ (statement_node489 /\ statement_node490)))))) /\ (((((statement_node491 /\ statement_node492) /\ (statement_node493 /\ statement_node494)) /\ ((statement_node495 /\ statement_node496) /\ (statement_node497 /\ statement_node498))) /\ (((statement_node499 /\ statement_node500) /\ (statement_node501 /\ statement_node502)) /\ ((statement_node503 /\ statement_node504) /\ (statement_node505 /\ statement_node506)))) /\ ((((statement_node507 /\ statement_node508) /\ (statement_node509 /\ statement_node510)) /\ ((statement_node511 /\ statement_node512) /\ (statement_node513 /\ statement_node514))) /\ (((statement_node515 /\ statement_node516) /\ (statement_node517 /\ statement_node518)) /\ ((statement_node519 /\ statement_node520) /\ (statement_node521 /\ (statement_node522 /\ statement_node523)))))))))). Theorem whole_network_conjunction : networkConjunction. Proof. exact (conj (conj (conj (conj (conj (conj (conj (conj (conj node0 node1) (conj node2 node3)) (conj (conj node4 node5) (conj node6 node7))) (conj (conj (conj node8 node9) (conj node10 node11)) (conj (conj node12 node13) (conj node14 node15)))) (conj (conj (conj (conj node16 node17) (conj node18 node19)) (conj (conj node20 node21) (conj node22 node23))) (conj (conj (conj node24 node25) (conj node26 node27)) (conj (conj node28 node29) (conj node30 node31))))) (conj (conj (conj (conj (conj node32 node33) (conj node34 node35)) (conj (conj node36 node37) (conj node38 node39))) (conj (conj (conj node40 node41) (conj node42 node43)) (conj (conj node44 node45) (conj node46 node47)))) (conj (conj (conj (conj node48 node49) (conj node50 node51)) (conj (conj node52 node53) (conj node54 node55))) (conj (conj (conj node56 node57) (conj node58 node59)) (conj (conj node60 node61) (conj node62 (conj node63 node64))))))) (conj (conj (conj (conj (conj (conj node65 node66) (conj node67 node68)) (conj (conj node69 node70) (conj node71 node72))) (conj (conj (conj node73 node74) (conj node75 node76)) (conj (conj node77 node78) (conj node79 node80)))) (conj (conj (conj (conj node81 node82) (conj node83 node84)) (conj (conj node85 node86) (conj node87 node88))) (conj (conj (conj node89 node90) (conj node91 node92)) (conj (conj node93 node94) (conj node95 (conj node96 node97)))))) (conj (conj (conj (conj (conj node98 node99) (conj node100 node101)) (conj (conj node102 node103) (conj node104 node105))) (conj (conj (conj node106 node107) (conj node108 node109)) (conj (conj node110 node111) (conj node112 node113)))) (conj (conj (conj (conj node114 node115) (conj node116 node117)) (conj (conj node118 node119) (conj node120 node121))) (conj (conj (conj node122 node123) (conj node124 node125)) (conj (conj node126 node127) (conj node128 (conj node129 node130)))))))) (conj (conj (conj (conj (conj (conj (conj node131 node132) (conj node133 node134)) (conj (conj node135 node136) (conj node137 node138))) (conj (conj (conj node139 node140) (conj node141 node142)) (conj (conj node143 node144) (conj node145 node146)))) (conj (conj (conj (conj node147 node148) (conj node149 node150)) (conj (conj node151 node152) (conj node153 node154))) (conj (conj (conj node155 node156) (conj node157 node158)) (conj (conj node159 node160) (conj node161 node162))))) (conj (conj (conj (conj (conj node163 node164) (conj node165 node166)) (conj (conj node167 node168) (conj node169 node170))) (conj (conj (conj node171 node172) (conj node173 node174)) (conj (conj node175 node176) (conj node177 node178)))) (conj (conj (conj (conj node179 node180) (conj node181 node182)) (conj (conj node183 node184) (conj node185 node186))) (conj (conj (conj node187 node188) (conj node189 node190)) (conj (conj node191 node192) (conj node193 (conj node194 node195))))))) (conj (conj (conj (conj (conj (conj node196 node197) (conj node198 node199)) (conj (conj node200 node201) (conj node202 node203))) (conj (conj (conj node204 node205) (conj node206 node207)) (conj (conj node208 node209) (conj node210 node211)))) (conj (conj (conj (conj node212 node213) (conj node214 node215)) (conj (conj node216 node217) (conj node218 node219))) (conj (conj (conj node220 node221) (conj node222 node223)) (conj (conj node224 node225) (conj node226 (conj node227 node228)))))) (conj (conj (conj (conj (conj node229 node230) (conj node231 node232)) (conj (conj node233 node234) (conj node235 node236))) (conj (conj (conj node237 node238) (conj node239 node240)) (conj (conj node241 node242) (conj node243 node244)))) (conj (conj (conj (conj node245 node246) (conj node247 node248)) (conj (conj node249 node250) (conj node251 node252))) (conj (conj (conj node253 node254) (conj node255 node256)) (conj (conj node257 node258) (conj node259 (conj node260 node261))))))))) (conj (conj (conj (conj (conj (conj (conj (conj node262 node263) (conj node264 node265)) (conj (conj node266 node267) (conj node268 node269))) (conj (conj (conj node270 node271) (conj node272 node273)) (conj (conj node274 node275) (conj node276 node277)))) (conj (conj (conj (conj node278 node279) (conj node280 node281)) (conj (conj node282 node283) (conj node284 node285))) (conj (conj (conj node286 node287) (conj node288 node289)) (conj (conj node290 node291) (conj node292 node293))))) (conj (conj (conj (conj (conj node294 node295) (conj node296 node297)) (conj (conj node298 node299) (conj node300 node301))) (conj (conj (conj node302 node303) (conj node304 node305)) (conj (conj node306 node307) (conj node308 node309)))) (conj (conj (conj (conj node310 node311) (conj node312 node313)) (conj (conj node314 node315) (conj node316 node317))) (conj (conj (conj node318 node319) (conj node320 node321)) (conj (conj node322 node323) (conj node324 (conj node325 node326))))))) (conj (conj (conj (conj (conj (conj node327 node328) (conj node329 node330)) (conj (conj node331 node332) (conj node333 node334))) (conj (conj (conj node335 node336) (conj node337 node338)) (conj (conj node339 node340) (conj node341 node342)))) (conj (conj (conj (conj node343 node344) (conj node345 node346)) (conj (conj node347 node348) (conj node349 node350))) (conj (conj (conj node351 node352) (conj node353 node354)) (conj (conj node355 node356) (conj node357 (conj node358 node359)))))) (conj (conj (conj (conj (conj node360 node361) (conj node362 node363)) (conj (conj node364 node365) (conj node366 node367))) (conj (conj (conj node368 node369) (conj node370 node371)) (conj (conj node372 node373) (conj node374 node375)))) (conj (conj (conj (conj node376 node377) (conj node378 node379)) (conj (conj node380 node381) (conj node382 node383))) (conj (conj (conj node384 node385) (conj node386 node387)) (conj (conj node388 node389) (conj node390 (conj node391 node392)))))))) (conj (conj (conj (conj (conj (conj (conj node393 node394) (conj node395 node396)) (conj (conj node397 node398) (conj node399 node400))) (conj (conj (conj node401 node402) (conj node403 node404)) (conj (conj node405 node406) (conj node407 node408)))) (conj (conj (conj (conj node409 node410) (conj node411 node412)) (conj (conj node413 node414) (conj node415 node416))) (conj (conj (conj node417 node418) (conj node419 node420)) (conj (conj node421 node422) (conj node423 node424))))) (conj (conj (conj (conj (conj node425 node426) (conj node427 node428)) (conj (conj node429 node430) (conj node431 node432))) (conj (conj (conj node433 node434) (conj node435 node436)) (conj (conj node437 node438) (conj node439 node440)))) (conj (conj (conj (conj node441 node442) (conj node443 node444)) (conj (conj node445 node446) (conj node447 node448))) (conj (conj (conj node449 node450) (conj node451 node452)) (conj (conj node453 node454) (conj node455 (conj node456 node457))))))) (conj (conj (conj (conj (conj (conj node458 node459) (conj node460 node461)) (conj (conj node462 node463) (conj node464 node465))) (conj (conj (conj node466 node467) (conj node468 node469)) (conj (conj node470 node471) (conj node472 node473)))) (conj (conj (conj (conj node474 node475) (conj node476 node477)) (conj (conj node478 node479) (conj node480 node481))) (conj (conj (conj node482 node483) (conj node484 node485)) (conj (conj node486 node487) (conj node488 (conj node489 node490)))))) (conj (conj (conj (conj (conj node491 node492) (conj node493 node494)) (conj (conj node495 node496) (conj node497 node498))) (conj (conj (conj node499 node500) (conj node501 node502)) (conj (conj node503 node504) (conj node505 node506)))) (conj (conj (conj (conj node507 node508) (conj node509 node510)) (conj (conj node511 node512) (conj node513 node514))) (conj (conj (conj node515 node516) (conj node517 node518)) (conj (conj node519 node520) (conj node521 (conj node522 node523)))))))))). Qed. Theorem whole_network_certificate : Certified allStatements. Proof. exact (@certified_cons statement_node0 _ node0 (@certified_cons statement_node1 _ node1 (@certified_cons statement_node2 _ node2 (@certified_cons statement_node3 _ node3 (@certified_cons statement_node4 _ node4 (@certified_cons statement_node5 _ node5 (@certified_cons statement_node6 _ node6 (@certified_cons statement_node7 _ node7 (@certified_cons statement_node8 _ node8 (@certified_cons statement_node9 _ node9 (@certified_cons statement_node10 _ node10 (@certified_cons statement_node11 _ node11 (@certified_cons statement_node12 _ node12 (@certified_cons statement_node13 _ node13 (@certified_cons statement_node14 _ node14 (@certified_cons statement_node15 _ node15 (@certified_cons statement_node16 _ node16 (@certified_cons statement_node17 _ node17 (@certified_cons statement_node18 _ node18 (@certified_cons statement_node19 _ node19 (@certified_cons statement_node20 _ node20 (@certified_cons statement_node21 _ node21 (@certified_cons statement_node22 _ node22 (@certified_cons statement_node23 _ node23 (@certified_cons statement_node24 _ node24 (@certified_cons statement_node25 _ node25 (@certified_cons statement_node26 _ node26 (@certified_cons statement_node27 _ node27 (@certified_cons statement_node28 _ node28 (@certified_cons statement_node29 _ node29 (@certified_cons statement_node30 _ node30 (@certified_cons statement_node31 _ node31 (@certified_cons statement_node32 _ node32 (@certified_cons statement_node33 _ node33 (@certified_cons statement_node34 _ node34 (@certified_cons statement_node35 _ node35 (@certified_cons statement_node36 _ node36 (@certified_cons statement_node37 _ node37 (@certified_cons statement_node38 _ node38 (@certified_cons statement_node39 _ node39 (@certified_cons statement_node40 _ node40 (@certified_cons statement_node41 _ node41 (@certified_cons statement_node42 _ node42 (@certified_cons statement_node43 _ node43 (@certified_cons statement_node44 _ node44 (@certified_cons statement_node45 _ node45 (@certified_cons statement_node46 _ node46 (@certified_cons statement_node47 _ node47 (@certified_cons statement_node48 _ node48 (@certified_cons statement_node49 _ node49 (@certified_cons statement_node50 _ node50 (@certified_cons statement_node51 _ node51 (@certified_cons statement_node52 _ node52 (@certified_cons statement_node53 _ node53 (@certified_cons statement_node54 _ node54 (@certified_cons statement_node55 _ node55 (@certified_cons statement_node56 _ node56 (@certified_cons statement_node57 _ node57 (@certified_cons statement_node58 _ node58 (@certified_cons statement_node59 _ node59 (@certified_cons statement_node60 _ node60 (@certified_cons statement_node61 _ node61 (@certified_cons statement_node62 _ node62 (@certified_cons statement_node63 _ node63 (@certified_cons statement_node64 _ node64 (@certified_cons statement_node65 _ node65 (@certified_cons statement_node66 _ node66 (@certified_cons statement_node67 _ node67 (@certified_cons statement_node68 _ node68 (@certified_cons statement_node69 _ node69 (@certified_cons statement_node70 _ node70 (@certified_cons statement_node71 _ node71 (@certified_cons statement_node72 _ node72 (@certified_cons statement_node73 _ node73 (@certified_cons statement_node74 _ node74 (@certified_cons statement_node75 _ node75 (@certified_cons statement_node76 _ node76 (@certified_cons statement_node77 _ node77 (@certified_cons statement_node78 _ node78 (@certified_cons statement_node79 _ node79 (@certified_cons statement_node80 _ node80 (@certified_cons statement_node81 _ node81 (@certified_cons statement_node82 _ node82 (@certified_cons statement_node83 _ node83 (@certified_cons statement_node84 _ node84 (@certified_cons statement_node85 _ node85 (@certified_cons statement_node86 _ node86 (@certified_cons statement_node87 _ node87 (@certified_cons statement_node88 _ node88 (@certified_cons statement_node89 _ node89 (@certified_cons statement_node90 _ node90 (@certified_cons statement_node91 _ node91 (@certified_cons statement_node92 _ node92 (@certified_cons statement_node93 _ node93 (@certified_cons statement_node94 _ node94 (@certified_cons statement_node95 _ node95 (@certified_cons statement_node96 _ node96 (@certified_cons statement_node97 _ node97 (@certified_cons statement_node98 _ node98 (@certified_cons statement_node99 _ node99 (@certified_cons statement_node100 _ node100 (@certified_cons statement_node101 _ node101 (@certified_cons statement_node102 _ node102 (@certified_cons statement_node103 _ node103 (@certified_cons statement_node104 _ node104 (@certified_cons statement_node105 _ node105 (@certified_cons statement_node106 _ node106 (@certified_cons statement_node107 _ node107 (@certified_cons statement_node108 _ node108 (@certified_cons statement_node109 _ node109 (@certified_cons statement_node110 _ node110 (@certified_cons statement_node111 _ node111 (@certified_cons statement_node112 _ node112 (@certified_cons statement_node113 _ node113 (@certified_cons statement_node114 _ node114 (@certified_cons statement_node115 _ node115 (@certified_cons statement_node116 _ node116 (@certified_cons statement_node117 _ node117 (@certified_cons statement_node118 _ node118 (@certified_cons statement_node119 _ node119 (@certified_cons statement_node120 _ node120 (@certified_cons statement_node121 _ node121 (@certified_cons statement_node122 _ node122 (@certified_cons statement_node123 _ node123 (@certified_cons statement_node124 _ node124 (@certified_cons statement_node125 _ node125 (@certified_cons statement_node126 _ node126 (@certified_cons statement_node127 _ node127 (@certified_cons statement_node128 _ node128 (@certified_cons statement_node129 _ node129 (@certified_cons statement_node130 _ node130 (@certified_cons statement_node131 _ node131 (@certified_cons statement_node132 _ node132 (@certified_cons statement_node133 _ node133 (@certified_cons statement_node134 _ node134 (@certified_cons statement_node135 _ node135 (@certified_cons statement_node136 _ node136 (@certified_cons statement_node137 _ node137 (@certified_cons statement_node138 _ node138 (@certified_cons statement_node139 _ node139 (@certified_cons statement_node140 _ node140 (@certified_cons statement_node141 _ node141 (@certified_cons statement_node142 _ node142 (@certified_cons statement_node143 _ node143 (@certified_cons statement_node144 _ node144 (@certified_cons statement_node145 _ node145 (@certified_cons statement_node146 _ node146 (@certified_cons statement_node147 _ node147 (@certified_cons statement_node148 _ node148 (@certified_cons statement_node149 _ node149 (@certified_cons statement_node150 _ node150 (@certified_cons statement_node151 _ node151 (@certified_cons statement_node152 _ node152 (@certified_cons statement_node153 _ node153 (@certified_cons statement_node154 _ node154 (@certified_cons statement_node155 _ node155 (@certified_cons statement_node156 _ node156 (@certified_cons statement_node157 _ node157 (@certified_cons statement_node158 _ node158 (@certified_cons statement_node159 _ node159 (@certified_cons statement_node160 _ node160 (@certified_cons statement_node161 _ node161 (@certified_cons statement_node162 _ node162 (@certified_cons statement_node163 _ node163 (@certified_cons statement_node164 _ node164 (@certified_cons statement_node165 _ node165 (@certified_cons statement_node166 _ node166 (@certified_cons statement_node167 _ node167 (@certified_cons statement_node168 _ node168 (@certified_cons statement_node169 _ node169 (@certified_cons statement_node170 _ node170 (@certified_cons statement_node171 _ node171 (@certified_cons statement_node172 _ node172 (@certified_cons statement_node173 _ node173 (@certified_cons statement_node174 _ node174 (@certified_cons statement_node175 _ node175 (@certified_cons statement_node176 _ node176 (@certified_cons statement_node177 _ node177 (@certified_cons statement_node178 _ node178 (@certified_cons statement_node179 _ node179 (@certified_cons statement_node180 _ node180 (@certified_cons statement_node181 _ node181 (@certified_cons statement_node182 _ node182 (@certified_cons statement_node183 _ node183 (@certified_cons statement_node184 _ node184 (@certified_cons statement_node185 _ node185 (@certified_cons statement_node186 _ node186 (@certified_cons statement_node187 _ node187 (@certified_cons statement_node188 _ node188 (@certified_cons statement_node189 _ node189 (@certified_cons statement_node190 _ node190 (@certified_cons statement_node191 _ node191 (@certified_cons statement_node192 _ node192 (@certified_cons statement_node193 _ node193 (@certified_cons statement_node194 _ node194 (@certified_cons statement_node195 _ node195 (@certified_cons statement_node196 _ node196 (@certified_cons statement_node197 _ node197 (@certified_cons statement_node198 _ node198 (@certified_cons statement_node199 _ node199 (@certified_cons statement_node200 _ node200 (@certified_cons statement_node201 _ node201 (@certified_cons statement_node202 _ node202 (@certified_cons statement_node203 _ node203 (@certified_cons statement_node204 _ node204 (@certified_cons statement_node205 _ node205 (@certified_cons statement_node206 _ node206 (@certified_cons statement_node207 _ node207 (@certified_cons statement_node208 _ node208 (@certified_cons statement_node209 _ node209 (@certified_cons statement_node210 _ node210 (@certified_cons statement_node211 _ node211 (@certified_cons statement_node212 _ node212 (@certified_cons statement_node213 _ node213 (@certified_cons statement_node214 _ node214 (@certified_cons statement_node215 _ node215 (@certified_cons statement_node216 _ node216 (@certified_cons statement_node217 _ node217 (@certified_cons statement_node218 _ node218 (@certified_cons statement_node219 _ node219 (@certified_cons statement_node220 _ node220 (@certified_cons statement_node221 _ node221 (@certified_cons statement_node222 _ node222 (@certified_cons statement_node223 _ node223 (@certified_cons statement_node224 _ node224 (@certified_cons statement_node225 _ node225 (@certified_cons statement_node226 _ node226 (@certified_cons statement_node227 _ node227 (@certified_cons statement_node228 _ node228 (@certified_cons statement_node229 _ node229 (@certified_cons statement_node230 _ node230 (@certified_cons statement_node231 _ node231 (@certified_cons statement_node232 _ node232 (@certified_cons statement_node233 _ node233 (@certified_cons statement_node234 _ node234 (@certified_cons statement_node235 _ node235 (@certified_cons statement_node236 _ node236 (@certified_cons statement_node237 _ node237 (@certified_cons statement_node238 _ node238 (@certified_cons statement_node239 _ node239 (@certified_cons statement_node240 _ node240 (@certified_cons statement_node241 _ node241 (@certified_cons statement_node242 _ node242 (@certified_cons statement_node243 _ node243 (@certified_cons statement_node244 _ node244 (@certified_cons statement_node245 _ node245 (@certified_cons statement_node246 _ node246 (@certified_cons statement_node247 _ node247 (@certified_cons statement_node248 _ node248 (@certified_cons statement_node249 _ node249 (@certified_cons statement_node250 _ node250 (@certified_cons statement_node251 _ node251 (@certified_cons statement_node252 _ node252 (@certified_cons statement_node253 _ node253 (@certified_cons statement_node254 _ node254 (@certified_cons statement_node255 _ node255 (@certified_cons statement_node256 _ node256 (@certified_cons statement_node257 _ node257 (@certified_cons statement_node258 _ node258 (@certified_cons statement_node259 _ node259 (@certified_cons statement_node260 _ node260 (@certified_cons statement_node261 _ node261 (@certified_cons statement_node262 _ node262 (@certified_cons statement_node263 _ node263 (@certified_cons statement_node264 _ node264 (@certified_cons statement_node265 _ node265 (@certified_cons statement_node266 _ node266 (@certified_cons statement_node267 _ node267 (@certified_cons statement_node268 _ node268 (@certified_cons statement_node269 _ node269 (@certified_cons statement_node270 _ node270 (@certified_cons statement_node271 _ node271 (@certified_cons statement_node272 _ node272 (@certified_cons statement_node273 _ node273 (@certified_cons statement_node274 _ node274 (@certified_cons statement_node275 _ node275 (@certified_cons statement_node276 _ node276 (@certified_cons statement_node277 _ node277 (@certified_cons statement_node278 _ node278 (@certified_cons statement_node279 _ node279 (@certified_cons statement_node280 _ node280 (@certified_cons statement_node281 _ node281 (@certified_cons statement_node282 _ node282 (@certified_cons statement_node283 _ node283 (@certified_cons statement_node284 _ node284 (@certified_cons statement_node285 _ node285 (@certified_cons statement_node286 _ node286 (@certified_cons statement_node287 _ node287 (@certified_cons statement_node288 _ node288 (@certified_cons statement_node289 _ node289 (@certified_cons statement_node290 _ node290 (@certified_cons statement_node291 _ node291 (@certified_cons statement_node292 _ node292 (@certified_cons statement_node293 _ node293 (@certified_cons statement_node294 _ node294 (@certified_cons statement_node295 _ node295 (@certified_cons statement_node296 _ node296 (@certified_cons statement_node297 _ node297 (@certified_cons statement_node298 _ node298 (@certified_cons statement_node299 _ node299 (@certified_cons statement_node300 _ node300 (@certified_cons statement_node301 _ node301 (@certified_cons statement_node302 _ node302 (@certified_cons statement_node303 _ node303 (@certified_cons statement_node304 _ node304 (@certified_cons statement_node305 _ node305 (@certified_cons statement_node306 _ node306 (@certified_cons statement_node307 _ node307 (@certified_cons statement_node308 _ node308 (@certified_cons statement_node309 _ node309 (@certified_cons statement_node310 _ node310 (@certified_cons statement_node311 _ node311 (@certified_cons statement_node312 _ node312 (@certified_cons statement_node313 _ node313 (@certified_cons statement_node314 _ node314 (@certified_cons statement_node315 _ node315 (@certified_cons statement_node316 _ node316 (@certified_cons statement_node317 _ node317 (@certified_cons statement_node318 _ node318 (@certified_cons statement_node319 _ node319 (@certified_cons statement_node320 _ node320 (@certified_cons statement_node321 _ node321 (@certified_cons statement_node322 _ node322 (@certified_cons statement_node323 _ node323 (@certified_cons statement_node324 _ node324 (@certified_cons statement_node325 _ node325 (@certified_cons statement_node326 _ node326 (@certified_cons statement_node327 _ node327 (@certified_cons statement_node328 _ node328 (@certified_cons statement_node329 _ node329 (@certified_cons statement_node330 _ node330 (@certified_cons statement_node331 _ node331 (@certified_cons statement_node332 _ node332 (@certified_cons statement_node333 _ node333 (@certified_cons statement_node334 _ node334 (@certified_cons statement_node335 _ node335 (@certified_cons statement_node336 _ node336 (@certified_cons statement_node337 _ node337 (@certified_cons statement_node338 _ node338 (@certified_cons statement_node339 _ node339 (@certified_cons statement_node340 _ node340 (@certified_cons statement_node341 _ node341 (@certified_cons statement_node342 _ node342 (@certified_cons statement_node343 _ node343 (@certified_cons statement_node344 _ node344 (@certified_cons statement_node345 _ node345 (@certified_cons statement_node346 _ node346 (@certified_cons statement_node347 _ node347 (@certified_cons statement_node348 _ node348 (@certified_cons statement_node349 _ node349 (@certified_cons statement_node350 _ node350 (@certified_cons statement_node351 _ node351 (@certified_cons statement_node352 _ node352 (@certified_cons statement_node353 _ node353 (@certified_cons statement_node354 _ node354 (@certified_cons statement_node355 _ node355 (@certified_cons statement_node356 _ node356 (@certified_cons statement_node357 _ node357 (@certified_cons statement_node358 _ node358 (@certified_cons statement_node359 _ node359 (@certified_cons statement_node360 _ node360 (@certified_cons statement_node361 _ node361 (@certified_cons statement_node362 _ node362 (@certified_cons statement_node363 _ node363 (@certified_cons statement_node364 _ node364 (@certified_cons statement_node365 _ node365 (@certified_cons statement_node366 _ node366 (@certified_cons statement_node367 _ node367 (@certified_cons statement_node368 _ node368 (@certified_cons statement_node369 _ node369 (@certified_cons statement_node370 _ node370 (@certified_cons statement_node371 _ node371 (@certified_cons statement_node372 _ node372 (@certified_cons statement_node373 _ node373 (@certified_cons statement_node374 _ node374 (@certified_cons statement_node375 _ node375 (@certified_cons statement_node376 _ node376 (@certified_cons statement_node377 _ node377 (@certified_cons statement_node378 _ node378 (@certified_cons statement_node379 _ node379 (@certified_cons statement_node380 _ node380 (@certified_cons statement_node381 _ node381 (@certified_cons statement_node382 _ node382 (@certified_cons statement_node383 _ node383 (@certified_cons statement_node384 _ node384 (@certified_cons statement_node385 _ node385 (@certified_cons statement_node386 _ node386 (@certified_cons statement_node387 _ node387 (@certified_cons statement_node388 _ node388 (@certified_cons statement_node389 _ node389 (@certified_cons statement_node390 _ node390 (@certified_cons statement_node391 _ node391 (@certified_cons statement_node392 _ node392 (@certified_cons statement_node393 _ node393 (@certified_cons statement_node394 _ node394 (@certified_cons statement_node395 _ node395 (@certified_cons statement_node396 _ node396 (@certified_cons statement_node397 _ node397 (@certified_cons statement_node398 _ node398 (@certified_cons statement_node399 _ node399 (@certified_cons statement_node400 _ node400 (@certified_cons statement_node401 _ node401 (@certified_cons statement_node402 _ node402 (@certified_cons statement_node403 _ node403 (@certified_cons statement_node404 _ node404 (@certified_cons statement_node405 _ node405 (@certified_cons statement_node406 _ node406 (@certified_cons statement_node407 _ node407 (@certified_cons statement_node408 _ node408 (@certified_cons statement_node409 _ node409 (@certified_cons statement_node410 _ node410 (@certified_cons statement_node411 _ node411 (@certified_cons statement_node412 _ node412 (@certified_cons statement_node413 _ node413 (@certified_cons statement_node414 _ node414 (@certified_cons statement_node415 _ node415 (@certified_cons statement_node416 _ node416 (@certified_cons statement_node417 _ node417 (@certified_cons statement_node418 _ node418 (@certified_cons statement_node419 _ node419 (@certified_cons statement_node420 _ node420 (@certified_cons statement_node421 _ node421 (@certified_cons statement_node422 _ node422 (@certified_cons statement_node423 _ node423 (@certified_cons statement_node424 _ node424 (@certified_cons statement_node425 _ node425 (@certified_cons statement_node426 _ node426 (@certified_cons statement_node427 _ node427 (@certified_cons statement_node428 _ node428 (@certified_cons statement_node429 _ node429 (@certified_cons statement_node430 _ node430 (@certified_cons statement_node431 _ node431 (@certified_cons statement_node432 _ node432 (@certified_cons statement_node433 _ node433 (@certified_cons statement_node434 _ node434 (@certified_cons statement_node435 _ node435 (@certified_cons statement_node436 _ node436 (@certified_cons statement_node437 _ node437 (@certified_cons statement_node438 _ node438 (@certified_cons statement_node439 _ node439 (@certified_cons statement_node440 _ node440 (@certified_cons statement_node441 _ node441 (@certified_cons statement_node442 _ node442 (@certified_cons statement_node443 _ node443 (@certified_cons statement_node444 _ node444 (@certified_cons statement_node445 _ node445 (@certified_cons statement_node446 _ node446 (@certified_cons statement_node447 _ node447 (@certified_cons statement_node448 _ node448 (@certified_cons statement_node449 _ node449 (@certified_cons statement_node450 _ node450 (@certified_cons statement_node451 _ node451 (@certified_cons statement_node452 _ node452 (@certified_cons statement_node453 _ node453 (@certified_cons statement_node454 _ node454 (@certified_cons statement_node455 _ node455 (@certified_cons statement_node456 _ node456 (@certified_cons statement_node457 _ node457 (@certified_cons statement_node458 _ node458 (@certified_cons statement_node459 _ node459 (@certified_cons statement_node460 _ node460 (@certified_cons statement_node461 _ node461 (@certified_cons statement_node462 _ node462 (@certified_cons statement_node463 _ node463 (@certified_cons statement_node464 _ node464 (@certified_cons statement_node465 _ node465 (@certified_cons statement_node466 _ node466 (@certified_cons statement_node467 _ node467 (@certified_cons statement_node468 _ node468 (@certified_cons statement_node469 _ node469 (@certified_cons statement_node470 _ node470 (@certified_cons statement_node471 _ node471 (@certified_cons statement_node472 _ node472 (@certified_cons statement_node473 _ node473 (@certified_cons statement_node474 _ node474 (@certified_cons statement_node475 _ node475 (@certified_cons statement_node476 _ node476 (@certified_cons statement_node477 _ node477 (@certified_cons statement_node478 _ node478 (@certified_cons statement_node479 _ node479 (@certified_cons statement_node480 _ node480 (@certified_cons statement_node481 _ node481 (@certified_cons statement_node482 _ node482 (@certified_cons statement_node483 _ node483 (@certified_cons statement_node484 _ node484 (@certified_cons statement_node485 _ node485 (@certified_cons statement_node486 _ node486 (@certified_cons statement_node487 _ node487 (@certified_cons statement_node488 _ node488 (@certified_cons statement_node489 _ node489 (@certified_cons statement_node490 _ node490 (@certified_cons statement_node491 _ node491 (@certified_cons statement_node492 _ node492 (@certified_cons statement_node493 _ node493 (@certified_cons statement_node494 _ node494 (@certified_cons statement_node495 _ node495 (@certified_cons statement_node496 _ node496 (@certified_cons statement_node497 _ node497 (@certified_cons statement_node498 _ node498 (@certified_cons statement_node499 _ node499 (@certified_cons statement_node500 _ node500 (@certified_cons statement_node501 _ node501 (@certified_cons statement_node502 _ node502 (@certified_cons statement_node503 _ node503 (@certified_cons statement_node504 _ node504 (@certified_cons statement_node505 _ node505 (@certified_cons statement_node506 _ node506 (@certified_cons statement_node507 _ node507 (@certified_cons statement_node508 _ node508 (@certified_cons statement_node509 _ node509 (@certified_cons statement_node510 _ node510 (@certified_cons statement_node511 _ node511 (@certified_cons statement_node512 _ node512 (@certified_cons statement_node513 _ node513 (@certified_cons statement_node514 _ node514 (@certified_cons statement_node515 _ node515 (@certified_cons statement_node516 _ node516 (@certified_cons statement_node517 _ node517 (@certified_cons statement_node518 _ node518 (@certified_cons statement_node519 _ node519 (@certified_cons statement_node520 _ node520 (@certified_cons statement_node521 _ node521 (@certified_cons statement_node522 _ node522 (@certified_cons statement_node523 _ node523 certified_nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). Qed. Theorem every_network_node_is_proved : forall p, In p allStatements -> p. Proof. intros p H; exact (certified_member allStatements whole_network_certificate p H). Qed. Theorem false_is_not_a_network_node : ~ In False allStatements. Proof. intro H; exact (every_network_node_is_proved False H). Qed. Theorem network_has_no_contradictory_member : forall p, In p allStatements -> ~ ~ p. Proof. intros p H denial; exact (denial (every_network_node_is_proved p H)). Qed. Theorem complete_network_not_false : ~ (networkConjunction -> False). Proof. intro denial; exact (denial whole_network_conjunction). Qed. Theorem scoped_implication_composition : forall P Q R : Prop, (P -> Q) -> (Q -> R) -> P -> R. Proof. intros P Q R first second p; exact (second (first p)). Qed. Theorem scoped_many_conclusion_fork : forall P Q R : Prop, (P -> Q) -> (P -> R) -> P -> Q /\ R. Proof. intros P Q R first second p; exact (conj (first p) (second p)). Qed. Theorem independent_context_union : forall A B P Q : Prop, (A -> P) -> (B -> Q) -> A /\ B -> P /\ Q. Proof. intros A B P Q first second [a b]; exact (conj (first a) (second b)). Qed. Theorem equivalent_context_transport : forall A B P : Prop, (A <-> B) -> (A -> P) -> B -> P. Proof. intros A B P equivalent proof b; exact (proof (proj2 equivalent b)). Qed. Theorem higher_order_path_composition : forall A B C D : Prop, (A -> B) -> (B -> C) -> (C -> D) -> A -> D. Proof. intros A B C D ab bc cd a; exact (cd (bc (ab a))). Qed. Check node0. Print Assumptions node0. Check node1. Print Assumptions node1. Check node2. Print Assumptions node2. Check node3. Print Assumptions node3. Check node4. Print Assumptions node4. Check node5. Print Assumptions node5. Check node6. Print Assumptions node6. Check node7. Print Assumptions node7. Check node8. Print Assumptions node8. Check node9. Print Assumptions node9. Check node10. Print Assumptions node10. Check node11. Print Assumptions node11. Check node12. Print Assumptions node12. Check node13. Print Assumptions node13. Check node14. Print Assumptions node14. Check node15. Print Assumptions node15. Check node16. Print Assumptions node16. Check node17. Print Assumptions node17. Check node18. Print Assumptions node18. Check node19. Print Assumptions node19. Check node20. Print Assumptions node20. Check node21. Print Assumptions node21. Check node22. Print Assumptions node22. Check node23. Print Assumptions node23. Check node24. Print Assumptions node24. Check node25. Print Assumptions node25. Check node26. Print Assumptions node26. Check node27. Print Assumptions node27. Check node28. Print Assumptions node28. Check node29. Print Assumptions node29. Check node30. Print Assumptions node30. Check node31. Print Assumptions node31. Check node32. Print Assumptions node32. Check node33. Print Assumptions node33. Check node34. Print Assumptions node34. Check node35. Print Assumptions node35. Check node36. Print Assumptions node36. Check node37. Print Assumptions node37. Check node38. Print Assumptions node38. Check node39. Print Assumptions node39. Check node40. Print Assumptions node40. Check node41. Print Assumptions node41. Check node42. Print Assumptions node42. Check node43. Print Assumptions node43. Check node44. Print Assumptions node44. Check node45. Print Assumptions node45. Check node46. Print Assumptions node46. Check node47. Print Assumptions node47. Check node48. Print Assumptions node48. Check node49. Print Assumptions node49. Check node50. Print Assumptions node50. Check node51. Print Assumptions node51. Check node52. Print Assumptions node52. Check node53. Print Assumptions node53. Check node54. Print Assumptions node54. Check node55. Print Assumptions node55. Check node56. Print Assumptions node56. Check node57. Print Assumptions node57. Check node58. Print Assumptions node58. Check node59. Print Assumptions node59. Check node60. Print Assumptions node60. Check node61. Print Assumptions node61. Check node62. Print Assumptions node62. Check node63. Print Assumptions node63. Check node64. Print Assumptions node64. Check node65. Print Assumptions node65. Check node66. Print Assumptions node66. Check node67. Print Assumptions node67. Check node68. Print Assumptions node68. Check node69. Print Assumptions node69. Check node70. Print Assumptions node70. Check node71. Print Assumptions node71. Check node72. Print Assumptions node72. Check node73. Print Assumptions node73. Check node74. Print Assumptions node74. Check node75. Print Assumptions node75. Check node76. Print Assumptions node76. Check node77. Print Assumptions node77. Check node78. Print Assumptions node78. Check node79. Print Assumptions node79. Check node80. Print Assumptions node80. Check node81. Print Assumptions node81. Check node82. Print Assumptions node82. Check node83. Print Assumptions node83. Check node84. Print Assumptions node84. Check node85. Print Assumptions node85. Check node86. Print Assumptions node86. Check node87. Print Assumptions node87. Check node88. Print Assumptions node88. Check node89. Print Assumptions node89. Check node90. Print Assumptions node90. Check node91. Print Assumptions node91. Check node92. Print Assumptions node92. Check node93. Print Assumptions node93. Check node94. Print Assumptions node94. Check node95. Print Assumptions node95. Check node96. Print Assumptions node96. Check node97. Print Assumptions node97. Check node98. Print Assumptions node98. Check node99. Print Assumptions node99. Check node100. Print Assumptions node100. Check node101. Print Assumptions node101. Check node102. Print Assumptions node102. Check node103. Print Assumptions node103. Check node104. Print Assumptions node104. Check node105. Print Assumptions node105. Check node106. Print Assumptions node106. Check node107. Print Assumptions node107. Check node108. Print Assumptions node108. Check node109. Print Assumptions node109. Check node110. Print Assumptions node110. Check node111. Print Assumptions node111. Check node112. Print Assumptions node112. Check node113. Print Assumptions node113. Check node114. Print Assumptions node114. Check node115. Print Assumptions node115. Check node116. Print Assumptions node116. Check node117. Print Assumptions node117. Check node118. Print Assumptions node118. Check node119. Print Assumptions node119. Check node120. Print Assumptions node120. Check node121. Print Assumptions node121. Check node122. Print Assumptions node122. Check node123. Print Assumptions node123. Check node124. Print Assumptions node124. Check node125. Print Assumptions node125. Check node126. Print Assumptions node126. Check node127. Print Assumptions node127. Check node128. Print Assumptions node128. Check node129. Print Assumptions node129. Check node130. Print Assumptions node130. Check node131. Print Assumptions node131. Check node132. Print Assumptions node132. Check node133. Print Assumptions node133. Check node134. Print Assumptions node134. Check node135. Print Assumptions node135. Check node136. Print Assumptions node136. Check node137. Print Assumptions node137. Check node138. Print Assumptions node138. Check node139. Print Assumptions node139. Check node140. Print Assumptions node140. Check node141. Print Assumptions node141. Check node142. Print Assumptions node142. Check node143. Print Assumptions node143. Check node144. Print Assumptions node144. Check node145. Print Assumptions node145. Check node146. Print Assumptions node146. Check node147. Print Assumptions node147. Check node148. Print Assumptions node148. Check node149. Print Assumptions node149. Check node150. Print Assumptions node150. Check node151. Print Assumptions node151. Check node152. Print Assumptions node152. Check node153. Print Assumptions node153. Check node154. Print Assumptions node154. Check node155. Print Assumptions node155. Check node156. Print Assumptions node156. Check node157. Print Assumptions node157. Check node158. Print Assumptions node158. Check node159. Print Assumptions node159. Check node160. Print Assumptions node160. Check node161. Print Assumptions node161. Check node162. Print Assumptions node162. Check node163. Print Assumptions node163. Check node164. Print Assumptions node164. Check node165. Print Assumptions node165. Check node166. Print Assumptions node166. Check node167. Print Assumptions node167. Check node168. Print Assumptions node168. Check node169. Print Assumptions node169. Check node170. Print Assumptions node170. Check node171. Print Assumptions node171. Check node172. Print Assumptions node172. Check node173. Print Assumptions node173. Check node174. Print Assumptions node174. Check node175. Print Assumptions node175. Check node176. Print Assumptions node176. Check node177. Print Assumptions node177. Check node178. Print Assumptions node178. Check node179. Print Assumptions node179. Check node180. Print Assumptions node180. Check node181. Print Assumptions node181. Check node182. Print Assumptions node182. Check node183. Print Assumptions node183. Check node184. Print Assumptions node184. Check node185. Print Assumptions node185. Check node186. Print Assumptions node186. Check node187. Print Assumptions node187. Check node188. Print Assumptions node188. Check node189. Print Assumptions node189. Check node190. Print Assumptions node190. Check node191. Print Assumptions node191. Check node192. Print Assumptions node192. Check node193. Print Assumptions node193. Check node194. Print Assumptions node194. Check node195. Print Assumptions node195. Check node196. Print Assumptions node196. Check node197. Print Assumptions node197. Check node198. Print Assumptions node198. Check node199. Print Assumptions node199. Check node200. Print Assumptions node200. Check node201. Print Assumptions node201. Check node202. Print Assumptions node202. Check node203. Print Assumptions node203. Check node204. Print Assumptions node204. Check node205. Print Assumptions node205. Check node206. Print Assumptions node206. Check node207. Print Assumptions node207. Check node208. Print Assumptions node208. Check node209. Print Assumptions node209. Check node210. Print Assumptions node210. Check node211. Print Assumptions node211. Check node212. Print Assumptions node212. Check node213. Print Assumptions node213. Check node214. Print Assumptions node214. Check node215. Print Assumptions node215. Check node216. Print Assumptions node216. Check node217. Print Assumptions node217. Check node218. Print Assumptions node218. Check node219. Print Assumptions node219. Check node220. Print Assumptions node220. Check node221. Print Assumptions node221. Check node222. Print Assumptions node222. Check node223. Print Assumptions node223. Check node224. Print Assumptions node224. Check node225. Print Assumptions node225. Check node226. Print Assumptions node226. Check node227. Print Assumptions node227. Check node228. Print Assumptions node228. Check node229. Print Assumptions node229. Check node230. Print Assumptions node230. Check node231. Print Assumptions node231. Check node232. Print Assumptions node232. Check node233. Print Assumptions node233. Check node234. Print Assumptions node234. Check node235. Print Assumptions node235. Check node236. Print Assumptions node236. Check node237. Print Assumptions node237. Check node238. Print Assumptions node238. Check node239. Print Assumptions node239. Check node240. Print Assumptions node240. Check node241. Print Assumptions node241. Check node242. Print Assumptions node242. Check node243. Print Assumptions node243. Check node244. Print Assumptions node244. Check node245. Print Assumptions node245. Check node246. Print Assumptions node246. Check node247. Print Assumptions node247. Check node248. Print Assumptions node248. Check node249. Print Assumptions node249. Check node250. Print Assumptions node250. Check node251. Print Assumptions node251. Check node252. Print Assumptions node252. Check node253. Print Assumptions node253. Check node254. Print Assumptions node254. Check node255. Print Assumptions node255. Check node256. Print Assumptions node256. Check node257. Print Assumptions node257. Check node258. Print Assumptions node258. Check node259. Print Assumptions node259. Check node260. Print Assumptions node260. Check node261. Print Assumptions node261. Check node262. Print Assumptions node262. Check node263. Print Assumptions node263. Check node264. Print Assumptions node264. Check node265. Print Assumptions node265. Check node266. Print Assumptions node266. Check node267. Print Assumptions node267. Check node268. Print Assumptions node268. Check node269. Print Assumptions node269. Check node270. Print Assumptions node270. Check node271. Print Assumptions node271. Check node272. Print Assumptions node272. Check node273. Print Assumptions node273. Check node274. Print Assumptions node274. Check node275. Print Assumptions node275. Check node276. Print Assumptions node276. Check node277. Print Assumptions node277. Check node278. Print Assumptions node278. Check node279. Print Assumptions node279. Check node280. Print Assumptions node280. Check node281. Print Assumptions node281. Check node282. Print Assumptions node282. Check node283. Print Assumptions node283. Check node284. Print Assumptions node284. Check node285. Print Assumptions node285. Check node286. Print Assumptions node286. Check node287. Print Assumptions node287. Check node288. Print Assumptions node288. Check node289. Print Assumptions node289. Check node290. Print Assumptions node290. Check node291. Print Assumptions node291. Check node292. Print Assumptions node292. Check node293. Print Assumptions node293. Check node294. Print Assumptions node294. Check node295. Print Assumptions node295. Check node296. Print Assumptions node296. Check node297. Print Assumptions node297. Check node298. Print Assumptions node298. Check node299. Print Assumptions node299. Check node300. Print Assumptions node300. Check node301. Print Assumptions node301. Check node302. Print Assumptions node302. Check node303. Print Assumptions node303. Check node304. Print Assumptions node304. Check node305. Print Assumptions node305. Check node306. Print Assumptions node306. Check node307. Print Assumptions node307. Check node308. Print Assumptions node308. Check node309. Print Assumptions node309. Check node310. Print Assumptions node310. Check node311. Print Assumptions node311. Check node312. Print Assumptions node312. Check node313. Print Assumptions node313. Check node314. Print Assumptions node314. Check node315. Print Assumptions node315. Check node316. Print Assumptions node316. Check node317. Print Assumptions node317. Check node318. Print Assumptions node318. Check node319. Print Assumptions node319. Check node320. Print Assumptions node320. Check node321. Print Assumptions node321. Check node322. Print Assumptions node322. Check node323. Print Assumptions node323. Check node324. Print Assumptions node324. Check node325. Print Assumptions node325. Check node326. Print Assumptions node326. Check node327. Print Assumptions node327. Check node328. Print Assumptions node328. Check node329. Print Assumptions node329. Check node330. Print Assumptions node330. Check node331. Print Assumptions node331. Check node332. Print Assumptions node332. Check node333. Print Assumptions node333. Check node334. Print Assumptions node334. Check node335. Print Assumptions node335. Check node336. Print Assumptions node336. Check node337. Print Assumptions node337. Check node338. Print Assumptions node338. Check node339. Print Assumptions node339. Check node340. Print Assumptions node340. Check node341. Print Assumptions node341. Check node342. Print Assumptions node342. Check node343. Print Assumptions node343. Check node344. Print Assumptions node344. Check node345. Print Assumptions node345. Check node346. Print Assumptions node346. Check node347. Print Assumptions node347. Check node348. Print Assumptions node348. Check node349. Print Assumptions node349. Check node350. Print Assumptions node350. Check node351. Print Assumptions node351. Check node352. Print Assumptions node352. Check node353. Print Assumptions node353. Check node354. Print Assumptions node354. Check node355. Print Assumptions node355. Check node356. Print Assumptions node356. Check node357. Print Assumptions node357. Check node358. Print Assumptions node358. Check node359. Print Assumptions node359. Check node360. Print Assumptions node360. Check node361. Print Assumptions node361. Check node362. Print Assumptions node362. Check node363. Print Assumptions node363. Check node364. Print Assumptions node364. Check node365. Print Assumptions node365. Check node366. Print Assumptions node366. Check node367. Print Assumptions node367. Check node368. Print Assumptions node368. Check node369. Print Assumptions node369. Check node370. Print Assumptions node370. Check node371. Print Assumptions node371. Check node372. Print Assumptions node372. Check node373. Print Assumptions node373. Check node374. Print Assumptions node374. Check node375. Print Assumptions node375. Check node376. Print Assumptions node376. Check node377. Print Assumptions node377. Check node378. Print Assumptions node378. Check node379. Print Assumptions node379. Check node380. Print Assumptions node380. Check node381. Print Assumptions node381. Check node382. Print Assumptions node382. Check node383. Print Assumptions node383. Check node384. Print Assumptions node384. Check node385. Print Assumptions node385. Check node386. Print Assumptions node386. Check node387. Print Assumptions node387. Check node388. Print Assumptions node388. Check node389. Print Assumptions node389. Check node390. Print Assumptions node390. Check node391. Print Assumptions node391. Check node392. Print Assumptions node392. Check node393. Print Assumptions node393. Check node394. Print Assumptions node394. Check node395. Print Assumptions node395. Check node396. Print Assumptions node396. Check node397. Print Assumptions node397. Check node398. Print Assumptions node398. Check node399. Print Assumptions node399. Check node400. Print Assumptions node400. Check node401. Print Assumptions node401. Check node402. Print Assumptions node402. Check node403. Print Assumptions node403. Check node404. Print Assumptions node404. Check node405. Print Assumptions node405. Check node406. Print Assumptions node406. Check node407. Print Assumptions node407. Check node408. Print Assumptions node408. Check node409. Print Assumptions node409. Check node410. Print Assumptions node410. Check node411. Print Assumptions node411. Check node412. Print Assumptions node412. Check node413. Print Assumptions node413. Check node414. Print Assumptions node414. Check node415. Print Assumptions node415. Check node416. Print Assumptions node416. Check node417. Print Assumptions node417. Check node418. Print Assumptions node418. Check node419. Print Assumptions node419. Check node420. Print Assumptions node420. Check node421. Print Assumptions node421. Check node422. Print Assumptions node422. Check node423. Print Assumptions node423. Check node424. Print Assumptions node424. Check node425. Print Assumptions node425. Check node426. Print Assumptions node426. Check node427. Print Assumptions node427. Check node428. Print Assumptions node428. Check node429. Print Assumptions node429. Check node430. Print Assumptions node430. Check node431. Print Assumptions node431. Check node432. Print Assumptions node432. Check node433. Print Assumptions node433. Check node434. Print Assumptions node434. Check node435. Print Assumptions node435. Check node436. Print Assumptions node436. Check node437. Print Assumptions node437. Check node438. Print Assumptions node438. Check node439. Print Assumptions node439. Check node440. Print Assumptions node440. Check node441. Print Assumptions node441. Check node442. Print Assumptions node442. Check node443. Print Assumptions node443. Check node444. Print Assumptions node444. Check node445. Print Assumptions node445. Check node446. Print Assumptions node446. Check node447. Print Assumptions node447. Check node448. Print Assumptions node448. Check node449. Print Assumptions node449. Check node450. Print Assumptions node450. Check node451. Print Assumptions node451. Check node452. Print Assumptions node452. Check node453. Print Assumptions node453. Check node454. Print Assumptions node454. Check node455. Print Assumptions node455. Check node456. Print Assumptions node456. Check node457. Print Assumptions node457. Check node458. Print Assumptions node458. Check node459. Print Assumptions node459. Check node460. Print Assumptions node460. Check node461. Print Assumptions node461. Check node462. Print Assumptions node462. Check node463. Print Assumptions node463. Check node464. Print Assumptions node464. Check node465. Print Assumptions node465. Check node466. Print Assumptions node466. Check node467. Print Assumptions node467. Check node468. Print Assumptions node468. Check node469. Print Assumptions node469. Check node470. Print Assumptions node470. Check node471. Print Assumptions node471. Check node472. Print Assumptions node472. Check node473. Print Assumptions node473. Check node474. Print Assumptions node474. Check node475. Print Assumptions node475. Check node476. Print Assumptions node476. Check node477. Print Assumptions node477. Check node478. Print Assumptions node478. Check node479. Print Assumptions node479. Check node480. Print Assumptions node480. Check node481. Print Assumptions node481. Check node482. Print Assumptions node482. Check node483. Print Assumptions node483. Check node484. Print Assumptions node484. Check node485. Print Assumptions node485. Check node486. Print Assumptions node486. Check node487. Print Assumptions node487. Check node488. Print Assumptions node488. Check node489. Print Assumptions node489. Check node490. Print Assumptions node490. Check node491. Print Assumptions node491. Check node492. Print Assumptions node492. Check node493. Print Assumptions node493. Check node494. Print Assumptions node494. Check node495. Print Assumptions node495. Check node496. Print Assumptions node496. Check node497. Print Assumptions node497. Check node498. Print Assumptions node498. Check node499. Print Assumptions node499. Check node500. Print Assumptions node500. Check node501. Print Assumptions node501. Check node502. Print Assumptions node502. Check node503. Print Assumptions node503. Check node504. Print Assumptions node504. Check node505. Print Assumptions node505. Check node506. Print Assumptions node506. Check node507. Print Assumptions node507. Check node508. Print Assumptions node508. Check node509. Print Assumptions node509. Check node510. Print Assumptions node510. Check node511. Print Assumptions node511. Check node512. Print Assumptions node512. Check node513. Print Assumptions node513. Check node514. Print Assumptions node514. Check node515. Print Assumptions node515. Check node516. Print Assumptions node516. Check node517. Print Assumptions node517. Check node518. Print Assumptions node518. Check node519. Print Assumptions node519. Check node520. Print Assumptions node520. Check node521. Print Assumptions node521. Check node522. Print Assumptions node522. Check node523. Print Assumptions node523. Check certified_member. Print Assumptions certified_member. Check whole_network_conjunction. Print Assumptions whole_network_conjunction. Check whole_network_certificate. Print Assumptions whole_network_certificate. Check every_network_node_is_proved. Print Assumptions every_network_node_is_proved. Check false_is_not_a_network_node. Print Assumptions false_is_not_a_network_node. Check network_has_no_contradictory_member. Print Assumptions network_has_no_contradictory_member. Check complete_network_not_false. Print Assumptions complete_network_not_false. Check scoped_implication_composition. Print Assumptions scoped_implication_composition. Check scoped_many_conclusion_fork. Print Assumptions scoped_many_conclusion_fork. Check independent_context_union. Print Assumptions independent_context_union. Check equivalent_context_transport. Print Assumptions equivalent_context_transport. Check higher_order_path_composition. Print Assumptions higher_order_path_composition.